Add bool example to univalence.ctt

diff --git a/examples/testUniv.ctt b/examples/testUniv.ctt
deleted file mode 100644 (file)
index 8662cda..0000000
--- a/examples/testUniv.ctt
+++ /dev/null
@@ -1,21 +0,0 @@
-module testUniv where
-
-import testContr
-import equiv
-
-swap : bool -> bool = split
- true -> false
- false -> true
-
-lemSwap : (x:bool) -> Id bool (swap (swap x)) x = split
- true -> <i>true
- false -> <i>false
-
-isEquivSwap : isEquiv bool bool swap =
- gradLemma bool bool swap swap lemSwap lemSwap
-
-eqBool : Id U bool bool = 
- trans (equiv bool bool) (Id U bool bool) (<i>corrUniv bool bool@-i) (swap,isEquivSwap)
-
-test1 : bool = trans bool bool eqBool true
-test2 : bool = trans bool bool eqBool false

diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 513591a4daa952faf5346d8089f8a7c8b83a5fbb..d62066bb49346bf8bd927fa2b69b6c2450496286 100644 (file)
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -139,6 +139,9 @@ corrUniv (A X:U) : Id U (Id U X A) (equiv X A) =
 
 corrUniv' (A B : U) : equiv (Id U A B) (equiv A B) = (lem2 B A,univalence B A)
 
+
+-- Some tests of normal forms:
+
 testUniv1 (A:U) : Id U A A =
   trans (equiv A A) (Id U A A) (<i> corrUniv A A @ -i) (idEquiv A)
 
@@ -158,6 +161,18 @@ ntestUniv2 : bool =
   ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> <j> bool ]) [ (i = 0) -> <j> bool, (i = 1) -> <j> bool ]) true []
 
 
+-- A small test of univalence using boolean negation
+isEquivNegBool : isEquiv bool bool negBool =
+ gradLemma bool bool negBool negBool negBoolK negBoolK
+
+eqBool : Id U bool bool = 
+ trans (equiv bool bool) (Id U bool bool)
+       (<i> corrUniv bool bool @ -i) (negBool,isEquivNegBool)
+
+test1 : bool = trans bool bool eqBool true
+test2 : bool = trans bool bool eqBool false
+
+
 ------------------------------------------------------------------------------
 -- The direct proof of univalence using transEquiv: