From d3d379d409da3e43543e1869915e07aea893b323 Mon Sep 17 00:00:00 2001
From: Anders <mortberg@chalmers.se>
Date: Thu, 23 Apr 2015 17:04:00 +0200
Subject: [PATCH] Elimination principle for set truncation

---
 examples/set.ctt      | 54 +++++++++++++++++++++++++++++++++++++++++++
 examples/setTrunc.ctt | 22 +++++++++++++-----
 2 files changed, 70 insertions(+), 6 deletions(-)
 create mode 100644 examples/set.ctt

diff --git a/examples/set.ctt b/examples/set.ctt
new file mode 100644
index 0000000..04607a6
--- /dev/null
+++ b/examples/set.ctt
@@ -0,0 +1,54 @@
+module set where
+
+sqDepPath (A:U) (F:A->U) (sF:(x:A) -> set (F x))
+          (a0 a1:A) (p:Id A a0 a1) (u0 : F a0) (u1 : F a1) (q r: IdP (<i> F (p@i)) u0 u1) :
+    Id (IdP (<i> F (p@i)) u0 u1) q r = <i j> rem @ j @ i
+ where
+ rem : IdP (<i>Id (F (p@i)) (q@i) (r@i)) (<i>u0) (<i>u1) =
+  <i> let xi : A = p@i
+          ui0 : F xi = transport (<j>F (p @ i/\j)) u0
+          ui1 : F xi = transport (<j>F (p @ i\/-j)) u1
+          qi : Id (F xi) ui0 ui1 = <j>transport (<k>F (p@(i/\-j/\k)\/(i/\j)\/(j/\-k)\/(i/\k))) (q@j)
+          ri : Id (F xi) ui0 ui1 = <j>transport (<k>F (p@(i/\-j/\k)\/(i/\j)\/(j/\-k)\/(i/\k))) (r@j)
+      in  <j>(sF xi ui0 ui1 qi ri @ j @ i)
+
+sqDepPathJ (A:U) (F:A->U) (sF:(x:A) -> set (F x))
+          (a0 : A) : (a1:A) (p:Id A a0 a1) (u0 : F a0) (u1 : F a1) (q r: IdP (<i> F (p@i)) u0 u1) ->
+    Id (IdP (<i> F (p@i)) u0 u1) q r =
+      J A a0 (\ (a1:A) (p:Id A a0 a1) -> (u0 : F a0) (u1 : F a1) (q r: IdP (<i> F (p@i)) u0 u1) ->
+                Id (IdP (<i> F (p@i)) u0 u1) q r) (sF a0)
+
+test (A:U) (F:A->U) (sF:(x:A) -> set (F x))
+          (a0 a1:A) (p:Id A a0 a1) (u0 : F a0) (u1 : F a1) (q r: IdP (<i> F (p@i)) u0 u1) :
+    Id (IdP (<i> F (p@i)) u0 u1) q r = sqDepPathJ A F sF a0 a1 p u0 u1 q r
+
+sqDepPath2 (A:U) (F:A->U) (sF:(x:A) -> set (F x))
+          (a0 a1:A) (p :Id A a0 a1) : (q : Id A a0 a1) (spq : Id (Id A a0 a1) p q)
+          (u0 : F a0) (u1 : F a1)
+          (r : IdP (<i> F (p@i)) u0 u1) (s : IdP (<i> F (q@i)) u0 u1) ->
+    IdP (<i> IdP (<j> F (spq @ i @ j)) u0 u1) r s =
+    J (Id A a0 a1) p
+      (\(q : Id A a0 a1) (spq : Id (Id A a0 a1) p q) ->
+            (u0 : F a0) (u1 : F a1) (r : IdP (<i> F (p@i)) u0 u1)
+            (s : IdP (<i> F (q@i)) u0 u1) -> IdP (<i> IdP (<j> F (spq @ i @ j)) u0 u1) r s) rem
+     where rem : (u0 : F a0) (u1 : F a1) (r s : IdP (<i> F (p@i)) u0 u1) ->
+                 Id (IdP (<j> F (p @ j)) u0 u1) r s = sqDepPath A F sF a0 a1 p
+
+-- <i j> rem @ j @ i
+--  where
+--  rem : IdP (<i> IdP (<j> F (spq @ j @ i)) (r@i) (s@i)) (<i>u0) (<i>u1) =
+--   <i> let xi : A = p @ i
+--           yi : A = q @ i
+--           li : Id A xi yi = <j> spq @ j @ i
+--           ui0 : F xi = transport (<j>F (p @ i/\j)) u0
+--           ui1 : F xi = transport (<j>F (p @ i\/-j)) u1
+--           vi0 : F yi = transport (<j>F (q @ i/\j)) u0
+--           vi1 : F yi = transport (<j>F (q @ i\/-j)) u1          
+--           ri : Id (F xi) ui0 ui1 = <j>transport (<k>F (p@(i/\-j/\k)\/(i/\j)\/(j/\-k)\/(i/\k))) (r@j)
+--           si : Id (F yi) vi0 vi1 = <j>transport (<k>F (q@(i/\-j/\k)\/(i/\j)\/(j/\-k)\/(i/\k))) (s@j)
+--           uvi0 : IdP (<j> F (li @ j)) ui0 vi0 = transport 
+--           uvi1 : IdP (<j> F (li @ j)) ui1 vi1 =
+--           test : U = U
+--       in  <j>(sF xi ui0 ui1 ri si @ j @ i)
+
+
diff --git a/examples/setTrunc.ctt b/examples/setTrunc.ctt
index bd34fba..e9abf8b 100644
--- a/examples/setTrunc.ctt
+++ b/examples/setTrunc.ctt
@@ -1,18 +1,21 @@
 module setTrunc where
 
