From: coquand Date: Tue, 29 Dec 2015 15:16:37 +0000 (+0100) Subject: updated collection X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9da12cd5f777c8c12b2504fc4ad0d3d06efd9524;p=cubicaltt.git updated collection --- diff --git a/examples/collection.ctt b/examples/collection.ctt index 984f6e2..ee294b9 100644 --- a/examples/collection.ctt +++ b/examples/collection.ctt @@ -2,8 +2,22 @@ module collection where import sigma import pi -import univalence -import retract +import testContr + +propIsContr (A:U) (z0 z1:isContr A) : Id (isContr A) z0 z1 = + (p0 a1@j, + \ (x:A) -> + comp (<_>A) (lem1 x@i@j) [ (i=0) -> p0 a1@j, (i=1) -> p0 x@(j\/k), + (j=0) -> p0 x@(i/\k), (j=1) -> p1 x@i ]) + where + a0 : A = z0.1 + p0 : (x:A) -> Id A a0 x = z0.2 + a1 : A = z1.1 + p1 : (x:A) -> Id A a1 x = z1.2 + lem1 (x:A) : IdP (Id A a0 (p1 x@i)) (p0 a1) (p0 x) = p0 (p1 x@i) @ j + +propIsEquiv (A B : U) (f : A -> B) + : prop (isEquiv A B f) = \ (u0 u1:isEquiv A B f) -> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i setFun (A B:U) (sB: set B) : set (A -> B) = setPi A (\ (x:A) -> B) (\ (x:A) -> sB) @@ -19,7 +33,7 @@ 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) (groupoidFun A B gB t.1 u.1) lem6 (A B : U) (sB : set B) : set (Id U A B) = - substInv U set (Id U A B) (equiv A B) (univalence1 A B) (lem4 A B sB) + substInv U set (Id U A B) (equiv A B) (corrUniv B A) (lem4 A B sB) -- the collection of all sets diff --git a/examples/sigma.ctt b/examples/sigma.ctt index faee60c..cd124eb 100644 --- a/examples/sigma.ctt +++ b/examples/sigma.ctt @@ -33,10 +33,7 @@ funDepTr (A:U) (P:A->U) (a0 a1 :A) (p:Id A a0 a1) (u0:P a0) (u1:P a1) : 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 + funDepTr A B t.1 u.1 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 @@ -93,7 +90,7 @@ lem3 (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) (p:Id A t.1 u.1) 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 -- + rem : Id U T0 T1 = 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) diff --git a/examples/testContr.ctt b/examples/testContr.ctt index 2d7b3a4..c65dafd 100644 --- a/examples/testContr.ctt +++ b/examples/testContr.ctt @@ -77,7 +77,6 @@ equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (sig A B) (retFunFib A B C f x z) (isEquivContr (sig A B) (sig A C) cB cC (totalFun A B C f) (x,z)) - lemSinglContr (A:U) (a:A) : isContr ((x:A) * Id A a x) = ((a,refl A a),\ (z:(x:A) * Id A a x) -> contrSingl A a z.1 z.2)