From 965cc99c0539aeb52957a17314ee339c09b8ac1f Mon Sep 17 00:00:00 2001 From: coquand Date: Thu, 30 Apr 2015 10:30:52 +0200 Subject: [PATCH] the collection of sets is a groupoid --- examples/collection.ctt | 36 ++++++++++++ examples/pi.ctt | 32 +++++++++++ examples/sigma.ctt | 120 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 188 insertions(+) create mode 100644 examples/collection.ctt create mode 100644 examples/pi.ctt create mode 100644 examples/sigma.ctt diff --git a/examples/collection.ctt b/examples/collection.ctt new file mode 100644 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 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) -> p@i x + G (p:T1) : T0 = \ (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) -> \ (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) (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) (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 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 ( 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 ( B (p@i)) t.2 u.2 + f (q:T0) : T1 = ( (q@i).1, (q@i).2) + g (z:T1) : T0 = (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 = (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 (B (p@i)) t.2 u.2) (Id (B u.1) (transport (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) = 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 (B (p@i)) t.2 u.2) = substInv U prop T0 T1 rem rem1 + where P : Id U (B t.1) (B u.1) = 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 (B (p@i)) t.2 u.2) = substInv U prop T0 T1 rem rem1 + where P : Id U (B t.1) (B u.1) = 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 ( 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 (B (p@i)) t.2 u.2) = substInv U set T0 T1 rem rem1 + where P : Id U (B t.1) (B u.1) = 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 ( 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 (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) = 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 (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 = (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 ( 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 ( 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) + + + + + + -- 2.34.1