From c0237f5181741e9181cb2b70c049c42e219e082c Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Thu, 14 Jan 2016 09:59:51 -0500
Subject: [PATCH] make bool compile and move tests using univalence for bool

---
 examples/bool.ctt       | 26 +++++++++++++++++---------
 examples/univalence.ctt | 15 ---------------
 2 files changed, 17 insertions(+), 24 deletions(-)

diff --git a/examples/bool.ctt b/examples/bool.ctt
index c542ce4..a101367 100644
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -1,13 +1,11 @@
 module bool where
 
 import hedberg
+import univalence
 
 data bool = false | true
 
-
 -- Proof that bool is a set using hedberg:
-
-
 caseBool (A : U) (f t : A) : bool -> A = split
  false -> f
  true  -> t
@@ -32,9 +30,7 @@ boolDec : (b1 b2 : bool) -> dec (Id bool b1 b2) = split
 
 setbool' : set bool = hedberg bool boolDec
 
-
 -- Direct proof that bool is a set:
-
 lem1 : (y:bool) (p:Id bool true y) -> Id bool true y = split
  false -> \ (p : Id bool true false) -> p
  true -> \ (p : Id bool true true) -> <i>true
@@ -48,7 +44,7 @@ lem3 : prop (Id bool true true) =
 
 lem4 : (y:bool) (p:Id bool false y) -> Id bool false y = split
  false -> \ (p : Id bool false false) -> <i>false
- true -> \ (p : Id bool false true) -> p 
+ true -> \ (p : Id bool false true) -> p
 
 lem5 : (x y :bool)  (p:Id bool false x) (q:Id bool false y) -> Id bool x y = split
  false -> \ (y:bool) (p:Id bool false false) (q:Id bool false y) -> lem4 y q
@@ -114,7 +110,7 @@ boolToF2K : (b : bool) -> Id bool (f2ToBool (boolToF2 b)) b = split
 
 boolEqF2 : Id U bool F2 =
  isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K
-  
+
 negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 negBool
 
 -- lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) =
@@ -145,7 +141,7 @@ squareBoolF2 : Square U bool bool bool F2 (refl U bool)
                   boolEqF2 (refl U bool) boolEqF2 =
   <i j> boolEqF2 @ i /\ j
 
-test5 : IdP boolEqF2 true oneF2 = 
+test5 : IdP boolEqF2 true oneF2 =
   <i> comp (<j> boolEqF2 @ i /\ j) true []
 
 test6 : Id bool true true =
@@ -161,4 +157,16 @@ test9 : Id U F2 F2 =
   comp (<i> Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool) []
 
 p : Id U F2 bool = <i> comp (<_> U) bool [ (i = 0) -> boolEqF2, (i = 1) -> <_> bool]
-q : Id U F2 F2 = <i> p @ (i /\ - i)
\ No newline at end of file
+q : Id U F2 F2 = <i> p @ (i /\ - i)
+
+
+-- 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)
+
+testf : bool = trans bool bool eqBool true
+testt : bool = trans bool bool eqBool false
diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 58c6920..2a18e4f 100644
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -6,7 +6,6 @@
 module univalence where
 
 import equiv
--- import bool
 
 ------------------------------------------------------------------------------
 -- Proof of univalence using unglue:
@@ -164,20 +163,6 @@ corrUniv' (A B : U) : equiv (Id U A B) (equiv A B) =
 --   ((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 which is too slow
 -- -- to normalize:
-- 
2.34.1