From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 19 Jan 2017 13:44:39 +0000 (+0100)
Subject: minor changes to bool
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9ae218e0beefd3cc2c617cf6b66ac9faba1a8af7;p=cubicaltt.git

minor changes to bool
---

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