From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Wed, 2 Dec 2015 19:33:06 +0000 (-0500)
Subject: prove that bool is a set
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=a440b67f1413c2e2c4a69db80377c2c3f1bb0d39;p=cubicaltt.git

prove that bool is a set
---

diff --git a/examples/bool.ctt b/examples/bool.ctt
index 5688ea7..a10709c 100644
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -1,9 +1,34 @@
 module bool where
 
-import prelude
+import hedberg
 
 data bool = false | true
 
+caseBool (A : U) (f t : A) : bool -> A = split
+ false -> f
+ true  -> t
+
+falseNeqTrue : neg (Id bool false true) =
+  \(h : Id bool false true) -> subst bool (caseBool U bool N0) false true h false
+
+trueNeqFalse : neg (Id bool true false) =
+  \(h : Id bool true false) -> subst bool (caseBool U N0 bool) true false h true
+
+boolDec : (b1 b2 : bool) -> dec (Id bool b1 b2) = split
+ false -> rem
+  where
+  rem : (b : bool) -> dec (Id bool false b) = split
+   false -> inl (<i> false)
+   true -> inr falseNeqTrue
+ true -> rem
+  where
+  rem : (b : bool) -> dec (Id bool true b) = split
+   false -> inr trueNeqFalse
+   true -> inl (<i> true)
+
+setbool : set bool = hedberg bool boolDec
+
+
       ---------------------------------------------------------
       -- Example: Non-trivial equality between bool and bool --
       ---------------------------------------------------------
@@ -26,7 +51,6 @@ testFalse : bool = transport negBoolEq true
 
 
 
-
 -- An isomorphic representation to bool:
 
 data F2 = zeroF2 | oneF2