Adapted

diff --git a/examples/bool.ctt b/examples/bool.ctt
index b88db124d0d47b74279e82e6dc90e11b26cfc6e8..8825eea028855e69fa8ba3a701f2cac049b56132 100644 (file)
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -71,8 +71,8 @@ squareBoolF2 : Square U bool bool (refl U bool) bool F2
 test5 : IdP boolEqF2 true oneF2 = 
   <i> transport (<j> boolEqF2 @ i /\ j) true
 
--- test6 : Id bool true true =
---   <i> transport (<j> F2EqBool @ i \/ j) (test5 @ - i)
+test6 : Id bool true true =
+  <i> transport (<j> F2EqBool @ i \/ j) (test5 @ - i)
 
 test7 : Id U F2 F2 =
   subst U (\(X:U) -> Id U X X) bool F2 boolEqF2 negNegEq
@@ -83,5 +83,5 @@ test8 : Id U F2 F2 =
 test9 : Id U F2 F2 =
   transport (<i> Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool)
 
--- p : Id U F2 bool = <i> comp U bool [ (i = 0) -> boolEqF2 ]
--- q : Id U F2 F2 = <i> p @ (i /\ - i)
\ No newline at end of file
+p : Id U F2 bool = <i> comp U bool [ (i = 0) -> boolEqF2 ]
+q : Id U F2 F2 = <i> p @ (i /\ - i)
\ No newline at end of file