From: Simon Huber <hubsim@gmail.com>
Date: Thu, 4 Jun 2015 08:08:43 +0000 (+0200)
Subject: Adapted
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=5fb54e46045260eae4301dce7b254499033c653d;p=cubicaltt.git

Adapted
---

diff --git a/examples/bool.ctt b/examples/bool.ctt
index b88db12..8825eea 100644
--- 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