From 5fb54e46045260eae4301dce7b254499033c653d Mon Sep 17 00:00:00 2001
From: Simon Huber <hubsim@gmail.com>
Date: Thu, 4 Jun 2015 10:08:43 +0200
Subject: [PATCH] Adapted

---
 examples/bool.ctt | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

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
-- 
2.34.1