From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 7 Jul 2016 11:38:21 +0000 (+0200)
Subject: more duplicate definitions
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=8518b6c00b42e5b5548de5b13f19189a8fb082f2;p=cubicaltt.git

more duplicate definitions
---

diff --git a/examples/groupoidTrunc.ctt b/examples/groupoidTrunc.ctt
index 1f4502d..6ea3f25 100644
--- a/examples/groupoidTrunc.ctt
+++ b/examples/groupoidTrunc.ctt
@@ -1,12 +1,12 @@
 module groupoidTrunc where
 
-import prelude
 import equiv
-
+import sigma
 
 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>
+  | 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
@@ -14,7 +14,8 @@ data gTrunc (A : U)
        , (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) : 
+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
 
@@ -85,13 +86,6 @@ gTruncElim : (A : U)
            (bG : (z:gTrunc A) -> groupoid (B z))
            (f : (x:A) -> B (inc x)) (z:gTrunc A) -> B z = gTruncElim1 lem
 
-
-
-
-
-
-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