the collection of sets is a groupoid

diff --git a/examples/collection.ctt b/examples/collection.ctt
new file mode 100644 (file)
index 0000000..3ebb7d3
--- /dev/null
+++ b/examples/collection.ctt
@@ -0,0 +1,36 @@
+module collection where
+
+import sigma
+import pi
+import univalence
+import retract
+
+lem1 (A B:U) (sB: set B) : set (A -> B) = setPi A (\ (x:A) -> B) (\ (x:A) -> sB)
+
+lem2 (A B : U) (gB:groupoid B) : groupoid (A -> B) = groupoidPi A (\ (x:A) -> B) (\ (x:A) -> gB)
+
+lem3 (A B : U) (t u : Equiv A B) : Id U (Id (Equiv A B) t u) (Id (A -> B) t.1 u.1)
+ = lemSigProp (A->B) (isEquiv A B) (propIsEquiv A B) t u 
+
+lem4 (A B : U) (sB:set B) (t u:Equiv A B) : prop (Id  (Equiv A B) t u)
+ = substInv U prop (Id (Equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (lem1 A B sB t.1 u.1)
+
+lem5 (A B : U) (gB:groupoid B) (t u:Equiv A B) : set (Id (Equiv A B) t u)
+ = substInv U set  (Id (Equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (lem2 A B gB t.1 u.1)
+
+lem6 (A B : U) (sB : set B) : set (Id U A B) = 
+ retractSet (Id U A B) (Equiv A B) (IdToEquiv A B) (EquivToId A B) (secIdEquiv A B) (lem4 A B sB)
+
+-- the collection of all sets
+
+SET : U = (X:U) * set X
+
+-- the collection of all sets is a groupoid
+
+groupoidSET (A B : SET) : set (Id SET A B) = 
+ rem2
+ where
+   rem : set (Id U A.1 B.1) = lem6 A.1 B.1 B.2
+   rem1 : Id U (Id SET A B) (Id U A.1 B.1) = lemSigProp U set setIsProp A B
+   rem2 : set (Id SET A B) = substInv U set (Id SET A B) (Id U A.1 B.1) rem1 rem
+

diff --git a/examples/pi.ctt b/examples/pi.ctt
new file mode 100644 (file)
index 0000000..34b0733
--- /dev/null
+++ b/examples/pi.ctt
@@ -0,0 +1,32 @@
+module pi where
+
+import prelude
+
+pi (A:U) (P:A->U) : U = (x:A) -> P x
+
+idPi (A:U) (B:A->U) (f g : pi A B) : Id U (Id (pi A B) f g) ((x:A) -> Id (B x) (f x) (g x)) =
+ isoId  (Id (pi A B) f g) ((x:A) -> Id (B x) (f x) (g x)) F G S T
+ where T0 : U = Id (pi A B) f g
+       T1 : U = (x:A) -> Id (B x) (f x) (g x)
+       F (p:T0) : T1 = \ (x:A) -> <i>p@i x
+       G (p:T1) : T0 = <i>\ (x:A) -> p x @ i
+       S (p:T1) : Id T1 (F (G p)) p = refl T1 p
+       T (p:T0) : Id T0 (G (F p)) p = refl T0 p
+
+setPi (A:U) (B:A -> U) (h:(x:A) -> set (B x)) (f g:pi A B) : prop (Id (pi A B) f g) =
+ rem
+ where
+  T : U = (x:A) -> Id (B x) (f x) (g x)
+  rem1 : prop T = \ (p q : T) -> <i> \ (x:A) -> h x (f x) (g x) (p x) (q x)@i
+
+  rem : prop (Id (pi A B) f g) =
+    subst U prop T (Id (pi A B) f g) (<i>idPi A B f g@-i) rem1
+
+groupoidPi (A:U) (B:A -> U) (h:(x:A) -> groupoid (B x)) (f g:pi A B) : set (Id (pi A B) f g) =
+    subst U set  T  (Id (pi A B) f g) (<i>idPi A B f g@-i) rem1
+ where
+  T : U = (x:A) -> Id (B x) (f x) (g x)
+  rem1 : set T =  setPi A (\ (x:A) -> Id (B x) (f x) (g x)) (\ (x:A) -> h x (f x) (g x))
+
+
+

diff --git a/examples/sigma.ctt b/examples/sigma.ctt
new file mode 100644 (file)
index 0000000..4f0bee7
--- /dev/null
+++ b/examples/sigma.ctt
@@ -0,0 +1,120 @@
+module sigma where
+
+import deppath
+import equiv
+
+-- application of this fact
+
+sig (A:U) (P : A -> U) : U = (x:A) * P x
+
+lemIdSig  (A:U) (B:A-> U) (t u : sig A B) : Id U (Id (sig A B) t u) ((p:Id A t.1 u.1) * IdP (<i> B (p@i)) t.2 u.2) =
+ isoId T0 T1 f g s t where
+  T0 : U = Id (sig A B) t u
+  T1 : U = (p:Id A t.1 u.1) * IdP (<i> B (p@i)) t.2 u.2
+  f (q:T0) : T1 = (<i> (q@i).1,<i> (q@i).2)
+  g (z:T1) : T0 = <i>(z.1 @i,z.2 @i)
+  s (z:T1) : Id T1 (f (g z)) z = refl T1 z
+  t (q:T0) : Id T0 (g (f q)) q = refl T0 q
+
+lem (A:U) (P:A->U) (pP:(x:A) -> prop (P x)) (u v:(x:A) * P x) (p:Id A u.1 v.1) :
+ Id ((x:A)*P x) u v = <i>(p@i,(lemPropF A P pP u.1 v.1 p u.2 v.2)@i)
+
+propSig (A:U) (B:A-> U) (pA:prop A) (pB : (x:A) -> prop (B x)) (t u : sig A B) : Id (sig A B) t u
+ = lem A B pB t u (pA t.1 u.1)
+
+lem2 (A:U) (B:A-> U) (t u : sig A B) (p:Id A t.1 u.1) : 
+  Id U  (IdP (<i>B (p@i)) t.2 u.2) (Id (B u.1) (transport (<i>B (p@i)) t.2) u.2) =
+    funDepTr (B t.1) (B u.1) P t.2 u.2
+ where P : Id U (B t.1) (B u.1) = <i>B (p@i)
+       T0 : U = IdP P t.2 u.2
+       T1 : U = Id (B u.1) (transport P t.2) u.2
+
+corSigProp (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) (p:Id A t.1 u.1) : 
+  prop (IdP (<i>B (p@i)) t.2 u.2) = substInv U prop T0 T1 rem rem1
+ where P : Id U (B t.1) (B u.1) = <i>B (p@i)
+       T0 : U = IdP P t.2 u.2
+       T1 : U = Id (B u.1) (transport P t.2) u.2
+       rem : Id U T0 T1 = lem2 A B t u p -- funDepTr (B t.1) (B u.1) P t.2 u.2
+       v2 : B u.1 = transport P t.2
+       rem1 : prop T1 = propSet (B u.1) (pB u.1) v2 u.2
+
+corSigSet (A:U) (B:A-> U) (sB : (x:A) -> set (B x)) (t u : sig A B) (p:Id A t.1 u.1) : 
+  prop (IdP (<i>B (p@i)) t.2 u.2) = substInv U prop T0 T1 rem rem1
+ where P : Id U (B t.1) (B u.1) = <i>B (p@i)
+       T0 : U = IdP P t.2 u.2
+       T1 : U = Id (B u.1) (transport P t.2) u.2
+       rem : Id U T0 T1 = lem2 A B t u p -- funDepTr (B t.1) (B u.1) P t.2 u.2
+       v2 : B u.1 = transport P t.2
+       rem1 : prop T1 = sB u.1 v2 u.2
+
+setSig (A:U) (B:A-> U) (sA: set A) (sB : (x:A) -> set (B x)) (t u : sig A B) : prop (Id (sig A B) t u) = 
+  substInv U prop (Id (sig A B) t u) ((p:T) * C p) rem3 rem2
+ where
+   T : U = Id A t.1 u.1
+   C (p:T) : U = IdP (<i> B (p@i)) t.2 u.2
+   rem (p : T) : prop (C p) = corSigSet A B sB t u p
+   rem1 : prop T = sA t.1 u.1
+   rem2 : prop ((p:T) * C p) = propSig T C rem1 rem
+   rem3 : Id U (Id (sig A B) t u) ((p:T) * C p) = lemIdSig A B t u
+
+corSigGroupoid (A:U) (B:A-> U) (gB : (x:A) -> groupoid (B x)) (t u : sig A B) (p:Id A t.1 u.1) : 
+  set (IdP (<i>B (p@i)) t.2 u.2) = substInv U set T0 T1 rem rem1
+ where P : Id U (B t.1) (B u.1) = <i>B (p@i)
+       T0 : U = IdP P t.2 u.2
+       T1 : U = Id (B u.1) (transport P t.2) u.2
+       rem : Id U T0 T1 = lem2 A B t u p -- funDepTr (B t.1) (B u.1) P t.2 u.2
+       v2 : B u.1 = transport P t.2
+       rem1 : set T1 = gB u.1 v2 u.2
+
+groupoidSig (A:U) (B:A-> U) (gA: groupoid A) (gB : (x:A) -> groupoid (B x)) (t u : sig A B) : set (Id (sig A B) t u) = 
+  substInv U set (Id (sig A B) t u) ((p:T) * C p) rem3 rem2
+ where
+   T : U = Id A t.1 u.1
+   C (p:T) : U = IdP (<i> B (p@i)) t.2 u.2
+   rem (p : T) : set (C p) = corSigGroupoid A B gB t u p
+   rem1 : set T = gA t.1 u.1
+   rem2 : set ((p:T) * C p) = setSig T C rem1 rem
+   rem3 : Id U (Id (sig A B) t u) ((p:T) * C p) = lemIdSig A B t u
+
+lem3 (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) (p:Id A t.1 u.1) : 
+  isContr (IdP (<i>B (p@i)) t.2 u.2) =
+ (substInv U prop T0 T1 rem rem1,rem2)
+ where P : Id U (B t.1) (B u.1) = <i>B (p@i)
+       T0 : U = IdP P t.2 u.2
+       T1 : U = Id (B u.1) (transport P t.2) u.2
+       rem : Id U T0 T1 = funDepTr (B t.1) (B u.1) P t.2 u.2 -- lem2 A B t u p -- 
+       v2 : B u.1 = transport P t.2
+       rem1 : prop T1 = propSet (B u.1) (pB u.1) v2 u.2
+       rem2 : T0 = transport (<i>rem@-i) (pB u.1 v2 u.2)
+
+lem6 (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) : Id U ((x:A)*P x) A = isoId T A f g t s
+ where
+   T : U = (x:A) * P x
+   f (z:T) : A = z.1
+   g (x:A) : T = (x,(cA x).2)
+   s (z:T) : Id T (g (f z)) z = <i>(z.1,((cA z.1).1 (cA z.1).2 z.2)@ i)
+   t (x:A) : Id A (f (g x)) x = refl A x
+
+lemSigProp (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) : Id U (Id (sig A B) t u) (Id A t.1 u.1) =
+ compId U (Id (sig A B) t u) ((p:Id A t.1 u.1) * IdP (<i> B (p@i)) t.2 u.2) (Id A t.1 u.1) rem2 rem1
+ where
+   T : U = Id A t.1 u.1
+   C (p:T) : U = IdP (<i> B (p@i)) t.2 u.2
+   rem (p : T) : isContr (C p) = lem3 A B pB t u p
+   rem1 : Id U ((p:T) * C p) T = lem6 T C rem
+   rem2 : Id U (Id (sig A B) t u) ((p:T) * C p) = lemIdSig A B t u
+
+{-
+idSigProp (A:U)(B:A->U)(pB: (x:A) -> prop (B x))(t u : sig A B) (h: Id A t.1 u.1) : Id (sig A B) t u
+ = fun2 A B t u (h,pB u.1  (subst A B t.1 u.1 h t.2) u.2)
+-}
+
+setGroupoid (A:U) (sA:set A) (a0 a1:A) : set (Id A a0 a1) = propSet (Id A a0 a1) (sA a0 a1)
+
+propGroupoid (A:U) (pA: prop A) : groupoid A = setGroupoid A (propSet A pA)
+
+
+
+
+
+