added groupoid truncation

diff --git a/examples/groupoidTrunc.ctt b/examples/groupoidTrunc.ctt
new file mode 100644 (file)
index 0000000..4ce230b
--- /dev/null
+++ b/examples/groupoidTrunc.ctt
@@ -0,0 +1,92 @@
+module groupoidTrunc where
+
+import prelude
+
+data gTrunc (A : U)
+  = inc (a : A)
+  | squashC (a b : gTrunc A) (p q : Id (gTrunc A) a b) (r s: Id (Id (gTrunc A) a b) p q) <i j k>
+       [ (i=0) -> r @ j @ k
+       , (i=1) -> s @ j @ k
+       , (j=0) -> p @ k
+       , (j=1) -> q @ k
+       , (k=0) -> a
+       , (k=1) -> b]
+
+gTr (A:U) (a b : gTrunc A) (p q : Id (gTrunc A) a b) (r s: Id (Id (gTrunc A) a b) p q) : 
+ Id (Id (Id (gTrunc A) a b) p q) r s = 
+ <i j k> squashC{gTrunc A} a b p q r s@ i @ j @k
+
+gTruncRec (A B : U) (bG : groupoid B) (f : A -> B) : gTrunc A -> B = split
+    inc a -> f a
+    squashC a b p q r s @ i j k   -> bG (gTruncRec A B bG f a)
+                                        (gTruncRec A B bG f b)
+                                        (<m> gTruncRec A B bG f (p @ m))
+                                        (<m> gTruncRec A B bG f (q @ m))
+                                        (<m n> gTruncRec A B bG f (r @ m @ n))
+                                        (<m n> gTruncRec A B bG f (s @ m @ n)) @ i @ j @ k
+
+lem1 (A:U) (P:A -> U) (gP:(x:A) -> groupoid (P x)) (a :A) : 
+     (s:Id (Id A a a) (refl A a) (refl A a)) 
+           (t:Id (Id (Id A a a) (refl A a) (refl A a)) (refl (Id A a a) (refl A a)) s)
+           (a1 b1:P a) (p1 q1: Id (P a) a1 b1)
+           (r1 : Id (Id (P a) a1 b1) p1 q1) (s1 : IdP (<i>IdP (<j>P (s@i@j)) a1 b1) p1 q1) ->
+                   IdP (<i>IdP (<j>IdP (<k>P (t@i@j@k)) a1 b1) p1 q1) r1 s1 =
+ J (Id (Id A a a) (refl A a) (refl A a)) (refl (Id A a a) (refl A a))
+   (\ (s:Id (Id A a a) (refl A a) (refl A a)) 
+      (t:Id (Id (Id A a a) (refl A a) (refl A a)) (refl (Id A a a) (refl A a)) s) ->
+      (a1 b1 :P a) (p1 q1: Id (P a) a1 b1)
+      (r1 : Id (Id (P a) a1 b1) p1 q1)  (s1 : IdP (<i>IdP (<j>P (s@i@j)) a1 b1) p1 q1) ->
+      IdP (<i>IdP (<j>IdP (<k>P (t@i@j@k)) a1 b1) p1 q1) r1 s1) (gP a)
+
+lem (A:U) (P:A -> U) (gP:(x:A) -> groupoid (P x))
+    (a :A) : (b:A) (p q:Id A a b) (r s:Id (Id A a b) p q) (t:Id (Id (Id A a b) p q) r s)
+    (a1:P a) (b1:P b) (p1: IdP (<i>P (p@i)) a1 b1) (q1: IdP (<i>P (q@i)) a1 b1)
+    (r1 : IdP (<i>IdP (<j>P (r@i@j)) a1 b1) p1 q1)  (s1 : IdP (<i>IdP (<j>P (s@i@j)) a1 b1) p1 q1) ->
+    IdP (<i>IdP (<j>IdP (<k>P (t@i@j@k)) a1 b1) p1 q1) r1 s1 =
+ J A a (\ (b:A) (p :Id A a b) -> (q:Id A a b) (r s:Id (Id A a b) p q) (t:Id (Id (Id A a b) p q) r s)
+          (a1:P a) (b1:P b) (p1: IdP (<i>P (p@i)) a1 b1) (q1: IdP (<i>P (q@i)) a1 b1)
+          (r1 : IdP (<i>IdP (<j>P (r@i@j)) a1 b1) p1 q1)  (s1 : IdP (<i>IdP (<j>P (s@i@j)) a1 b1) p1 q1) ->
+          IdP (<i>IdP (<j>IdP (<k>P (t@i@j@k)) a1 b1) p1 q1) r1 s1) rem
+ where
+  rem : (q:Id A a a) (r s:Id (Id A a a) (refl A a) q) (t:Id (Id (Id A a a) (refl A a) q) r s)
+        (a1:P a) (b1:P a) (p1: Id (P a) a1 b1) (q1: IdP (<i>P (q@i)) a1 b1)
+        (r1 : IdP (<i>IdP (<j>P (r@i@j)) a1 b1) p1 q1)  (s1 : IdP (<i>IdP (<j>P (s@i@j)) a1 b1) p1 q1) ->
+    IdP (<i>IdP (<j>IdP (<k>P (t@i@j@k)) a1 b1) p1 q1) r1 s1 =
+   J (Id A a a) (refl A a) (\ (q:Id A a a) (r:Id (Id A a a) (refl A a) q) ->
+     (s:Id (Id A a a) (refl A a) q) (t:Id (Id (Id A a a) (refl A a) q) r s)
+     (a1:P a) (b1:P a) (p1: Id (P a) a1 b1) (q1: IdP (<i>P (q@i)) a1 b1)
+     (r1 : IdP (<i>IdP (<j>P (r@i@j)) a1 b1) p1 q1)  (s1 : IdP (<i>IdP (<j>P (s@i@j)) a1 b1) p1 q1) ->
+     IdP (<i>IdP (<j>IdP (<k>P (t@i@j@k)) a1 b1) p1 q1) r1 s1) (lem1 A P gP a)
+
+gTruncElim (A : U)
+           (B : (gTrunc A) -> U)
+           (bG : (z:gTrunc A) -> groupoid (B z))
+           (f : (x:A) -> B (inc x)) : (z:gTrunc A) -> B z = split
+    inc a -> f a
+    squashC a b p q r s @ i j k   -> lem (gTrunc A) B bG a b p q r s
+                                        (gTr A a b p q r s)
+                                        (gTruncElim A B bG f a)
+                                        (gTruncElim A B bG f b)
+                                        (<m> gTruncElim A B bG f (p @ m))
+                                        (<m> gTruncElim A B bG f (q @ m))
+                                        (<m n> gTruncElim A B bG f (r @ m @ n))
+                                        (<m n> gTruncElim A B bG f (s @ m @ n)) @ i @ j @ k
+
+setGroupoid (A:U) (h:set A) (a b:A) : set (Id A a b) =  propSet (Id A a b) (h a b)
+
+univG (A B:U) (bG:groupoid B) : Id U ((gTrunc A) -> B) (A -> B) = 
+   isoId (gTrunc A -> B) (A -> B) F G s t
+ where
+   F (h : gTrunc A -> B) (a: A) : B = h (inc a)
+   G : (A -> B) -> gTrunc A -> B = gTruncRec A B bG
+
+   s (h : A -> B) : Id (A -> B) (F (G h)) h = <i> \ (x:A) -> h x
+
+   t (h : gTrunc A -> B) : Id (gTrunc A -> B) (G (F h)) h = <i> \ (z:gTrunc A) -> rem z @ i
+     where
+      P (z:gTrunc A) : U = Id B (G (F h) z) (h z)
+
+      tP (z : gTrunc A) : groupoid (P z) = setGroupoid (P z) (bG (G (F h) z) (h z))
+
+      rem : (z:gTrunc A) -> P z = gTruncElim A P tP (\ (a:A) -> refl B (h (inc a)))
+