-import prelude
+import set
 
 data setTrunc (A : U)
   = inc (a : A)
-  | setTr (a b : setTrunc A) (p q : Id (setTrunc A) a b) <i j>
+  | setTrC (a b : setTrunc A) (p q : Id (setTrunc A) a b) <i j>
        [ (i=0) -> p @ j
        , (i=1) -> q @ j
        , (j=0) -> a
        , (j=1) -> b]
 
-setTruncSet (A : U) : set (setTrunc A) =
-   \(a b : setTrunc A) (p q : Id (setTrunc A) a b) ->
-     <i j> setTr {setTrunc A} a b p q @ i @ j
+setTr (A : U) (a b : setTrunc A) (p q : Id (setTrunc A) a b) : Id (Id (setTrunc A) a b) p q =
+  <i j> setTrC {setTrunc A} a b p q @ i @ j
+
+-- setTruncSet (A : U) : set (setTrunc A) =
+--    \(a b : setTrunc A) (p q : Id (setTrunc A) a b) ->
+--      <i j> setTrC {setTrunc A} a b p q @ i @ j
 
 
 setTruncRec (A : U)
@@ -22,7 +25,14 @@ setTruncRec (A : U)
             setTrunc A -> B =
   split
     inc a -> f a
-    setTr a b p q @ i j -> (bS (setTruncRec A B bS f a)
+    setTrC a b p q @ i j -> (bS (setTruncRec A B bS f a)
                                (setTruncRec A B bS f b)
                                (<k> setTruncRec A B bS f (p @ k))
                                (<k> setTruncRec A B bS f (q @ k))) @ i @ j
+
+setTruncElim (A : U) (P : setTrunc A -> U) (sP : (z : setTrunc A) -> set (P z)) (h : (x : A) -> P (inc x))
+  : (z : setTrunc A) -> P z = split
+    inc a -> h a
+    setTrC a b p q @ i j -> sqDepPath2 (setTrunc A) P sP a b p q (setTr A a b p q)
+                                       (f a) (f b) (<k> f (p @ k)) (<k> f (q @ k)) @ i @ j
+      where f : (z : setTrunc A) -> P z = setTruncElim A P sP h
\ No newline at end of file
-- 
2.34.1