From 9ae218e0beefd3cc2c617cf6b66ac9faba1a8af7 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Thu, 19 Jan 2017 14:44:39 +0100
Subject: [PATCH] minor changes to bool

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

diff --git a/examples/bool.ctt b/examples/bool.ctt
index 396982a..89b365d 100644
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -77,12 +77,17 @@ negBool : bool -> bool = split
 
 -- negBool is involutive:
 negBoolK : (b : bool) -> Path bool (negBool (negBool b)) b = split
-  false -> refl bool false
-  true -> refl bool true
+  false -> <i> false
+  true  -> <i> true
+
+-- negBool is hence and equivalence:
+negBoolEquiv : equiv bool bool =
+  (negBool,gradLemma bool bool negBool negBool negBoolK negBoolK)
 
 -- This defines a non-trivial equality between bool and bool:
 negBoolEq : Path U bool bool =
-  isoPath bool bool negBool negBool negBoolK negBoolK
+  <i> Glue bool [ (i = 0) -> (bool,negBoolEquiv)
+                , (i = 1) -> (bool,idEquiv bool) ]
 
 -- We can transport true along this non-trivial equality:
 testFalse : bool = transport negBoolEq true
-- 
2.34.1