From: Rafaël Bocquet Date: Fri, 8 Apr 2016 11:35:53 +0000 (+0200) Subject: slow proof X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=a46458a55eedd3bd1b159246a1fd5662da162600;p=cubicaltt.git slow proof --- diff --git a/examples/torsor0.ctt b/examples/torsor0.ctt new file mode 100644 index 0000000..0825628 --- /dev/null +++ b/examples/torsor0.ctt @@ -0,0 +1,258 @@ +module torsor0 where +import prelude +import int +import circle +import helix +import univalence + +lemEquiv1 (A B : U) (F : A -> B) (G : A -> B) (e : isEquiv A B G) (p : (x : A) -> Id A (e (F x)).1.1 x) : Id (A -> B) F G + = \(x : A) -> transport ( Id B (retEq A B (G, e) (F x) @ i) (G x)) (mapOnPath A B G (e (F x)).1.1 x (p x)) @ i + +transRefl (A : U) (a : A) : Id A (transport (<_> A) a) a = comp (<_> A) a [(i=1) -> <_>a] +lemReflComp (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a a b (<_> a) p) p = + comp ( A) (p @ i /\ j) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> p @ k \/ j ] +lemReflComp' (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a b b p (<_> b)) p = + comp ( A) (p @ i) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <_> b ] + +lem2ItPos : (n:nat) -> Id loopS1 (loopIt (predZ (inr n))) (backTurn (loopIt (inr n))) = split + zero -> transport ( Id loopS1 invLoop (lemReflComp S1 base base invLoop @ -i)) (<_> invLoop) + suc p -> compInv S1 base base (loopIt (inr p)) base loop1 + +lem2It : (n:Z) -> Id loopS1 (loopIt (predZ n)) (backTurn (loopIt n)) = split + inl n -> <_> loopIt (inl (suc n)) + inr n -> lem2ItPos n + +transportCompId (a b c : U) (p1 : Id U a b) (p2 : Id U b c) (x : a) + : Id c (transport (compId U a b c p1 p2) x) (transport p2 (transport p1 x)) + = J U b (\(c : U) -> \(p2 : Id U b c) -> Id c (comp (compId U a b c p1 p2) x []) (comp p2 (transport p1 x) [])) + hole c p2 + where + hole : Id b (comp (compId U a b b p1 (<_> b)) x []) (comp (<_> b) (transport p1 x) []) = + compId b (comp (compId U a b b p1 (<_> b)) x []) (transport p1 x) (comp (<_> b) (transport p1 x) []) + ( comp (lemReflComp' U a b p1 @ i) x []) + ( transRefl b (transport p1 x) @ -i) + +lemRevCompId (A : U) (a b c : A) (p1 : Id A a b) (p2 : Id A b c) + : Id (Id A c a) ( compId A a b c p1 p2 @ -i) (compId A c b a ( p2@-i) ( p1@-i)) + = comp ( A) (hole1 @ i @ j) [(i=0) -> p2 @ k \/ j, (i=1) -> p1 @ -k /\ j] + where + hole1 : Square A b a c b ( p1@-i) ( p2@-i) p2 p1 + = comp ( A) (p1 @ -i \/ j) [(i=0) -> p2 @ j /\ k, (i=1) -> <_> p1@j, (j=0) -> <_> p1@-i, (j=1) -> p2 @ k /\ -i ] + +setPi (A : U) (B : A -> U) (h : (x : A) -> set (B x)) + (f0 f1 : (x : A) -> B x) + (p1 p2 : Id ((x : A) -> B x) f0 f1) + : Id (Id ((x : A) -> B x) f0 f1) p1 p2 + = \(x : A) -> (h x (f0 x) (f1 x) ( (p1@i) x) ( (p2@i) x)) @ i @ j + +lemIdPProp (A B : U) (AProp : prop A) (p : Id U A B) : (x : A) -> (y : B) -> IdP p x y + = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) -> (y : B) -> IdP p x y) AProp B p + +lemIdPSet (A B : U) (ASet : set A) (p : Id U A B) : (x : A) (y : B) (s t : IdP p x y) -> Id (IdP p x y) s t + = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) (y : B) (s t : IdP p x y) -> Id (IdP p x y) s t) ASet B p + +lemIdPSet2 (A B : U) (ASet : set A) (p1 : Id U A B) + : (p2 : Id U A B) -> (p : Id (Id U A B) p1 p2) -> + (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP ( (IdP (p @ i) x y)) s t + = J (Id U A B) p1 (\(p2 : Id U A B) -> \(p : Id (Id U A B) p1 p2) -> (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP ( (IdP (p @ i) x y)) s t) + (lemIdPSet A B ASet p1) + + +isEquivId (A : U) : isEquiv A A (\(x : A) -> x) = gradLemma A A (\(x : A) -> x) (\(x : A) -> x) (\(x : A) -> <_> x) (\(x : A) -> <_> x) + +lem10 (A B : U) (e : equiv A B) (x y : B) (p : Id A (e.2 x).1.1 (e.2 y).1.1) : Id B x y + = transport + (compId U (Id B (e.1 (e.2 x).1.1) (e.1 (e.2 y).1.1)) (Id B x (e.1 (e.2 y).1.1)) (Id B x y) + ( Id B (retEq A B e x @ i) (e.1 (e.2 y).1.1)) ( Id B x (retEq A B e y @ i))) + (mapOnPath A B e.1 (e.2 x).1.1 (e.2 y).1.1 p) + +lem10' (A B : U) (e : equiv A B) (x y : A) (p : Id B (e.1 x) (e.1 y)) : Id A x y + = transport + (compId U (Id A (e.2 (e.1 x)).1.1 (e.2 (e.1 y)).1.1) (Id A x (e.2 (e.1 y)).1.1) (Id A x y) + ( Id A (secEq A B e x @ i) (e.2 (e.1 y)).1.1) ( Id A x (secEq A B e y @ i)) + ) + (mapOnPath B A (invEq A B e) (e.1 x) (e.1 y) p) + + +lem11 (A : U) : Id (Id U A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A) = hole + where + hole0 : Id (equiv A A) + (\(x : A) -> x, isEquivId A) + (transEquiv' A A (<_> A)) + = ( (transRefl (A->A) (\(x : A) -> x) @ -i) + , lemIdPProp (isEquiv A A (\(x : A) -> x)) (isEquiv A A (transEquiv' A A (<_> A)).1) + (propIsEquiv A A (\(x : A) -> x)) ( isEquiv A A (transRefl (A->A) (\(x : A) -> x) @ -j)) + (isEquivId A) (transEquiv' A A (<_> A)).2 @ i + ) + hole1 : Id (equiv A A) (transEquiv' A A (univalence A A (\(x : A) -> x, isEquivId A)).1.1) (\(x : A) -> x, isEquivId A) + = retEq (Id U A A) (equiv A A) (corrUniv' A A) (\(x : A) -> x, isEquivId A) + hole : Id (Id U A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A) + = lem10' (Id U A A) (equiv A A) (corrUniv' A A) + (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A) + (compId (equiv A A) (transEquiv' A A (univalence A A (\(x : A) -> x, isEquivId A)).1.1) (\(x : A) -> x, isEquivId A) (transEquiv' A A (<_> A)) hole1 hole0) + +substIdP (A B : U) (p : Id U A B) (x : A) (y : B) (q : Id B (transport p x) y) : IdP p x y + = transport ( IdP p x (q@i)) hole + where + hole : IdP p x (transport p x) = comp ( p @ (i /\ j)) x [(i=0) -> <_> x] + +lemIdSig (A:U) (B : A -> U) (t u : Sigma A B) : + Id U (Id (Sigma 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 (Sigma 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 + +transConstN (A : U) (a : A) : (n : nat) -> A = split + zero -> a + suc n -> transport (<_> A) (transConstN A a n) + +transConstNRefl (A : U) (a : A) : (n : nat) -> Id A (transConstN A a n) a = split + zero -> <_> a + suc n -> compId A (transport (<_> A) (transConstN A a n)) (transConstN A a n) a + (transRefl A (transConstN A a n)) (transConstNRefl A a n) + +lem0 (A B : U) (f : A -> B) (e : isEquiv A B f) (x : A) + : Id B (transport (univalence B A (f, e)).1.1 x) (f x) + = transConstNRefl B (f x) (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))))) + +lem1 (A B : U) (f : A -> B) (e : isEquiv A B f) (x : B) + : Id A (transport ( (univalence B A (f, e)).1.1 @ -i) x) (e x).1.1 + = compId A + (transConstN A (e (transConstN B x (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))).1.1 (suc (suc (suc zero)))) + (transConstN A (e x).1.1 (suc (suc (suc zero)))) + (e x).1.1 + ( transConstN A (e (transConstNRefl B x (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) @ i)).1.1 (suc (suc (suc zero)))) + (transConstNRefl A (e x).1.1 (suc (suc (suc zero)))) + +-- truncation + +hProp : U = (X : U) * prop X + +ishinh_UU (X : U) : U = (P : hProp) -> ((X -> P.1) -> P.1) + +propishinh (X : U) : prop (ishinh_UU X) = + propPi hProp (\(P : hProp) -> ((X -> P.1) -> P.1)) rem1 + where + rem1 (P : hProp) : prop ((X -> P.1) -> P.1) = + propPi (X -> P.1) (\(_ : X -> P.1) -> P.1) (\(f : X -> P.1) -> P.2) + +ishinh (X : U) : hProp = (ishinh_UU X,propishinh X) + +hinhpr (X : U) : X -> (ishinh X).1 = + \(x : X) (P : hProp) (f : X -> P.1) -> f x + +inhPropContr (A : U) (x : prop A) (y : ishinh_UU A) : isContr A = y (isContr A, propIsContr A) (\(z : A) -> (z, x z)) + +action (A : U) (shift : equiv A A) (x : A) : Z -> A = split + inl n -> invEq A A shift (actionAux n) + where actionAux : nat -> A = split + zero -> x + suc n -> action A shift x (inl n) + inr n -> actionAux n + where actionAux : nat -> A = split + zero -> x + suc n -> shift.1 (action A shift x (inr n)) + +BZ : U = (A : U) * (ASet : set A) * (a : ishinh_UU A) + * (AShift : equiv A A) + * ((x : A) -> isEquiv Z A (action A AShift x)) + +BZSet (x : BZ) : U = x.1 +BZASet (A : BZ) : set (BZSet A) = A.2.1 +BZNE (A : BZ) : ishinh_UU (BZSet A) = A.2.2.1 +BZShift (A : BZ) : equiv (BZSet A) (BZSet A) = A.2.2.2.1 +BZAction (A : BZ) : BZSet A -> Z -> BZSet A = action (BZSet A) (BZShift A) +BZS (A : BZ) : BZSet A -> BZSet A = (BZShift A).1 +BZP (A : BZ) (a : BZSet A) : BZSet A = ((BZShift A).2 a).1.1 +BZEquiv (A : BZ) : (x : BZSet A) -> isEquiv Z (BZSet A) (BZAction A x) = A.2.2.2.2 + +-- Two Z-torsors are equal if their underlying sets are equal in a way compatible with the actions +lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) = hole + where + A : U = BA.1 + ASet : set A = BA.2.1 + a : ishinh_UU A = BA.2.2.1 + AShift : equiv A A = BA.2.2.2.1 + AEquiv : (x : A) -> isEquiv Z A (BZAction BA x) = BA.2.2.2.2 + B : U = BB.1 + BSet : set B = BB.2.1 + b : ishinh_UU B = BB.2.2.1 + BShift : equiv B B = BB.2.2.2.1 + BEquiv : (x : B) -> isEquiv Z B (BZAction BB x) = BB.2.2.2.2 + F (w : (p : Id U A B) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) : Id BZ BA BB = hole + where + p : Id U A B = w.1 + pS : IdP ( p@i -> p@i) (BZS BA) (BZS BB) = w.2 + pASet : IdP ( set (p@i)) ASet BSet = undefined + pNE : IdP ( ishinh_UU (p@i)) a b = undefined + pShift : IdP ( equiv (p@i) (p@i)) AShift BShift = + ( pS @ i + , (lemIdPProp + (isEquiv A A AShift.1) + (isEquiv B B BShift.1) + (propIsEquiv A A AShift.1) + ( isEquiv (p@j) (p@j) (pS@j)) + AShift.2 BShift.2) @ i + ) + pEquiv : IdP ( (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@i) x)) AEquiv BEquiv = undefined + hole : Id BZ BA BB = (p@i, (pASet@i, (pNE@i, (pShift@i, pEquiv@i)))) + G (q : Id BZ BA BB) : (p : Id U A B) * IdP ( p@i -> p@i) (BZS BA) (BZS BB) = ( BZSet (q @ i), (BZShift (q@i)).1) + GF (w : (p : Id U A B) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) + : Id ((p : Id U A B) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) ( BZSet (F w @ i), (BZShift (F w @ i)).1) w + = <_> w + FG (q : Id BZ BA BB) : Id (Id BZ BA BB) (F ( BZSet (q@i), (BZShift (q@i)).1)) q = undefined + hole : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) + = (F, gradLemma ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) F G FG GF) + +lem2 (A : U) (shift : equiv A A) (a : A) : (x : Z) -> Id A (shift.1 (action A shift a x)) (action A shift a (sucZ x)) = split + inl n -> lem2Aux n + where + lem2Aux : (n : nat) -> Id A (shift.1 (action A shift a (inl n))) (action A shift a (sucZ (inl n))) = split + zero -> retEq A A shift a + suc n -> retEq A A shift (action A shift a (inl n)) + inr n -> lem2Aux n + where + lem2Aux : (n : nat) -> Id A (shift.1 (action A shift a (inr n))) (action A shift a (sucZ (inr n))) = split + zero -> <_> shift.1 a + suc n -> <_> shift.1 (action A shift a (inr (suc n))) + +ZBZ : BZ = (Z, (ZSet, (hinhpr Z zeroZ, (ZShift, ZEquiv)))) + where + ZShift : equiv Z Z = (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ) + plus : Z -> Z -> Z = action Z ZShift + ZEquiv (x : Z) : isEquiv Z Z (plus x) = undefined + +loopBZ : U = Id BZ ZBZ ZBZ +compBZ : loopBZ -> loopBZ -> loopBZ = compId BZ ZBZ ZBZ ZBZ + +-- loopBZ = Z = loopS1 + +encodeZ (A : BZ) (p : Id BZ ZBZ A) : BZSet A = transport ( BZSet (p@i)) zeroZ + +decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 ( p @ -i, q @ -i) + where + p1 : isEquiv Z (BZSet A) (BZAction A a) = BZEquiv A a + p : Id U (BZSet A) Z = (univalence (BZSet A) Z (BZAction A a, p1)).1.1 @ -i + q : IdP ( (p@i) -> (p@i)) (BZS A) sucZ = undefined + +prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = undefined + +decodeEncodeZRefl0 + : Id (Id U Z Z) (univalence Z Z (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ)).1.1 (<_> Z) + = transport ( Id (Id U Z Z) (univalence Z Z (prf @ -i)).1.1 (<_> Z)) (lem11 Z) + +decodeEncodeZRefl1 + : IdP ( (IdP ( decodeEncodeZRefl0@j@i -> decodeEncodeZRefl0@j@i) sucZ sucZ)) + ( (BZShift (decodeZ ZBZ zeroZ@i)).1) (<_> sucZ) + = lemIdPSet2 (Z->Z) (Z->Z) (setPi Z (\(_ : Z) -> Z) (\(_ : Z) -> ZSet)) + ( decodeEncodeZRefl0@0@j -> decodeEncodeZRefl0@0@j) + ( decodeEncodeZRefl0@1@j -> decodeEncodeZRefl0@1@j) + ( decodeEncodeZRefl0@i@j -> decodeEncodeZRefl0@i@j) + sucZ sucZ ( (BZShift (decodeZ ZBZ zeroZ@i)).1) (<_> sucZ) + +decodeEncodeZRefl2 : Id ((p : Id U Z Z) * IdP ( p@i -> p@i) sucZ sucZ) ((lemBZ ZBZ ZBZ).2 (decodeZ ZBZ zeroZ)).1.1 ((lemBZ ZBZ ZBZ).2 (<_> ZBZ)).1.1 + = (decodeEncodeZRefl0 @ i, decodeEncodeZRefl1 @ i)