prove that bool is a set

diff --git a/examples/bool.ctt b/examples/bool.ctt
index 5688ea70ff630850e03d84a1f2225707e0ceff5b..a10709c4a1053472ba8dbade1bb9df7703a65888 100644 (file)
--- 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