From: Anders Mörtberg Date: Thu, 19 Apr 2018 14:22:12 +0000 (-0400) Subject: copy over brunerie.ctt from hcomptrans branch. some computations are very slow X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f13541bb0684237fbf4f661c5f68363c591997f3;p=cubicaltt.git copy over brunerie.ctt from hcomptrans branch. some computations are very slow --- diff --git a/examples/brunerie.ctt b/examples/brunerie.ctt index d09daff..d1abdbd 100644 --- a/examples/brunerie.ctt +++ b/examples/brunerie.ctt @@ -1,3 +1,29 @@ +{- + +The structure of the file is as follows (numbers as in Appendix B in +Guillaume's thesis): + +B.3 Suspension and spheres + +B.4 Pointed types, pointed maps and loop spaces + +B.5 Loop space of a suspension + +B.6 The 3-sphere and the join of two circles + +B.7 The main map + +B.8 The map defining pi3(S2) + +B.9 Going back to pi2(S2) + +B.10 Loop space of truncations + +B.11 Down one more dimension + +B.2 The definition + +-} module brunerie where data bool = false | true @@ -24,11 +50,20 @@ mtwoZ : Z = neg (suc zero) Path (A : U) (a0 a1 : A) : U = PathP ( A) a0 a1 +Sigma (A : U) (B : A -> U) : U = (x : A) * B x +refl (A : U) (a : A) : Path A a a = a + Square (A : U) (a0 a1 b0 b1 : A) (u : Path A a0 a1) (v : Path A b0 b1) (r0 : Path A a0 b0) (r1 : Path A a1 b1) : U = PathP ( (PathP ( A) (u @ i) (v @ i))) r0 r1 +constSquare (A : U) (a : A) (p : Path A a a) : Square A a a a a p p p p = + comp (<_> A) a [ (i = 0) -> p @ (j \/ - k) + , (i = 1) -> p @ (j /\ k) + , (j = 0) -> p @ (i \/ - k) + , (j = 1) -> p @ (i /\ k)] + compPath (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c = comp (<_> A) (p @ i) [ (i =0) -> a, (i = 1) -> q ] @@ -49,6 +84,19 @@ compInvPath (A : U) (a b : A) (p : Path A a b) : , (i = 1) -> p @ j \/ k ] +-- p ; 1 = p +compPath1 (A : U) (a b : A) (p : Path A a b) : + Path (Path A a b) (compPath A a b b p (<_> b)) p = + comp (<_> A) (p @ i /\ -j) [ (i = 0) -> <_> a + , (i = 1) -> p @ -j \/ k + , (j = 1) -> p @ i /\ k ] +-- 1 ; p = p +comp1Path (A : U) (a b : A) (p : Path A a b) : + Path (Path A a b) (compPath A a a b (<_> a) p) p = + comp (<_> A) a [ (i = 0) -> a + , (i = 1) -> p + , (j = 1) -> p @ i /\ k ] + -------------------------------------------------------------------------------- -- B.3 Suspension and spheres @@ -92,7 +140,6 @@ meridP (A : U) (a : A) : Path (susp A) north south = S2 : U = susp S1 S3 : U = susp S2 - -------------------------------------------------------------------------------- -- B.4 Pointed types, pointed maps and loop spaces @@ -147,7 +194,7 @@ mapOmegaRefl2 (A : ptType) (B : U) (h : A.1 -> B) (p : (Omega2 A).1) : mapOmegaRefl3 (A : ptType) (B : U) (h : A.1 -> B) (p : (Omega3 A).1) : (Omega3 (B, h (pt A))).1 = h (p @ i @ j @ k) -- mapOmegaRefl2 (Omega A) (Omega (B,h (pt A))).1 (mapOmegaRefl A B h) - + -------------------------------------------------------------------------------- -- B.5 Loop space of a suspension @@ -162,7 +209,6 @@ phi (A : ptType) : ptMap A (Omega (susppt A.1)) = (g,pg) compPathInv (susp A.1) north south (meridP A.1 (pt A)) in p - -------------------------------------------------------------------------------- -- B.6 The 3-sphere and the join of two circles @@ -222,41 +268,46 @@ joinassoc1 (A B C : U) : join A (join B C) -> join (join A B) C = split -- Map from [join (join A B) C] to [join A (join B C)] --- l2rInl (A B C : U) : join A B -> join A (join B C) = split --- inl a -> inl a --- inr b -> inr (inl b) --- push a b @ i -> pushP A (join B C) a (inl b) @ i - --- l2rPushInr (A B C : U) (b : B) (c : C) : --- Path (join A (join B C)) (inr (inl b)) (inr (inr c)) = inr (pushP B C b c@i) - --- l2rSquare (A B C : U) (a : A) (b : B) (c : C) : --- PathP ( Path (join A (join B C)) (inl a) (inr (pushP B C b c@i))) --- (pushP A (join B C) a (inl b)@i) (pushP A (join B C) a (inr c)@i) = --- pushP A (join B C) a (pushP B C b c@i)@j - --- opl2r (A : U) (a b c : A) (p : Path A a c) (q : Path A a b) (r : Path A b c) --- (sq : Square A a a b c (<_> a) r q p) : Square A a b c c q (<_> c) p r = undefined --- -- comp A (sq@j@i) [(i=0) -> p@(j/\k),(j=1) -> p@(i\/k)] - --- l2rPushPush (A B C : U) (a : A) (b : B) (c : C) : --- Square (join A (join B C)) (inl a) (inr (inl b)) (inr (inr c)) (inr (inr c)) --- (pushP A (join B C) a (inl b)) (<_> inr (inr c)) --- (pushP A (join B C) a (inr c)) (l2rPushInr A B C b c) = --- opl2r (join A (join B C)) (inl a) (inr (inl b)) (inr (inr c)) --- (pushP A (join B C) a (inr c)) (pushP A (join B C) a (inl b)) (l2rPushInr A B C b c) --- (l2rSquare A B C a b c) - --- l2rPush (A B C : U) (c : C) : (u : join A B) -> --- Path (join A (join B C)) (l2rInl A B C u) (inr (inr c)) = split --- inl a -> pushP A (join B C) a (inr c) --- inr b -> l2rPushInr A B C b c --- push a b @ i -> l2rPushPush A B C a b c @ i - --- joinassoc2 (A B C : U) : join (join A B) C -> join A (join B C) = split --- inl jab -> l2rInl A B C jab --- inr c -> inr (inr c) --- push p q @ i -> l2rPush A B C q p @ i +l2rInl (A B C : U) : join A B -> join A (join B C) = split + inl a -> inl a + inr b -> inr (inl b) + push a b @ i -> pushP A (join B C) a (inl b) @ i + +l2rPushInr (A B C : U) (b : B) (c : C) : + Path (join A (join B C)) (inr (inl b)) (inr (inr c)) = inr (pushP B C b c @ i) + +l2rSquare (A B C : U) (a : A) (b : B) (c : C) : + PathP ( Path (join A (join B C)) (inl a) (inr (pushP B C b c @ i))) + ( pushP A (join B C) a (inl b) @ i) ( pushP A (join B C) a (inr c) @ i) = + pushP A (join B C) a (pushP B C b c @ i) @ j + +opl2r (A : U) (a b c : A) (p : Path A a c) (q : Path A a b) (r : Path A b c) + (sq : Square A a a b c (<_> a) r q p) : + Square A a b c c q (<_> c) p r = + comp (<_> A) (q @ i \/ j) + [ (i = 0) -> sq @ k @ j + , (i = 1) -> r @ j /\ k + , (j = 0) -> q @ i + , (j = 1) -> r @ k ] + +l2rPushPush (A B C : U) (a : A) (b : B) (c : C) : + Square (join A (join B C)) (inl a) (inr (inl b)) (inr (inr c)) (inr (inr c)) + (pushP A (join B C) a (inl b)) (<_> inr (inr c)) + (pushP A (join B C) a (inr c)) (l2rPushInr A B C b c) = + opl2r (join A (join B C)) (inl a) (inr (inl b)) (inr (inr c)) + (pushP A (join B C) a (inr c)) (pushP A (join B C) a (inl b)) (l2rPushInr A B C b c) + (l2rSquare A B C a b c) + +l2rPush (A B C : U) (c : C) : (u : join A B) -> + Path (join A (join B C)) (l2rInl A B C u) (inr (inr c)) = split + inl a -> pushP A (join B C) a (inr c) + inr b -> l2rPushInr A B C b c + push a b @ i -> l2rPushPush A B C a b c @ i + +joinassoc2 (A B C : U) : join (join A B) C -> join A (join B C) = split + inl jab -> l2rInl A B C jab + inr c -> inr (inr c) + push p q @ i -> l2rPush A B C q p @ i mapJoin (A A' B B' : U) (f : A -> A') (g : B -> B') : join A B -> join A' B' = split @@ -264,11 +315,6 @@ mapJoin (A A' B B' : U) (f : A -> A') (g : B -> B') : join A B -> join A' B' = s inr b -> inr (g b) push a b @ i -> pushP A' B' (f a) (g b) @ i --- TODO: mapJoin is pointed as soon as f is --- mapJoinPt (A A' : ptType) (B B' : U) (f : ptMap A A') (g : B -> B') : --- ptMap (joinpt A B) (joinpt A' B') = undefined - - -- B.6.2 Suspension and join with the booleans -- It is not necessary that the maps here are pointed yet, we fix it -- in the end after composing them @@ -291,7 +337,7 @@ psiinv (A : U) : join bool A -> susp A = split false -> <_> south true -> meridP A a in case a b @ i - + -- I define c by going via susp bool -- TODO: maybe do it directly? @@ -324,7 +370,15 @@ e (x : S3) : join S1 S1 = res : join S1 S1 = mapJoin (join bool bool) S1 S1 S1 c (idfun S1) x3 in res --- einv : join S1 S1 -> S3 = undefined +einv (x : join S1 S1) : S3 = + let x1 : join (join bool bool) S1 = + mapJoin S1 (join bool bool) S1 S1 cinv (idfun S1) x + x2 : join bool (join bool S1) = joinassoc2 bool bool S1 x1 + x3 : join bool S2 = + mapJoin bool bool (join bool S1) S2 (idfun bool) (psiinv S1) x2 + res : S3 = psiinv S2 x3 + in res + -------------------------------------------------------------------------------- @@ -342,22 +396,1653 @@ prealpha : join S1 S1 -> S2 = split alpha : ptMap (joinpt S1pt S1) S2pt = (prealpha, <_> north) +{- + -------------------------------------------------------------------------------- -- B.8 The map defining pi3(S2) +-- This is where things get complicated and slow. This is also the place where +-- univalence is first needed. + + +-- Basic results about equivalences and lower h-levels: + +isContr (A : U) : U = (x : A) * ((y : A) -> Path A x y) + +prop (A : U) : U = (a b : A) -> Path A a b +set (A : U) : U = (a b : A) -> prop (Path A a b) +groupoid (A : U) : U = (a b : A) -> set (Path A a b) +twogroupoid (A : U) : U = (a b : A) -> groupoid (Path A a b) +threegroupoid (A : U) : U = (a b : A) -> twogroupoid (Path A a b) + +SET : U = (A : U) * set A +GROUPOID : U = (A : U) * groupoid A + +fiber (A B : U) (f : A -> B) (y : B) : U = + (x : A) * Path B y (f x) + +isEquiv (A B : U) (f : A -> B) : U = (y : B) -> isContr (fiber A B f y) + +equiv (A B : U) : U = (f : A -> B) * isEquiv A B f + +-- This can be proved in many ways, not sure which is the most efficient +propIsContr (A : U) (z0 z1 : isContr A) : Path (isContr A) z0 z1 = + (p0 a1 @ j + ,\(x : A) -> hcomp 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) -> Path A a0 x = z0.2 + a1 : A = z1.1 + p1 : (x : A) -> Path A a1 x = z1.2 + lem1 (x : A) : PathP ( Path A a0 (p1 x @ i)) (p0 a1) (p0 x) = + p0 (p1 x @ i) @ j + +propSet (A : U) (h : prop A) : set A = + \(a b : A) (p q : Path A a b) -> + hcomp A a [ (i=0) -> h a a + , (i=1) -> h a b + , (j=0) -> h a (p @ i) + , (j=1) -> h a (q @ i)] + +setGroupoid (A : U) (h : set A) : groupoid A = + \(a b : A) -> propSet (Path A a b) (h a b) + +groupoidTwoGroupoid (A : U) (h : groupoid A) : twogroupoid A = + \(a b : A) -> setGroupoid (Path A a b) (h a b) + +twogroupoidThreeGroupoid (A : U) (h : twogroupoid A) : threegroupoid A = + \(a b : A) -> groupoidTwoGroupoid (Path A a b) (h a b) + +propIsProp (A : U) : prop (prop A) = + \(f g : prop A) -> \(a b : A) -> + propSet A f a b (f a b) (g a b) @ i + +setIsProp (A : U) : prop (set A) = + \(f g : set A) -> \(a b :A) -> + propIsProp (Path A a b) (f a b) (g a b) @ i + +groupoidIsProp (A : U) : prop (groupoid A) = + \(f g : groupoid A) -> \(a b :A) -> + setIsProp (Path A a b) (f a b) (g a b) @ i + +propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x)) + (f0 f1 : (x : A) -> B x) : Path ((x : A) -> B x) f0 f1 + = \ (x:A) -> (h x (f0 x) (f1 x)) @ i + +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 + +-- This opaque makes typechecking mu below faster, not sure if it breaks computation +-- opaque propIsEquiv + +lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 :A) + (p : Path A a0 a1) (b0 : P a0) (b1 : P a1) : PathP ( P (p @ i)) b0 b1 = + pP (p @ i) (comp ( P (p @ i/\ j)) b0 [ (i=0) -> <_> b0]) + (comp ( P (p @ i\/ -j)) b1 [ (i=1) -> <_> b1]) @ i + +lemSig (A : U) (B : A -> U) (pB : (x : A) -> prop (B x)) + (u v : (x:A) * B x) (p : Path A u.1 v.1) : + Path ((x:A) * B x) u v = (p @ i, lemPropF A B pB u.1 v.1 p u.2 v.2 @ i) + +equivEq (A B : U) (v w : equiv A B) (p : Path (A -> B) v.1 w.1) : Path (equiv A B) v w = + lemSig (A -> B) (isEquiv A B) (propIsEquiv A B) v w p + +contrSingl (A : U) (a b : A) (p : Path A a b) : + Path ((x : A) * Path A a x) (a,<_>a) (b,p) = (p @ i, p @ i/\j) + +idIsEquiv (A : U) : isEquiv A A (idfun A) = + \(a : A) -> ((a,<_>a) + ,\(z : fiber A A (idfun A) a) -> contrSingl A a z.1 z.2) + +idEquiv (A : U) : equiv A A = (idfun A,idIsEquiv A) + +-- Univalence map +ua (A B : U) (e : equiv A B) : Path U A B = + Glue B [ (i = 0) -> (A,e) + , (i = 1) -> (B,idEquiv B) ] +-- End of basics + -- B.8.1 The Hopf fibration +mu : S1 -> equiv S1 S1 = split + base -> idEquiv S1 + loop @ i -> + let f : (x : S1) -> Path S1 x x = split + base -> loopP + loop @ i -> constSquare S1 base loopP @ i + goal : Path (equiv S1 S1) (idEquiv S1) (idEquiv S1) = + equivEq S1 S1 (idEquiv S1) (idEquiv S1) ( \(x : S1) -> f x @ j) + in goal @ i + +Hopf : S2 -> U = split + north -> S1 + south -> S1 + merid x @ i -> ua S1 S1 (mu x) @ i + +-- Definition of the t map, this needs cleaning! + +subst (A : U) (P : A -> U) (a b : A) (p : Path A a b) (e : P a) : P b = + transGen ( P (p @ i)) 0 e + +substInv (A : U) (P : A -> U) (a b : A) (p : Path A a b) : P b -> P a = + subst A P b a ( p @ -i) + +J (A : U) (a : A) (C : (x : A) -> Path A a x -> U) + (d : C a (<_> a)) (x : A) (p : Path A a x) : C x p = + subst ((x : A) * Path A a x) T (a,<_> a) (x, p) (contrSingl A a x p) d + where T (z : (x : A) * Path A a x) : U = C (z.1) (z.2) + +PathS (A : U) (P : A -> U) (a0 a1 : A) (p : Path A a0 a1) (u0 : P a0) (u1 : P a1) : U = + PathP ( P (p @ i)) u0 u1 + +-- CLEAN THIS MESS! +-- TODO: is there a direct proof not involving J? +funExt1 (C B : U) (F : C -> U) (a : C) : (b : C) (p : Path C a b) + (f : F a -> B) (g : F b -> B) + (h : (x : F a) -> Path B (f x) (g (subst C F a b p x))) -> + PathP ( F (p @ i) -> B) f g = + let + rem (f g : F a -> B) (h : (x : F a) -> Path B (f x) (g x)) : Path (F a -> B) f g = + \(x:F a) -> h x @ i + P : (b:C) (p:Path C a b) -> U = \(b:C) (p:Path C a b) -> (f : F a -> B) (g : F b -> B) + (h : (x : F a) -> Path B (f x) (g (subst C F a b p x))) + -> PathP ( F (p @ i) -> B) f g + rem1 (f g : F a -> B) + (h : (x : F a) -> Path B (f x) (g (transGen (<_> F a) 0 x))) + : Path (F a -> B) f g = + let + moo : Path (F a -> B) f (\(x : F a) -> g (transGen (<_> F a) 0 x)) = + \(x : F a) -> h x @ i + boo' (x : F a) : Path (F a) x (hcomp (F a) (transGen (<_> F a) 0 x) []) = + fill (<_> F a) x [] + boo'' (x : F a) : Path (F a) (transGen (<_> F a) 0 x) (hcomp (F a) (transGen (<_> F a) 0 x) []) = hfill (F a) (transGen (<_> F a) 0 x) [] + boo''' (x : F a) : Path (F a) x (transGen (<_> F a) 0 x) = + compPath (F a) x (hcomp (F a) (transGen (<_> F a) 0 x) []) (transGen (<_> F a) 0 x) (boo' x) ( boo'' x @ -i) + boo (x : F a) : Path B (g x) (g (transGen (<_> F a) 0 x)) = + g (boo''' x @ i) + boof : Path (F a -> B) (\(x : F a) -> g (transGen (<_> F a) 0 x)) g = + \(x : F a) -> boo x @ -i + in compPath (F a -> B) f (\(x : F a) -> g (transGen (<_> F a) 0 x)) g moo boof + in J C a (\ (b:C) (p:Path C a b) -> (f : F a -> B) (g : F b -> B) + (h : (x : F a) -> Path B (f x) (g (subst C F a b p x))) + -> PathP ( F (p @ i) -> B) f g) rem1 + +t : (x : S2) -> (Hopf x -> join S1 S1) = split + north -> \(x : S1) -> inl x + south -> \(x : S1) -> inr x + merid x @ i -> + let eq (y : S1) : Path (join S1 S1) (inl y) (inr (subst S2 Hopf north south (meridP S1 x) y)) = + pushP S1 S1 y (subst S2 Hopf north south (meridP S1 x) y) + in funExt1 S2 (join S1 S1) Hopf north south (meridP S1 x) + (\(y : S1) -> inl y) (\(y : S1) -> inr y) eq @ i + +t' (xy : (x : S2) * Hopf x) : join S1 S1 = t xy.1 xy.2 + -- B.8.2 Looping a fibration +-- TODO: define all of these directly? (like for Omega2, Omega3..) +fibOmega (B : ptType) (P : B.1 -> U) (f : P (pt B)) (p : (Omega B).1) : U = + PathS B.1 P (pt B) (pt B) p f f + +itOmega : nat -> ptType -> ptType = split + zero -> \(A : ptType) -> A + suc n -> \(A : ptType) -> itOmega n (Omega A) + +itFibOmega : (n : nat) (B : ptType) (P : B.1 -> U) (f : P (pt B)) -> (itOmega n B).1 -> U = split + zero -> \(B : ptType) (P : B.1 -> U) (f : P (pt B)) -> P + suc n -> \(B : ptType) (P : B.1 -> U) (f : P (pt B)) -> + itFibOmega n (Omega B) (fibOmega B P f) (<_> f) + +itMapOmega : (n : nat) (A B : ptType) (h : ptMap A B) -> ptMap (itOmega n A) (itOmega n B) = split + zero -> \(A B : ptType) (h : ptMap A B) -> h + suc n -> \(A B : ptType) (h : ptMap A B) -> itMapOmega n (Omega A) (Omega B) (mapOmega A B h) + +totalFibOmega (B : ptType) (P : B.1 -> U) (f : P (pt B)) + (p : Sigma (Omega B).1 (fibOmega B P f)) : (Omega (Sigma B.1 P, (pt B, f))).1 = + (p.1 @ i,p.2 @ i) + +itTotalFibOmega : (n : nat) (B : ptType) (P : B.1 -> U) (f : P (pt B)) + (x : Sigma (itOmega n B).1 (itFibOmega n B P f)) -> (itOmega n (Sigma B.1 P, (pt B, f))).1 = split + zero -> \(B : ptType) (P : B.1 -> U) (f : P (pt B)) (x : Sigma B.1 P) -> x + suc n -> \(B : ptType) (P : B.1 -> U) (f : P (pt B)) + (x : Sigma (itOmega n (Omega B)).1 (itFibOmega n (Omega B) (fibOmega B P f) (<_> f))) -> + let BOm : ptType = Omega B + POm : BOm.1 -> U = fibOmega B P f + fOm : Path (P (pt B)) f f = <_> f + ih : (Sigma (itOmega n BOm).1 (itFibOmega n BOm POm fOm)) -> + (itOmega n (Sigma BOm.1 POm, (pt BOm, fOm))).1 = + itTotalFibOmega n (Omega B) (fibOmega B P f) fOm + in (itMapOmega n (Sigma BOm.1 POm, (pt BOm, fOm)) + (Omega (Sigma B.1 P, (pt B, f))) + (totalFibOmega B P f,<_ _> (pt B, f))).1 (ih x) + + + -- B.8.3 Looping the Hopf fibration +one : nat = suc zero +two : nat = suc one +three : nat = suc two + +HopfOne : (Omega S2pt).1 -> U = itFibOmega one S2pt Hopf base + +HopfTwo : (Omega2 S2pt).1 -> U = itFibOmega two S2pt Hopf base + +HopfThree : (Omega3 S2pt).1 -> U = itFibOmega three S2pt Hopf base + +inhOrTrunc (A : U) : nat -> U = split + zero -> A + suc n -> (x y : A) -> inhOrTrunc (Path A x y) n -h : ptMap (Omega3 S2pt) (Omega3 (joinpt S1pt S1)) = undefined +-- TODO: change to transGen +subst' (A : U) (P : A -> U) (a b : A) (p : Path A a b) (e : P a) : P b = + transport ( P (p @ i)) e +funDepTr (A : U) (P : A -> U) (a0 a1 : A) (p : Path A a0 a1) (u0 : P a0) (u1 : P a1) : + Path U (PathP ( P (p @ i)) u0 u1) + (Path (P a1) (subst' A P a0 a1 p u0) u1) = + PathP ( P (p @ j \/ i)) (comp ( P (p @ j /\ i)) u0 [ (j=0) -> <_> u0 ]) u1 +truncFibOmega (B : ptType) (P : B.1 -> U) (f : P (pt B)) (n : nat) + (tr : inhOrTrunc (P (pt B)) (suc n)) (p : (Omega B).1) : inhOrTrunc (fibOmega B P f p) n = + let trf : inhOrTrunc (Path (P B.2) (subst' B.1 P (pt B) (pt B) p f) f) n = + tr (subst' B.1 P (pt B) (pt B) p f) f + eq : Path U (Path (P (pt B)) (subst' B.1 P (pt B) (pt B) p f) f) + (PathP ( P (p @ i)) f f) = + funDepTr B.1 P (pt B) (pt B) p f f @ -i + in subst U (\(X : U) -> inhOrTrunc X n) + (Path (P (pt B)) (subst' B.1 P (pt B) (pt B) p f) f) + (PathP ( P (p @ i)) f f) + eq trf +------- +-- We now need that S1 is a groupoid + +-- I now do this by proving that loopS1 is a retract of Z, as Z is a +-- set this is also set. Previously the proof transported the proof +-- that Z is a set to loopS1 along the equivalence loopS1 ~= Z, +-- hopefully this proof will compute faster. + +retract (A B : U) (f : A -> B) (g : B -> A) : U = + (a : A) -> Path A (g (f a)) a + +compUp (A : U) (a a' b b' : A) (p : Path A a a') (q : Path A b b') + (r : Path A a b) : Path A a' b' = + hcomp A (r @ i) [(i = 0) -> p, (i = 1) -> q] + +lemRetract (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) + (x y : A) : Path A (g (f x)) (g (f y)) -> Path A x y = + compUp A (g (f x)) x (g (f y)) y (rfg x) (rfg y) + +retractProp (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) + (pB : prop B) (x y : A) : Path A x y = + lemRetract A B f g rfg x y ( g (pB (f x) (f y) @ i)) + +retractInv (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) + (x y : A) (q : Path B (f x) (f y)) : Path A x y = + hcomp A (g (q @ i)) [(i = 0) -> rfg x, (i = 1) -> rfg y] + +lemRSquare (A B : U) (f : A -> B) (g : B -> A) + (rfg : (a : A) -> Path A (g (f a)) a) + (x y : A) (p : Path A x y) : + Square A (g (f x)) (g (f y)) x y + ( g (f (p @ i))) + ( hcomp A (g (f (p @ i))) [(i = 0) -> rfg x, (i = 1) -> rfg y]) + (rfg x) + (rfg y) = + hcomp A (g (f (p @ i))) [ (i = 0) -> rfg x @ j /\ k + , (i = 1) -> rfg y @ j /\ k + , (j = 0) -> g (f (p @ i)) ] + +retractPath (A B : U)(f : A -> B) (g : B -> A) (rfg : retract A B f g) (x y :A) (p:Path A x y) : + Path (Path A x y) (retractInv A B f g rfg x y ( f (p@ i))) p = + hcomp A (g (f (p @ j))) + [ (j=0) -> rfg x + , (j=1) -> rfg y + , (i=0) -> lemRSquare A B f g rfg x y p @ j + , (i=1) -> rfg (p @ j) ] + + +retractSet (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) + (sB : set B) (x y : A) : prop (Path A x y) = + retractProp (Path A x y) (Path B (f x) (f y)) (\(p : Path A x y) -> f (p @ i)) + (retractInv A B f g rfg x y) (retractPath A B f g rfg x y) (sB (f x) (f y)) + +-- This not needed! +-- loopS1equalsZ : Path U loopS1 Z = +-- isoPath loopS1 Z (encode base) (decode base) decodeEncodeBase (encodeDecode base) + +-- Z is a set +data N0 = + +efq (A : U) : N0 -> A = split {} +not (A : U) : U = A -> N0 + +data or (A B : U) = inl (a : A) + | inr (b : B) + +data Unit = tt + +stable (A : U) : U = not (not A) -> A +const (A : U) (f : A -> A) : U = (x y : A) -> Path A (f x) (f y) + +exConst (A : U) : U = (f:A -> A) * const A f +propN0 : prop N0 = \ (x y:N0) -> efq (Path N0 x y) x + +propNot (A : U) : prop (not A) = \ (f g:not A) -> \(x:A) -> (propN0 (f x) (g x))@i + +dNot (A : U) (a : A) : not (not A) = \ (h : not A) -> h a + +stableConst (A : U) (sA : stable A) : exConst A = + (\ (x:A) -> sA (dNot A x),\ (x y:A) -> sA (propNot (not A) (dNot A x) (dNot A y) @ i)) + +dec (A : U) : U = or A (not A) + +decEqCong (A B : U) (f : A -> B) (g : B -> A) : dec A -> dec B = split + inl a -> inl (f a) + inr h -> inr (\ (b:B) -> h (g b)) + +decStable (A : U) : dec A -> stable A = split + inl a -> \ (h :not (not A)) -> a + inr b -> \ (h :not (not A)) -> efq A (h b) + +discrete (A : U) : U = (a b : A) -> dec (Path A a b) + +hedbergLemma (A: U) (a b:A) (f : (x : A) -> Path A a x -> Path A a x) (p : Path A a b) : + Square A a a a b (<_> a) p (f a (<_> a)) (f b p) = + comp ( Square A a a a (p @ i) (<_> a) ( p @ i /\ j) + (f a (<_> a)) (f (p @ i) ( p @ i /\ j))) + ( f a (<_> a)) [] + +hedbergStable (A : U) (a b : A) (h : (x : A) -> stable (Path A a x)) + (p q : Path A a b) : Path (Path A a b) p q = + comp (<_> A) a [ (j = 0) -> rem2 @ i + , (j = 1) -> rem3 @ i + , (i = 0) -> r + , (i = 1) -> rem4 @ j] + where + rem1 (x : A) : exConst (Path A a x) = stableConst (Path A a x) (h x) + f (x : A) : Path A a x -> Path A a x = (rem1 x).1 + fIsConst (x : A) : const (Path A a x) (f x) = (rem1 x).2 + rem4 : Square A a a b b (<_> a) (<_> b) (f b p) (f b q) = fIsConst b p q + r : Path A a a = f a (<_> a) + rem2 : Square A a a a b (<_> a) p r (f b p) = hedbergLemma A a b f p + rem3 : Square A a a a b (<_> a) q r (f b q) = hedbergLemma A a b f q + +hedbergS (A : U) (h : (a x : A) -> stable (Path A a x)) : set A = + \(a b : A) -> hedbergStable A a b (h a) + +hedberg (A : U) (h : discrete A) : set A = + \(a b : A) -> hedbergStable A a b (\(b : A) -> decStable (Path A a b) (h a b)) + +caseNat (A : U) (a0 aS : A) : nat -> A = split + zero -> a0 + suc n -> aS + +caseDNat (P:nat -> U) (a0 :P zero) (aS : (n:nat) -> P (suc n)) + : (n:nat) -> P n = split + zero -> a0 + suc n -> aS n + +znots (n : nat) : not (Path nat zero (suc n)) = + \(h : Path nat zero (suc n)) -> subst nat (caseNat U nat N0) zero (suc n) h zero + +snotz (n : nat) : not (Path nat (suc n) zero) = + \(h : Path nat (suc n) zero) -> znots n ( h @ -i) + +pred : nat -> nat = split + zero -> zero + suc n -> n + +sucInj (n m : nat) (p : Path nat (suc n) (suc m)) : Path nat n m = + pred (p @ i) + +discreteNat : discrete nat = split + zero -> caseDNat (\(m : nat) -> dec (Path nat zero m)) (inl (<_> zero)) (\(m : nat) -> inr (znots m)) + suc n -> caseDNat (\(m : nat) -> dec (Path nat (suc n) m)) (inr (snotz n)) + (\(m : nat) -> decEqCong (Path nat n m) (Path nat (suc n) (suc m)) (\(p : Path nat n m) -> suc (p @ i)) + (sucInj n m) (discreteNat n m)) + +posNotneg (a b : nat) (h : Path Z (pos a) (neg b)) : N0 = subst Z T (pos a) (neg b) h tt + where + T : Z -> U = split + pos _ -> Unit + neg _ -> N0 + +negNotpos (a b : nat) (h : Path Z (neg b) (pos a)) : N0 = subst Z T (neg b) (pos a) h tt + where + T : Z -> U = split + pos _ -> N0 + neg _ -> Unit + +injPos (a b : nat) (h : Path Z (pos a) (pos b)) : Path nat a b = + subst Z T (pos a) (pos b) h (<_> a) + where + T : Z -> U = split + pos c -> Path nat a c + neg _ -> N0 + +injNeg (a b : nat) (h : Path Z (neg a) (neg b)) : Path nat a b = + subst Z T (neg a) (neg b) h (<_> a) + where + T : Z -> U = split + pos _ -> N0 + neg c -> Path nat a c + +discreteZ : discrete Z = split + pos a -> split@((z1 : Z) -> dec (Path Z (pos a) z1)) with + pos a1 -> let rem : dec (Path nat a a1) -> dec (Path Z (pos a) (pos a1)) = split + inl p -> inl ( pos (p @ i)) + inr h -> inr (\(p : Path Z (pos a) (pos a1)) -> h (injPos a a1 p)) + in rem (discreteNat a a1) + neg b -> inr (posNotneg a b) + neg b -> split@((z1 : Z) -> dec (Path Z (neg b) z1)) with + pos a -> inr (negNotpos a b) + neg b1 -> let rem : dec (Path nat b b1) -> dec (Path Z (neg b) (neg b1)) = split + inl p -> inl ( neg (p @ i)) + inr h -> inr (\(p : Path Z (neg b) (neg b1)) -> h (injNeg b b1 p)) + in rem (discreteNat b b1) + + +ZSet : set Z = hedberg Z discreteZ +-- + +-- No need for substituting in the universe here +-- setLoop : set loopS1 = subst U set Z loopS1 ( loopS1equalsZ @ -i) ZSet + +predZ : Z -> Z = split + pos u -> auxpredZ u + where + auxpredZ : nat -> Z = split + zero -> neg zero + suc n -> pos n + neg v -> neg (suc v) + +sucZ : Z -> Z = split + pos u -> pos (suc u) + neg v -> auxsucZ v + where + auxsucZ : nat -> Z = split + zero -> pos zero + suc n -> neg n + +predsucZ : (x : Z) -> Path Z (predZ (sucZ x)) x = split + pos u -> <_> pos u + neg v -> lem v + where + lem : (u : nat) -> Path Z (predZ (sucZ (neg u))) (neg u) = split + zero -> <_> neg zero + suc n -> <_> neg (suc n) + +sucpredZ : (x : Z) -> Path Z (sucZ (predZ x)) x = split + pos u -> lem u + where + lem : (u : nat) -> Path Z (sucZ (predZ (pos u))) (pos u) = split + zero -> <_> pos zero + suc n -> <_> pos (suc n) + neg v -> <_> neg v + +lemIso (A B : U) (f : A -> B) (g : B -> A) + (s : (y : B) -> Path B (f (g y)) y) + (t : (x : A) -> Path A (g (f x)) x) + (y : B) (x0 x1 : A) (p0 : Path B y (f x0)) (p1 : Path B y (f x1)) : + Path (fiber A B f y) (x0,p0) (x1,p1) = (p @ i,sq1 @ i) + where + rem0 : Path A (g y) x0 = + hcomp A (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> g y ] + + rem1 : Path A (g y) x1 = + hcomp A (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> g y ] + + p : Path A x0 x1 = + hcomp A (g y) [ (i = 0) -> rem0 + , (i = 1) -> rem1 ] + + fill0 : Square A (g y) (g (f x0)) (g y) x0 + ( g (p0 @ i)) rem0 ( g y) (t x0) = + hcomp A (g (p0 @ i)) [ (i = 1) -> t x0 @ j /\ k + , (i = 0) -> g y + , (j = 0) -> g (p0 @ i) ] + + fill1 : Square A (g y) (g (f x1)) (g y) x1 + ( g (p1 @ i)) rem1 ( g y) (t x1) = + hcomp A (g (p1 @ i)) [ (i = 1) -> t x1 @ j /\ k + , (i = 0) -> g y + , (j = 0) -> g (p1 @ i) ] + + fill2 : Square A (g y) (g y) x0 x1 + ( g y) p rem0 rem1 = + hcomp A (g y) [ (i = 0) -> rem0 @ j /\ k + , (i = 1) -> rem1 @ j /\ k + , (j = 0) -> g y ] + + sq : Square A (g y) (g y) (g (f x0)) (g (f x1)) + ( g y) ( g (f (p @ i))) + ( g (p0 @ j)) ( g (p1 @ j)) = + hcomp A (fill2 @ i @ j) [ (i = 0) -> fill0 @ j @ -k + , (i = 1) -> fill1 @ j @ -k + , (j = 0) -> g y + , (j = 1) -> t (p @ i) @ -k ] + + sq1 : Square B y y (f x0) (f x1) + (y) ( f (p @ i)) p0 p1 = + hcomp B (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j) + , (i = 1) -> s (p1 @ j) + , (j = 1) -> s (f (p @ i)) + , (j = 0) -> s y ] + +gradLemma (A B : U) (f : A -> B) (g : B -> A) + (s : (y : B) -> Path B (f (g y)) y) + (t : (x : A) -> Path A (g (f x)) x) : isEquiv A B f = + \(y:B) -> ((g y,s y@-i),\ (z:fiber A B f y) -> + lemIso A B f g s t y (g y) z.1 (s y@-i) z.2) + +isoPath (A B : U) (f : A -> B) (g : B -> A) + (s : (y : B) -> Path B (f (g y)) y) + (t : (x : A) -> Path A (g (f x)) x) : Path U A B = + Glue B [ (i = 0) -> (A,f,gradLemma A B f g s t) + , (i = 1) -> (B,idfun B,idIsEquiv B) ] + +sucPathZ : Path U Z Z = isoPath Z Z sucZ predZ sucpredZ predsucZ + +helix : S1 -> U = split + base -> Z + loop @ i -> sucPathZ @ i + +encode (x : S1) (p : Path S1 base x) : helix x = subst S1 helix base x p zeroZ + + +lem1ItPos : (n:nat) -> Path loopS1 (loopIt (sucZ (pos n))) (oneTurn ((loopIt (pos n)))) = split + zero -> refl loopS1 (oneTurn (<_> base)) + suc p -> oneTurn (lem1ItPos p@i) + +-- todo: clean +compInv (A:U) (a:A) : (x:A) (p:Path A a x) -> Path (Path A x x) (<_>x) (compPath A x a x (p@-i) p) = + J A a (\ (x:A) (p:Path A a x) -> Path (Path A x x) (<_>x) (compPath A x a x (p@-i) p)) rem + where rem : Path (Path A a a) (<_>a) (hcomp A a [(i=0) -> <_>a,(i=1) -> <_>a]) = + hcomp A a [(j=0) -> <_>a,(i=0) -> <_>a,(i=1) -> <_>a] + +compInvS1 : Path loopS1 (refl S1 base) (compS1 invLoop loopP) = compInv S1 base base loopP + +-- todo: why this one with the same name? clean! +compInv (A:U) (a b:A) (q:Path A a b) : (x:A) (p:Path A b x) -> Path (Path A a b) q (compPath A a x b (compPath A a b x q p) (p@-i)) = + J A b (\ (x:A) (p:Path A b x) -> Path (Path A a b) q (compPath A a x b (compPath A a b x q p) (p@-i))) rem + where rem : Path (Path A a b) q + (hcomp A (hcomp A (q@i) [(i=0) -> <_>a,(i=1) -> <_>b]) [(i=0) -> <_>a,(i=1) -> <_>b]) = + hcomp A (hcomp A (q@i) [(j=0) -> <_>q@i,(i=0) -> <_>a,(i=1) -> <_>b]) [(j=0) -> <_>q@i,(i=0) -> <_>a,(i=1) -> <_>b] + +lem1ItNeg : (n:nat) -> Path loopS1 (loopIt (sucZ (neg n))) (oneTurn (loopIt (neg n))) = split + zero -> compInvS1 + suc p -> compInv S1 base base (loopIt (neg p)) base invLoop + +lem1It : (n:Z) -> Path loopS1 (loopIt (sucZ n)) (oneTurn (loopIt n)) = split + pos n -> lem1ItPos n + neg n -> lem1ItNeg n + +-- todo: this should be used above! +transGen0 (A : U) (a : A) : A = transGen (<_> A) 0 a + +lemTransGen0 (A : U) (a : A) : Path A (transGen0 A a) a = + -- let rem1 : Path A a (hcomp A (transGen (<_> A) 0 a) []) = fill (<_> A) a [] + -- rem2 : Path A (transGen (<_> A) 0 a) (hcomp A (transGen (<_> A) 0 a) []) = + -- hfill A (transGen (<_> A) 0 a) [] + -- in compPath A (transGen0 A a) (hcomp A (transGen (<_> A) 0 a) []) a rem2 ( rem1 @ -i) + hcomp A (hfill A (transGen (<_> A) 0 a) [] @ i) + [ (i = 0) -> <_> transGen0 A a + , (i = 1) -> fill (<_> A) a [] @ -j ] + +lemFib1 (A:U) (F G : A -> U) (a:A) (fa : F a -> G a) : + (x:A) (p : Path A a x) -> (fx : F x -> G x) -> + Path U (Path (F a -> G x) (\(u : F a) -> subst A G a x p (fa u)) + (\(u : F a) -> fx (subst A F a x p u))) + (PathP ( F (p @ i) -> G (p @ i)) fa fx) = + J A a (\(x : A) (p : Path A a x) -> (fx : F x -> G x) -> + Path U (Path (F a -> G x) (\(u : F a) -> subst A G a x p (fa u)) + (\(u : F a) -> fx (subst A F a x p u))) + (PathP (F (p@i) -> G (p@i)) fa fx)) rem + where + rem (ga : F a -> G a) : + Path U (Path (F a -> G a) (\(u : F a) -> transGen (<_> G a) 0 (fa u)) + (\(u : F a) -> ga (transGen (<_> F a) 0 u))) + (PathP (<_> F a -> G a) fa ga) = + Path (F a -> G a) (\(u : F a) -> lemTransGen0 (G a) (fa u) @ j) + (\(u : F a) -> ga (lemTransGen0 (F a) u @ j)) + +corFib1 (A:U) (F G : A -> U) (a:A) (fa ga : F a -> G a) (p:Path A a a) + (h : (u:F a) -> Path (G a) (subst A G a a p (fa u)) (ga (subst A F a a p u))) : + PathP ( F (p @ i) -> G (p @ i)) fa ga = + comp (lemFib1 A F G a fa a p ga) ( \(u : F a) -> h u @ i) [] + +testHelix : Path (Z->Z) sucZ (subst S1 helix base base loopP) = + let rem (x : Z) : Path Z (sucZ x) (hcomp Z (hcomp Z (transGen ( Z) 0 (sucZ x)) []) []) = + compPath Z (sucZ x) + (hcomp Z (transGen ( Z) 0 (sucZ x)) []) + (hcomp Z (hcomp Z (transGen ( Z) 0 (sucZ x)) []) []) + (fill (<_> Z) (sucZ x) []) + (hfill Z (hcomp Z (transGen ( Z) 0 (sucZ x)) []) []) + in \(x : Z) -> rem x @ i + +decode : (x:S1) -> helix x -> Path S1 base x = split + base -> loopIt + loop @ i -> rem @ i + where + T : U = Z -> loopS1 + G (x:S1) : U = Path S1 base x + p : Path U T T = helix (loopP @ j) -> Path S1 base (loopP@j) + rem2 (x:Z) : + Path loopS1 (oneTurn (loopIt x)) + (loopIt (sucZ x)) = lem1It x @ -i + rem4 (x : Z) : Path (Path S1 base base) + ( hcomp S1 (transGen0 S1 (loopIt x @ i)) + [ (i = 0) -> <_> base + , (i = 1) -> loopP ]) + ( hcomp S1 (loopIt x @ i) + [ (i = 0) -> <_> base + , (i = 1) -> loopP ]) = hcomp S1 (transGen (<_> S1) j (loopIt x @ i)) [ (i = 0) -> <_> base, (i = 1) -> loopP ] + rem3 (x : Z) : + Path loopS1 (subst S1 G base base loopP (loopIt x)) + (loopIt (sucZ x)) = + compPath loopS1 (subst S1 G base base loopP (loopIt x)) + (oneTurn (loopIt x)) (loopIt (sucZ x)) + (rem4 x) (rem2 x) + rem1 (x:Z) : Path loopS1 (subst S1 G base base loopP (loopIt x)) + (loopIt (subst S1 helix base base loopP x)) = + comp ( Path loopS1 (subst S1 G base base loopP (loopIt x)) + (loopIt (testHelix @ i x))) (rem3 x) [] + rem : PathP p loopIt loopIt = corFib1 S1 helix G base loopIt loopIt loopP rem1 + +encodeDecode (x : S1) (p : Path S1 base x) : Path (Path S1 base x) (decode x (encode x p)) p = + transport ( Path (Path S1 base (p @ i)) + (decode (p @ i) (encode (p @ i) ( p @ i /\ j))) ( p @ i /\ j)) + (<_> triv) + +setLoop : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (encodeDecode base) ZSet + + +lemPropFib (P : S1 -> U) (pP : (x : S1) -> prop (P x)) (bP : P base) : (x : S1) -> P x = split + base -> bP + loop @ i -> lemPropF S1 P pP base base loopP bP bP @ i + +isGroupoidS1 : groupoid S1 = lem + where + lem2 : (y : S1) -> set (Path S1 base y) + = lemPropFib (\(y : S1) -> set (Path S1 base y)) (\(y : S1) -> setIsProp (Path S1 base y)) setLoop + + lem : (x y : S1) -> set (Path S1 x y) + = lemPropFib (\(x : S1) -> (y : S1) -> set (Path S1 x y)) pP lem2 + where + pP (x : S1) : prop ((y : S1) -> set (Path S1 x y)) = + propPi S1 (\(y : S1) -> set (Path S1 x y)) (\(y : S1) -> setIsProp (Path S1 x y)) + +fibContrHopfThree (p : (Omega3 S2pt).1) : HopfThree p = + truncFibOmega (Omega2 S2pt) HopfTwo (<_ _> base) zero + (truncFibOmega (Omega S2pt) HopfOne (<_> base) one + (truncFibOmega S2pt Hopf base two isGroupoidS1 (<_> north)) + (<_> pt (Omega S2pt))) p + +-- The map h from 9.3 +h (p : (Omega3 S2pt).1) : (Omega3 (joinpt S1pt S1)).1 = + mapOmegaRefl3 (Sigma S2 Hopf, (north,base)) (join S1 S1) t' + (itTotalFibOmega three S2pt Hopf base (p, fibContrHopfThree p)) + + +-------------------------------------------------------------------------------- +-- B.9 Going back to pi2(S2) + +-- B.9.1 Truncations + +-- 2-Groupoid truncation +data g2Trunc (A : U) = + g2inc (a : A) + | g2squashC (a b : g2Trunc A) + (p q : Path (g2Trunc A) a b) + (r s : Path (Path (g2Trunc A) a b) p q) + (t u : Path (Path (Path (g2Trunc A) a b) p q) r s) + + [ (i=0) -> t @ j @ k @ l + , (i=1) -> u @ j @ k @ l + , (j=0) -> r @ k @ l + , (j=1) -> s @ k @ l + , (k=0) -> p @ l + , (k=1) -> q @ l + , (l=0) -> a + , (l=1) -> b ] + +g2Truncpt (A : ptType) : ptType = (g2Trunc A.1,g2inc (pt A)) + +g2TruncRec (A B : U) (bG : twogroupoid B) (f : A -> B) : g2Trunc A -> B = split + g2inc a -> f a + g2squashC a b p q r s t u @ i j k l -> + bG (g2TruncRec A B bG f a) + (g2TruncRec A B bG f b) + ( g2TruncRec A B bG f (p @ m)) + ( g2TruncRec A B bG f (q @ m)) + ( g2TruncRec A B bG f (r @ m @ n)) + ( g2TruncRec A B bG f (s @ m @ n)) + ( g2TruncRec A B bG f (t @ m @ n @ o)) + ( g2TruncRec A B bG f (u @ m @ n @ o)) + @ i @ j @ k @ l + +g2TruncTwoGroupoid (A : U) : twogroupoid (g2Trunc A) = + \(a b : g2Trunc A) (p q : Path (g2Trunc A) a b) + (r s : Path (Path (g2Trunc A) a b) p q) + (t u : Path (Path (Path (g2Trunc A) a b) p q) r s) -> + g2squashC{g2Trunc A} a b p q r s t u @ i @ j @ k @ l + +-- We now prove the eliminator for 2-groupoid truncation. This would +-- be a lot nicer in a proper proof assistant... + +lem0 (A : U) (P : A -> U) (gP : (x : A) -> twogroupoid (P x)) (a : A) : + (u : Path (Path (Path A a a) (<_> a) (<_> a)) (<_ _> a) (<_ _> a)) + (v : Path (Path (Path (Path A a a) (<_> a) (<_> a)) (<_ _> a) (<_ _> a)) (<_ _ _> a) u) + (a1 b1 : P a) + (p1 q1 : Path (P a) a1 b1) + (r1 s1 : Path (Path (P a) a1 b1) p1 q1) + (t1 : Path (Path (Path (P a) a1 b1) p1 q1) r1 s1) + (u1 : PathP ( PathP ( PathP ( P (u @ i @ j @ k)) a1 b1) p1 q1) r1 s1) -> + PathP ( PathP ( PathP ( PathP ( P (v @ i @ j @ k @ l)) a1 b1) p1 q1) r1 s1) t1 u1 = + J (Path (Path (Path A a a) (<_> a) (<_> a)) (<_ _> a) (<_ _> a)) (<_ _ _> a) + (\(u : Path (Path (Path A a a) (<_> a) (<_> a)) (<_ _> a) (<_ _> a)) + (v : Path (Path (Path (Path A a a) (<_> a) (<_> a)) (<_ _> a) (<_ _> a)) (<_ _ _> a) u) -> + (a1 b1 : P a) + (p1 q1 : Path (P a) a1 b1) + (r1 s1 : Path (Path (P a) a1 b1) p1 q1) + (t1 : Path (Path (Path (P a) a1 b1) p1 q1) r1 s1) + (u1 : PathP ( PathP ( PathP ( P (u @ i @ j @ k)) a1 b1) p1 q1) r1 s1) -> + PathP ( PathP ( PathP ( PathP ( P (v @ i @ j @ k @ l)) a1 b1) p1 q1) r1 s1) t1 u1) + (gP a) + +lem1 (A : U) (P : A -> U) (gP : (x : A) -> twogroupoid (P x)) (a : A) : + (s : Path (Path A a a) (<_> a) (<_> a)) + (t u : Path (Path (Path A a a) (<_> a) (<_> a)) (<_ _> a) s) + (v : Path (Path (Path (Path A a a) (<_> a) (<_> a)) (<_ _> a) s) t u) + (a1 b1 : P a) + (p1 q1 : Path (P a) a1 b1) + (r1 : Path (Path (P a) a1 b1) p1 q1) + (s1 : PathP ( PathP ( P (s @ i @ j)) a1 b1) p1 q1) + (t1 : PathP ( PathP ( PathP ( P (t @ i @ j @ k)) a1 b1) p1 q1) r1 s1) + (u1 : PathP ( PathP ( PathP ( P (u @ i @ j @ k)) a1 b1) p1 q1) r1 s1) -> + PathP ( PathP ( PathP ( PathP ( P (v @ i @ j @ k @ l)) a1 b1) p1 q1) r1 s1) t1 u1 = + J (Path (Path A a a) (<_> a) (<_> a)) (<_ _> a) + (\(s : Path (Path A a a) (<_> a) (<_> a)) + (t : Path (Path (Path A a a) (<_> a) (<_> a)) (<_ _> a) s) -> + (u : Path (Path (Path A a a) (<_> a) (<_> a)) (<_ _> a) s) + (v : Path (Path (Path (Path A a a) (<_> a) (<_> a)) (<_ _> a) s) t u) + (a1 b1 : P a) + (p1 q1 : Path (P a) a1 b1) + (r1 : Path (Path (P a) a1 b1) p1 q1) + (s1 : PathP ( PathP ( P (s @ i @ j)) a1 b1) p1 q1) + (t1 : PathP ( PathP ( PathP ( P (t @ i @ j @ k)) a1 b1) p1 q1) r1 s1) + (u1 : PathP ( PathP ( PathP ( P (u @ i @ j @ k)) a1 b1) p1 q1) r1 s1) -> + PathP ( PathP ( PathP ( PathP ( P (v @ i @ j @ k @ l)) a1 b1) p1 q1) r1 s1) t1 u1) + (lem0 A P gP a) + +lem2 (A : U) (P : A -> U) (gP : (x : A) -> twogroupoid (P x)) (a : A) : + (q : Path A a a) (r s : Path (Path A a a) (<_> a) q) + (t u : Path (Path (Path A a a) (<_> a) q) r s) + (v : Path (Path (Path (Path A a a) (<_> a) q) r s) t u) + (a1 : P a) (b1 : P a) + (p1 : Path (P a) a1 b1) + (q1 : PathP ( P (q @ i)) a1 b1) + (r1 : PathP ( PathP ( P (r @ i @ j)) a1 b1) p1 q1) + (s1 : PathP ( PathP ( P (s @ i @ j)) a1 b1) p1 q1) + (t1 : PathP ( PathP ( PathP ( P (t @ i @ j @ k)) a1 b1) p1 q1) r1 s1) + (u1 : PathP ( PathP ( PathP ( P (u @ i @ j @ k)) a1 b1) p1 q1) r1 s1) -> + PathP ( PathP ( PathP ( PathP ( P (v @ i @ j @ k @ l)) a1 b1) p1 q1) r1 s1) t1 u1 = + J (Path A a a) (<_> a) (\(q : Path A a a) (r : Path (Path A a a) (<_> a) q) -> + (s : Path (Path A a a) (<_> a) q) + (t u : Path (Path (Path A a a) (<_> a) q) r s) + (v : Path (Path (Path (Path A a a) (<_> a) q) r s) t u) + (a1 b1 : P a) + (p1 : Path (P a) a1 b1) + (q1 : PathP ( P (q @ i)) a1 b1) + (r1 : PathP ( PathP ( P (r @ i @ j)) a1 b1) p1 q1) + (s1 : PathP ( PathP ( P (s @ i @ j)) a1 b1) p1 q1) + (t1 : PathP ( PathP ( PathP ( P (t @ i @ j @ k)) a1 b1) p1 q1) r1 s1) + (u1 : PathP ( PathP ( PathP ( P (u @ i @ j @ k)) a1 b1) p1 q1) r1 s1) -> + PathP ( PathP ( PathP ( PathP ( P (v @ i @ j @ k @ l)) a1 b1) p1 q1) r1 s1) t1 u1) (lem1 A P gP a) + +lem (A : U) (P : A -> U) (gP : (x : A) -> twogroupoid (P x)) (a : A) : + (b : A) (p q : Path A a b) + (r s : Path (Path A a b) p q) + (t u : Path (Path (Path A a b) p q) r s) + (v : Path (Path (Path (Path A a b) p q) r s) t u) + (a1 : P a) (b1 : P b) + (p1 : PathP ( P (p @ i)) a1 b1) + (q1 : PathP ( P (q @ i)) a1 b1) + (r1 : PathP ( PathP ( P (r @ i @ j)) a1 b1) p1 q1) + (s1 : PathP ( PathP ( P (s @ i @ j)) a1 b1) p1 q1) + (t1 : PathP ( PathP ( PathP ( P (t @ i @ j @ k)) a1 b1) p1 q1) r1 s1) + (u1 : PathP ( PathP ( PathP ( P (u @ i @ j @ k)) a1 b1) p1 q1) r1 s1) -> + PathP ( PathP ( PathP ( PathP ( P (v @ i @ j @ k @ l)) a1 b1) p1 q1) r1 s1) t1 u1 = + J A a (\(b : A) (p : Path A a b) -> (q : Path A a b) + (r s : Path (Path A a b) p q) + (t u : Path (Path (Path A a b) p q) r s) + (v : Path (Path (Path (Path A a b) p q) r s) t u) + (a1 : P a) (b1 : P b) + (p1 : PathP ( P (p @ i)) a1 b1) + (q1 : PathP ( P (q @ i)) a1 b1) + (r1 : PathP ( PathP ( P (r @ i @ j)) a1 b1) p1 q1) + (s1 : PathP ( PathP ( P (s @ i @ j)) a1 b1) p1 q1) + (t1 : PathP ( PathP ( PathP ( P (t @ i @ j @ k)) a1 b1) p1 q1) r1 s1) + (u1 : PathP ( PathP ( PathP ( P (u @ i @ j @ k)) a1 b1) p1 q1) r1 s1) -> + PathP ( PathP ( PathP ( PathP ( P (v @ i @ j @ k @ l)) a1 b1) p1 q1) r1 s1) t1 u1) + (lem2 A P gP a) + +T : U = (A : U) (P : A -> U) (gP : (x : A) -> twogroupoid (P x)) + (a b : A) + (p q : Path A a b) + (r s : Path (Path A a b) p q) + (t u : Path (Path (Path A a b) p q) r s) + (v : Path (Path (Path (Path A a b) p q) r s) t u) + (a1 : P a) (b1 : P b) + (p1 : PathP ( P (p @ i)) a1 b1) + (q1 : PathP ( P (q @ i)) a1 b1) + (r1 : PathP ( PathP ( P (r @ i @ j)) a1 b1) p1 q1) + (s1 : PathP ( PathP ( P (s @ i @ j)) a1 b1) p1 q1) + (t1 : PathP ( PathP ( PathP ( P (t @ i @ j @ k)) a1 b1) p1 q1) r1 s1) + (u1 : PathP ( PathP ( PathP ( P (u @ i @ j @ k)) a1 b1) p1 q1) r1 s1) -> + PathP ( PathP ( PathP ( PathP ( P (v @ i @ j @ k @ l)) a1 b1) p1 q1) r1 s1) t1 u1 + +g2TruncElim1 (P : T) (A : U) (B : (g2Trunc A) -> U) + (bG : (x : g2Trunc A) -> twogroupoid (B x)) + (f : (x : A) -> B (g2inc x)) : (x : g2Trunc A) -> B x = split + g2inc a -> f a + g2squashC a b p q r s t u @ i j k l -> + P (g2Trunc A) B bG a b p q r s t u + (g2TruncTwoGroupoid A a b p q r s t u) + (g2TruncElim1 P A B bG f a) + (g2TruncElim1 P A B bG f b) + ( g2TruncElim1 P A B bG f (p @ m)) + ( g2TruncElim1 P A B bG f (q @ m)) + ( g2TruncElim1 P A B bG f (r @ m @ n)) + ( g2TruncElim1 P A B bG f (s @ m @ n)) + ( g2TruncElim1 P A B bG f (t @ m @ n @ o)) + ( g2TruncElim1 P A B bG f (u @ m @ n @ o)) @ i @ j @ k @ l + +g2TruncElim : (A : U) + (B : (g2Trunc A) -> U) + (bG : (x : g2Trunc A) -> twogroupoid (B x)) + (f : (x : A) -> B (g2inc x)) (x : g2Trunc A) -> B x = g2TruncElim1 lem + + +-- Groupoid truncation +data gTrunc (A : U) = + ginc (a : A) + | gsquashC (a b : gTrunc A) (p q : Path (gTrunc A) a b) + (r s : Path (Path (gTrunc A) a b) p q) + [ (i=0) -> r @ j @ k + , (i=1) -> s @ j @ k + , (j=0) -> p @ k + , (j=1) -> q @ k + , (k=0) -> a + , (k=1) -> b ] + +gTruncpt (A : ptType) : ptType = (gTrunc A.1,ginc (pt A)) + +gTruncRec (A B : U) (bG : groupoid B) (f : A -> B) : gTrunc A -> B = split + ginc a -> f a + gsquashC a b p q r s @ i j k -> + bG (gTruncRec A B bG f a) + (gTruncRec A B bG f b) + ( gTruncRec A B bG f (p @ m)) + ( gTruncRec A B bG f (q @ m)) + ( gTruncRec A B bG f (r @ m @ n)) + ( gTruncRec A B bG f (s @ m @ n)) @ i @ j @ k + +gTruncGroupoid (A : U) : groupoid (gTrunc A) = + \(a b : gTrunc A) (p q : Path (gTrunc A) a b) (r s : Path (Path (gTrunc A) a b) p q) -> + gsquashC{gTrunc A} a b p q r s @ i @ j @ k + +-- Set truncation +data sTrunc (A : U) = + sinc (a : A) + | ssquashC (a b : sTrunc A) (p q : Path (sTrunc A) a b) + [ (i=0) -> p @ j + , (i=1) -> q @ j + , (j=0) -> a + , (j=1) -> b ] + +sTruncpt (A : ptType) : ptType = (sTrunc A.1,sinc (pt A)) + +sTruncRec (A B : U) (bS : set B) (f : A -> B) : sTrunc A -> B = split + sinc a -> f a + ssquashC a b p q @ i j -> (bS (sTruncRec A B bS f a) + (sTruncRec A B bS f b) + ( sTruncRec A B bS f (p @ k)) + ( sTruncRec A B bS f (q @ k))) @ i @ j + +setTruncSet (A : U) : set (sTrunc A) = + \(a b : sTrunc A) (p q : Path (sTrunc A) a b) -> + ssquashC{sTrunc A} a b p q @ i @ j + + +-- B.9.2 Truncated higher Hopf fibration + +-- See https://github.com/simhu/cubical/blob/connections/examples/truncHopf.cub + +trS2 : U = g2Trunc S2 +trS2Trunc : twogroupoid trS2 = g2TruncTwoGroupoid S2 +idIncNS : U = Path trS2 (g2inc north) (g2inc south) + +incSouthPath (x : S1) : Path trS2 (g2inc south) (g2inc south) = + -- let pp : Path S2 south south = + -- compPath S2 south north south ( meridP S1 base @ -i) (meridP S1 x) + -- in g2inc (pp @ i) + compPath trS2 (g2inc south) (g2inc north) (g2inc south) + ( g2inc (meridP S1 base @ -i)) ( g2inc (meridP S1 x @ i)) + + +multTwoSouth : S2 -> trS2 = split + north -> g2inc south + south -> g2inc south + merid x @ i -> incSouthPath x @ i + +meridIncSouth (x y : S1) : Path trS2 (g2inc north) (g2inc south) = + compPath trS2 (g2inc north) (g2inc south) (g2inc south) + ( g2inc (meridP S1 x @ i)) (incSouthPath y) + + +eqSubstSig (A : U) (F : A -> U) (x : A) : (y : A) (p : Path A x y) (u : F x) (v : F y) -> + Path U (PathS A F x y p u v) (Path (F y) (subst A F x y p u) v) = + J A x (\(y : A) (p : Path A x y) -> (u : F x) (v : F y) -> + Path U (PathS A F x y p u v) (Path (F y) (subst A F x y p u) v)) + rem + where + rem (u v : F x) : + Path U (PathS A F x x (<_> x) u v) + (Path (F x) (subst A F x x (<_> x) u) v) = + let goal : Path U + (Path (F x) u v) + (Path (F x) (transGen (<_> F x) 0 u) v) = + Path (F x) (transGen (<_> F x) (-i) u) v + in goal + +-- a general Lemma about set-valued family of type over S1 x S1 +lemSetTorus (E : S1 -> S1 -> U) (sE : set (E base base)) + (f : (y:S1) -> E base y) (g : (x:S1) -> E x base) + (efg : Path (E base base) (f base) (g base)) : (x y : S1) -> E x y = split + base -> f + loop @ i -> lem2 @ i + where + F (x : S1) : U = (y : S1) -> E x y + + sbE : (y : S1) -> set (E base y) = lemPropFib (\(y : S1) -> set (E base y)) pP sE + where pP (y : S1) : prop (set (E base y)) = setIsProp (E base y) + + lem1 : (y : S1) -> PathS S1 (\(x : S1) -> E x y) base base loopP (f y) (f y) = + let P (y : S1) : U = PathS S1 (\(x : S1) -> E x y) base base loopP (f y) (f y) + pP (y : S1) : prop (P y) = + let rem1 : Path U (P y) (Path (E base y) (subst S1 (\(x : S1) -> E x y) base base loopP (f y)) (f y)) = eqSubstSig S1 (\(x : S1) -> E x y) base base loopP (f y) (f y) + + rem2 : prop (Path (E base y) (subst S1 (\(x : S1) -> E x y) base base loopP (f y)) (f y)) = sbE y (subst S1 (\(x : S1) -> E x y) base base loopP (f y)) (f y) + + in substInv U prop (P y) (Path (E base y) (subst S1 (\(x : S1) -> E x y) base base loopP (f y)) (f y)) rem1 rem2 + + lem2 : PathS S1 (\(x : S1) -> E x base) base base loopP (g base) (g base) = + g (loopP @ i) + + bP : P base = substInv (E base base) (\(u : E base base) -> PathS S1 (\(x : S1) -> E x base) base base loopP u u) (f base) (g base) efg lem2 + in lemPropFib P pP bP + + lem2 : PathS S1 F base base loopP f f = + \(y : S1) -> lem1 y @ i + +-- First approach, like in the paper, that didn't work due to lack of +-- computation for J (and maybe regularity?). + +-- -- |p|^1 . | !p0 . q |^1 +-- auxComp (a b : S2) (p p0 q : Path S2 a b) : Path trS2 (g2inc a) (g2inc b) = +-- compPath trS2 (g2inc a) (g2inc b) (g2inc b) +-- ( g2inc (p @ i)) ( g2inc (compPath S2 b a b ( p0 @ -j) q @ i)) + +-- -- |p|^1 . | !p0 . q |^1 = |q|^1 . | !p0 . p |^1 +-- auxCompId (a b : S2) (p p0 q : Path S2 a b) : U = +-- Path (Path trS2 (g2inc a) (g2inc b)) (auxComp a b p p0 q) (auxComp a b q p0 p) + +-- This definition makes it hard to prove things later: +-- |p0|^1 . | !p0 . q |^1 = |q|^1 . | !p0 . p0 |^1 +-- alphaAuxCompId (a : S2) : (b : S2) (p0 q : Path S2 a b) -> auxCompId a b p0 p0 q = +-- J S2 a (\(b : S2) (p0 : Path S2 a b) -> (q : Path S2 a b) -> auxCompId a b p0 p0 q) rem2 +-- where p1 (q : Path S2 a a) : +-- Path (Path trS2 (g2inc a) (g2inc a)) +-- ( g2inc (compPath S2 a a a (<_> a) q @ i)) +-- ( g2inc (q @ i)) = +-- g2inc (comp1Path S2 a a q @ i @ j) +-- p2 (q : Path S2 a a) : Path (Path trS2 (g2inc a) (g2inc a)) +-- (auxComp a a (<_> a) (<_> a) q) +-- ( g2inc (compPath S2 a a a (<_> a) q @ i)) = +-- comp1Path trS2 (g2inc a) (g2inc a) +-- ( g2inc (compPath S2 a a a (<_> a) q @ i)) +-- p3 (q : Path S2 a a) : +-- Path (Path trS2 (g2inc a) (g2inc a)) +-- (auxComp a a (<_> a) (<_> a) q) +-- ( g2inc (q @ i)) = +-- compPath (Path trS2 (g2inc a) (g2inc a)) +-- (auxComp a a (<_> a) (<_> a) q) +-- ( g2inc (compPath S2 a a a (<_> a) q @ i)) +-- ( g2inc (q @ i)) +-- (p2 q) (p1 q) + +-- q1 : Path (Path trS2 (g2inc a) (g2inc a)) +-- ( g2inc (compPath S2 a a a (<_> a) (<_> a) @ i)) +-- ( g2inc a) = p1 (<_> a) + +-- q2' (q : Path S2 a a) : +-- Path (Path trS2 (g2inc a) (g2inc a)) +-- (compPath trS2 (g2inc a) (g2inc a) (g2inc a) ( g2inc (q @ i)) (<_> g2inc a)) +-- (auxComp a a q (<_> a) (<_> a)) = +-- compPath trS2 (g2inc a) (g2inc a) (g2inc a) +-- ( g2inc (q @ i)) (q1 @ -i) + +-- q2 (q : Path S2 a a) : +-- Path (Path trS2 (g2inc a) (g2inc a)) +-- (compPath trS2 (g2inc a) (g2inc a) (g2inc a) ( g2inc (q @ i)) (<_> g2inc a)) +-- ( g2inc (q @ i)) = compPath1 trS2 (g2inc a) (g2inc a) ( g2inc (q @ i)) + +-- q3 (q : Path S2 a a) : +-- Path (Path trS2 (g2inc a) (g2inc a)) +-- (auxComp a a q (<_> a) (<_> a)) +-- ( g2inc (q @ i)) = +-- compPath (Path trS2 (g2inc a) (g2inc a)) +-- (auxComp a a q (<_> a) (<_> a)) +-- (compPath trS2 (g2inc a) (g2inc a) (g2inc a) ( g2inc (q @ i)) (<_> g2inc a)) +-- ( g2inc (q @ i)) +-- ( q2' q @ -i) +-- (q2 q) + +-- rem2 (q : Path S2 a a) : +-- Path (Path trS2 (g2inc a) (g2inc a)) +-- (auxComp a a (<_> a) (<_> a) q) +-- (auxComp a a q (<_> a) (<_> a)) = +-- compPath (Path trS2 (g2inc a) (g2inc a)) +-- (auxComp a a (<_> a) (<_> a) q) +-- ( g2inc (q @ i)) +-- (auxComp a a q (<_> a) (<_> a)) +-- (p3 q) +-- ( q3 q @ -i) + +-- |p|^1 . | !p0 . p0 |^1 = |p0|^1 . | !p0 . p |^1 +-- betaAuxCompId (a : S2) (b : S2) (p0 p : Path S2 a b) : auxCompId a b p p0 p0 = +-- alphaAuxCompId a b p0 p @ -i + +-- alphaEqBetaDiag (a : S2) : (b : S2) (p0 : Path S2 a b) -> +-- Path (auxCompId a b p0 p0 p0) (alphaAuxCompId a b p0 p0) (betaAuxCompId a b p0 p0) = +-- J S2 a (\(b : S2) (p0 : Path S2 a b) -> +-- Path (auxCompId a b p0 p0 p0) (alphaAuxCompId a b p0 p0) (betaAuxCompId a b p0 p0)) +-- rem +-- where +-- rem : Path (auxCompId a a (<_> a) (<_> a) (<_> a)) +-- (alphaAuxCompId a a (<_> a) (<_> a)) +-- (betaAuxCompId a a (<_> a) (<_> a)) = ? + +substPathPi (A B : U) (f g : A -> B) (a : A) : (a' : A) (p : Path A a a') + (qa : Path B (f a) (g a)) (qa' : Path B (f a') (g a')) -> + Path (Path B (f a) (g a')) + (compPath B (f a) (g a) (g a') qa ( g (p @ i))) + (compPath B (f a) (f a') (g a') ( f (p @ i)) qa') -> + PathS A (\(x : A) -> Path B (f x) (g x)) a a' p qa qa' = + J A a + (\(a' : A) (p : Path A a a') -> + (qa : Path B (f a) (g a)) (qa' : Path B (f a') (g a')) -> + Path (Path B (f a) (g a')) + (compPath B (f a) (g a) (g a') qa ( g (p @ i))) + (compPath B (f a) (f a') (g a') ( f (p @ i)) qa') -> + PathS A (\(x : A) -> Path B (f x) (g x)) a a' p qa qa') + rem + where rem (qa : Path B (f a) (g a)) (qa' : Path B (f a) (g a)) + (pp : Path (Path B (f a) (g a)) + (compPath B (f a) (g a) (g a) qa (<_> g a)) + (compPath B (f a) (f a) (g a) (<_> f a) qa')) : + Path (Path B (f a) (g a)) qa qa' = + let p1 : Path (Path B (f a) (g a)) + (compPath B (f a) (g a) (g a) qa (<_> g a)) qa = + compPath1 B (f a) (g a) qa + p2 : Path (Path B (f a) (g a)) + (compPath B (f a) (f a) (g a) (<_> f a) qa') qa' = + comp1Path B (f a) (g a) qa' + in hcomp (Path B (f a) (g a)) (pp @ i) + [ (i = 0) -> p1 + , (i = 1) -> p2 ] + +-- alternative approach + +comp3 (A : U) (a b c d : A) (p : Path A a b) (q : Path A b c) (r : Path A c d) : Path A a d = + hcomp A (q @ i) [ (i = 0) -> p @ -j, (i = 1) -> r ] + +meridIncSouth' (x y : S1) : idIncNS = + comp3 trS2 (g2inc north) (g2inc south) (g2inc north) (g2inc south) + ( g2inc (meridP S1 x @ i)) -- p + ( g2inc (meridP S1 base @ -i)) -- q + ( g2inc (meridP S1 y @ j)) -- r + -- hcomp trS2 (g2inc (meridP S1 base @ -i)) + -- [ (i = 0) -> g2inc (meridP S1 x @ -j) + -- , (i = 1) -> g2inc (meridP S1 y @ j) ] + + -- compPath trS2 (g2inc north) (g2inc south) (g2inc south) + -- ( g2inc (meridP S1 x @ i)) (incSouthPath' y) + + +-- This would make a nice exercise +helper (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : + Square A a b b c p q p q = + hcomp A b [ (i = 0) -> p @ j \/ -k + , (i = 1) -> q @ j /\ k + , (j = 0) -> p @ i \/ -k + , (j = 1) -> q @ i /\ k ] + +temp (A : U) (a b c d : A) (p : Path A a b) (q : Path A b c) (r : Path A c d) : + Path (Path A a d) (compPath A a b d p (compPath A b c d q r)) (comp3 A a b c d p q r) = + let sq : Square A b c d d q (<_> d) (compPath A b c d q r) r = + hcomp A (q @ j) [ (i = 1) -> helper A b c d q r @ j + , (j = 0) -> q @ i /\ k + , (j = 1) -> r ] + goal : Path (Path A a d) (compPath A a b d p (compPath A b c d q r)) (comp3 A a b c d p q r) = + hcomp A (helper A a b c p q @ i @ j) [ (i = 0) -> p @ j /\ -k + , (i = 1) -> sq @ j ] + + in goal + + +meridIncSouthEq (x y : S1) : Path idIncNS (meridIncSouth x y) (meridIncSouth' x y) = + temp trS2 (g2inc north) (g2inc south) (g2inc north) (g2inc south) + ( g2inc (meridP S1 x @ i)) -- p + ( g2inc (meridP S1 base @ -i)) -- q + ( g2inc (meridP S1 y @ j)) -- r + + + +-- |p| . | !p0 | . |q| +auxComp' (a b : S2) (p p0 q : Path S2 a b) : Path trS2 (g2inc a) (g2inc b) = + hcomp trS2 (g2inc (p0 @ -i)) + [ (i = 0) -> g2inc (p @ -j) + , (i = 1) -> g2inc (q @ j) ] + -- compPath trS2 (g2inc a) (g2inc b) (g2inc b) + -- ( g2inc (p @ i)) + -- (compPath trS2 (g2inc b) (g2inc a) (g2inc b) + -- ( g2inc (p0 @ -j)) + -- ( g2inc (q @ i))) + +-- |p| . | !p0 | . |q| = |q| . | !p0 | . |p| +auxCompId' (a b : S2) (p p0 q : Path S2 a b) : U = + Path (Path trS2 (g2inc a) (g2inc b)) (auxComp' a b p p0 q) (auxComp' a b q p0 p) + +-- |p0| . | !p0 | . |q| = |q| . | !p0 | . |p0| +alphaAuxCompId' (a : S2) (b : S2) (p0 q : Path S2 a b) : auxCompId' a b p0 p0 q = + let a' : trS2 = g2inc a + b' : trS2 = g2inc b + p0' : Path trS2 a' b' = g2inc (p0 @ i) + p0inv : Path trS2 b' a' = p0' @ -i + q' : Path trS2 a' b' = g2inc (q @ i) + qinv : Path trS2 b' a' = q' @ -i + + bottom : Square trS2 b' a' b' a' p0inv p0inv + (compPath trS2 b' a' b' p0inv q') + (compPath trS2 a' b' a' q' p0inv) = + hcomp trS2 (helper trS2 b' a' b' p0inv q' @ i @ j) + [ (j = 0) -> p0inv @ i + , (j = 1) -> helper trS2 a' b' a' q' p0inv @ i @ k ] + + right : Square trS2 a' a' b' b' + (compPath trS2 a' b' a' q' p0inv) (<_> b') q' p0' = + hcomp trS2 (q' @ j \/ k) + [ (j = 0) -> q' @ k + , (j = 1) -> p0' @ k \/ -l + , (k = 1) -> b' ] + + left : Square trS2 b' b' a' a' + (compPath trS2 b' a' b' p0inv q') (<_> a') p0inv qinv = + hcomp trS2 (p0inv @ j \/ k) + [ (j = 0) -> p0inv @ k + , (j = 1) -> qinv @ k \/ -l + , (k = 1) -> a' ] + + goal : Square trS2 a' b' a' b' + (auxComp' a b p0 p0 q) (auxComp' a b q p0 p0) (<_> a') (<_> b') = + hcomp trS2 (bottom @ i @ j) + [ (i = 0) -> left @ j + , (i = 1) -> right @ j ] + in goal @ j @ i + +-- |p| . | !p0 | . |p0| = |p0| . | !p0 | . |p| +betaAuxCompId' (a : S2) (b : S2) (p0 p : Path S2 a b) : auxCompId' a b p p0 p0 = + alphaAuxCompId' a b p0 p @ -i + +alphaEqBetaDiag' (a : S2) : (b : S2) (p0 : Path S2 a b) -> + Path (auxCompId' a b p0 p0 p0) (alphaAuxCompId' a b p0 p0) (betaAuxCompId' a b p0 p0) = + J S2 a (\(b : S2) (p0 : Path S2 a b) -> + Path (auxCompId' a b p0 p0 p0) (alphaAuxCompId' a b p0 p0) (betaAuxCompId' a b p0 p0)) + rem + where + rem : Path (auxCompId' a a (<_> a) (<_> a) (<_> a)) + (alphaAuxCompId' a a (<_> a) (<_> a)) + (betaAuxCompId' a a (<_> a) (<_> a)) = + let foo : Square trS2 (g2inc a) (g2inc a) (g2inc a) (g2inc a) + (<_> g2inc a) (<_> g2inc a) (<_> g2inc a) (<_> g2inc a) = + hcomp trS2 (g2inc a) + [ (i = 0) -> <_> g2inc a, (i = 1) -> <_> g2inc a + , (j = 0) -> <_> g2inc a, (j = 1) -> <_> g2inc a ] + + bar : Square trS2 (g2inc a) (g2inc a) (g2inc a) (g2inc a) + (compPath trS2 (g2inc a) (g2inc a) (g2inc a) (<_> g2inc a) (<_> g2inc a)) + (<_> g2inc a) (<_> g2inc a) (<_> g2inc a) = + hcomp trS2 (g2inc a) + [ (i = 0) -> <_> g2inc a + , (i = 1) -> <_> g2inc a + , (k = 1) -> <_> g2inc a ] + + T : Path trS2 (g2inc a) (g2inc a) = + hcomp trS2 (g2inc a) [ (i = 0) -> <_> g2inc a, (i = 1) -> <_> g2inc a ] + + T0 : Path (Path trS2 (g2inc a) (g2inc a)) T T = + hcomp trS2 (foo @ i @ j) + [ (i = 0) -> <_> g2inc a + , (i = 1) -> foo @ j ] + T1 : Path (Path trS2 (g2inc a) (g2inc a)) T T = + hcomp trS2 (foo @ i @ j) + [ (i = 0) -> foo @ j + , (i = 1) -> <_> g2inc a ] + + test : Path (Square trS2 (g2inc a) (g2inc a) (g2inc a) (g2inc a) + (<_> g2inc a) (<_> g2inc a) (<_> g2inc a) (<_> g2inc a)) + foo (<_ _> g2inc a) = + hcomp trS2 (g2inc a) [ (i = 0) -> <_> g2inc a + , (i = 1) -> <_> g2inc a + , (j = 0) -> <_> g2inc a + , (j = 1) -> <_> g2inc a + , (k = 1) -> <_> g2inc a] + + key0 : Path (Path (Path trS2 (g2inc a) (g2inc a)) T T) + T0 ( hcomp trS2 (g2inc a) + [ (i = 0) -> <_> g2inc a + , (i = 1) -> <_> g2inc a ]) = + hcomp trS2 (test @ k @ i @ j) + [ (i = 0) -> <_> g2inc a + , (i = 1) -> test @ k @ j ] + key1 : Path (Path (Path trS2 (g2inc a) (g2inc a)) T T) + T1 ( hcomp trS2 (g2inc a) + [ (i = 0) -> <_> g2inc a + , (i = 1) -> <_> g2inc a ]) = + hcomp trS2 (test @ k @ i @ j) + [ (i = 0) -> test @ k @ j + , (i = 1) -> <_> g2inc a ] + + key : Path (Path (Path trS2 (g2inc a) (g2inc a)) T T) T0 T1 = + compPath (Path (Path trS2 (g2inc a) (g2inc a)) T T) T0 ( hcomp trS2 (g2inc a) + [ (i = 0) -> <_> g2inc a + , (i = 1) -> <_> g2inc a ]) T1 key0 ( key1 @ -i) + + goal : Path (Path (Path trS2 (g2inc a) (g2inc a)) T T) + ( hcomp trS2 (T0 @ j @ i) + [ (j = 0) -> bar @ i, (j = 1) -> bar @ i ]) + ( hcomp trS2 (T1 @ j @ i) + [ (j = 0) -> bar @ i, (j = 1) -> bar @ i ] ) = + hcomp trS2 + (key @ k @ j @ i) + [ (j = 0) -> bar @ i, (j = 1) -> bar @ i ] + in goal + + +multTwoMeridMerid' : (x y : S1) -> Path idIncNS (meridIncSouth' x y) (meridIncSouth' y x) = + lemSetTorus E sE + (\(x : S1) -> alphaAuxCompId' north south (meridP S1 base) (meridP S1 x)) + (\(x : S1) -> betaAuxCompId' north south (meridP S1 base) (meridP S1 x)) + (alphaEqBetaDiag' north south (meridP S1 base)) + where E (x y : S1) : U = Path idIncNS (meridIncSouth' x y) (meridIncSouth' y x) + + sE : set (E base base) = + g2TruncTwoGroupoid S2 (g2inc north) (g2inc south) + (meridIncSouth' base base) (meridIncSouth' base base) + +multTwoMeridMerid (x y : S1) : Path idIncNS (meridIncSouth x y) (meridIncSouth y x) = + hcomp idIncNS (multTwoMeridMerid' x y @ i) + [ (i = 0) -> meridIncSouthEq x y @ -j + , (i = 1) -> meridIncSouthEq y x @ -j ] + +multTwoMerid (x : S1) : (y : S2) -> Path trS2 (g2inc y) (multTwoSouth y) = split + north -> g2inc (meridP S1 x @ i) + south -> incSouthPath x + merid y @ i -> substPathPi S2 trS2 (\(x : S2) -> g2inc x) multTwoSouth north south (meridP S1 y) + ( g2inc (meridP S1 x @ i)) + (incSouthPath x) (multTwoMeridMerid x y) @ i + +multTwo : S2 -> S2 -> trS2 = split + north -> \(x : S2) -> g2inc x + south -> multTwoSouth + merid x @ i -> \(y : S2) -> multTwoMerid x y @ i + +multTwoTilde (x : S2) : trS2 -> trS2 = + g2TruncRec S2 trS2 trS2Trunc (multTwo x) + +idSIntro (A : U) (F : A -> U) (x y : A) (p : Path A x y) (u : F x) (v : F y) + (w : Path (F y) (subst A F x y p u) v) : PathS A F x y p u v = + transGen ( eqSubstSig A F x y p u v @ -i) 0 w + +lemPropS2 (P : S2 -> U) (pP : (x : S2) -> prop (P x)) (pN : P north) : (x : S2) -> P x = split + north -> pN + south -> subst S2 P north south (meridP S1 base) pN + merid x @ i -> rem1 @ i + where + pS (x : S1) : P south = subst S2 P north south (meridP S1 x) pN + + rem (p : P south) : PathS S2 P north south (meridP S1 x) pN p = + idSIntro S2 P north south (meridP S1 x) pN p (pP south (pS x) p) + + rem1 : PathS S2 P north south (meridP S1 x) pN (pS base) = rem (pS base) + +-- This needs the elimination principle for 2-groupoid truncation... +lem3Trunc (A B : U) (hB : twogroupoid B) (g h : g2Trunc A -> B) + (H : (a : A) -> Path B (g (g2inc a)) (h (g2inc a))) : + (x : g2Trunc A) -> Path B (g x) (h x) = + g2TruncElim A (\(x : g2Trunc A) -> Path B (g x) (h x)) + (\(x : g2Trunc A) -> twogroupoidThreeGroupoid B hB (g x) (h x)) H + +multTwoTildeEquiv : (x : S2) -> isEquiv trS2 trS2 (multTwoTilde x) = + lemPropS2 + (\(x : S2) -> isEquiv trS2 trS2 (multTwoTilde x)) + (\(x : S2) -> propIsEquiv trS2 trS2 (multTwoTilde x)) + multEquivNorth + where multNorthEqPath : Path (trS2 -> trS2) (\(x : trS2) -> x) (multTwoTilde north) = + \(x : trS2) -> lem3Trunc S2 trS2 (g2TruncTwoGroupoid S2) (idfun trS2) + (multTwoTilde north) (\(a : S2) -> <_> g2inc a) x @ i + multEquivNorth : isEquiv trS2 trS2 (multTwoTilde north) = + subst (trS2 -> trS2) (isEquiv trS2 trS2) (idfun trS2) + (multTwoTilde north) multNorthEqPath (idIsEquiv trS2) + +tHopf3 : S3 -> U = split + north -> trS2 + south -> trS2 + merid x @ i -> ua trS2 trS2 (multTwoTilde x,multTwoTildeEquiv x) @ i + +pi3S3 : (Omega3 S3pt).1 -> (Omega2 (g2Truncpt S2pt)).1 = + mapOmegaRefl2 (Omega S3pt) trS2 pi3S3' + where + pi3S3' (p : (Omega S3pt).1) : trS2 = + subst S3 tHopf3 north north p (g2inc north) + + +-------------------------------------------------------------------------------- +-- B.10 Loop space of truncations + +-- See https://github.com/simhu/cubical/blob/connections/examples/loopTrunc.cub + +-- We now need full univalence to prove "groupoidSET : groupoid SET" +-- todo: is full univalence strictly necessary for this? +-- note: this is a proposition, so making it opaque should probably be fine. + +univalenceAlt (B : U) : isContr ((X : U) * equiv X B) = + ((B,idEquiv B) + ,\(w : (X : U) * equiv X B) + -> let GlueB : U = Glue B [(i=0) -> (B,idEquiv B), (i=1) -> w] + unglueB (g : GlueB) : B = + unglue g B [(i=0) -> (B,idEquiv B) + ,(i=1) -> w] + in (GlueB + ,unglueB + ,\(b : B) + -> let center : fiber GlueB B unglueB b + = (glue (hcomp B b [(i=0) -> b + ,(i=1) -> (w.2.2 b).1.2]) + [(i=0) -> b + ,(i=1) -> (w.2.2 b).1.1] + ,hfill B b [(i=0) -> b + ,(i=1) -> (w.2.2 b).1.2]) + contr (v : fiber GlueB B unglueB b) + : Path (fiber GlueB B unglueB b) center v + = (glue (hcomp B b [(i=0) -> v.2 @ (j /\ k) + ,(i=1) -> ((w.2.2 b).2 v @ j).2 + ,(j=0) -> hfill B b [(i=0) -> b + ,(i=1) -> (w.2.2 b).1.2] + ,(j=1) -> v.2]) + [(i=0) -> v.2 @ j + ,(i=1) -> ((w.2.2 b).2 v @ j).1] + ,hfill B b [(i=0) -> v.2 @ (j /\ l) + ,(i=1) -> ((w.2.2 b).2 v @ j).2 + ,(j=0) -> hfill B b [(i=0) -> b + ,(i=1) -> (w.2.2 b).1.2] + ,(j=1) -> v.2]) + in (center,contr))) + +retIsContr (A B : U) (f : A -> B) (g : B -> A) + (h : (x : A) -> Path A (g (f x)) x) (v : isContr B) + : isContr A = (g b,p) + where + b : B = v.1 + q : (y:B) -> Path B b y = v.2 + p (x:A) : Path A (g b) x = + hcomp A (g (q (f x) @ i)) [(i=0) -> g b,(i=1) -> h x] + +sigIsContr (A : U) (B : A -> U) (u : isContr A) + (q : (x : A) -> isContr (B x)) : isContr ((x:A) * B x) = ((a,g a),r) + where + a : A = u.1 + p : (x:A) -> Path A a x = u.2 + g (x:A) : B x = (q x).1 + h (x:A) : (y:B x) -> Path (B x) (g x) y = (q x).2 + C : U = (x:A) * B x + r (z:C) : Path C (a,g a) z = + (p z.1@i,h (p z.1@i) (comp (B (p z.1@i\/-j)) z.2 [(i=1)->z.2])@i) + +isPathContr (A:U) (cA:isContr A) (x y:A) : isContr (Path A x y) = (p0,q) + where + a : A = cA.1 + f : (x:A) -> Path A a x = cA.2 + p0 : Path A x y = hcomp A a [(i=0) -> f x,(i=1) -> f y] + q (p:Path A x y) : Path (Path A x y) p0 p = + hcomp A a [(i=0) -> f x,(i=1) -> f y, + (j=0) -> hcomp A a [(k=0) -> a,(i=0) -> f x@k/\l,(i=1) -> f y@k/\l], + (j=1) -> f (p@i)] + +isEquivContr (A B:U) (cA:isContr A) (cB:isContr B) (f:A->B) : isEquiv A B f = + \ (y:B) -> sigIsContr A (\ (x:A) -> Path B y (f x)) cA (\ (x:A) -> isPathContr B cB y (f x)) + +totalFun (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (w:Sigma A B) : Sigma A C = + (w.1,f (w.1) (w.2)) + +funFib1 (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) : + fiber (Sigma A B) (Sigma A C) (totalFun A B C f) (x0,z0) = ((x0,u.1),(x0,u.2@i)) + +funFib2 (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) + (w : fiber (Sigma A B) (Sigma A C) (totalFun A B C f) (x0,z0)) : fiber (B x0) (C x0) (f x0) z0 = (b0,s) + where + x : A = w.1.1 + b : B x = w.1.2 + p : Path A x0 x = (w.2@i).1 + q : PathP (C (p@i)) z0 (f x b) = (w.2@i).2 + b0 : B x0 = comp (B (p@-i)) b [] + r : PathP (B (p@-i)) b b0 = comp (B (p@-j\/-i)) b [(i=0) -> b] + s : Path (C x0) z0 (f x0 b0) = comp (C (p@(i/\-j))) (q@i) [(i=0) -> z0,(i=1) -> f (p@-k) (r@k)] + +compFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) : + fiber (B x0) (C x0) (f x0) z0 = funFib2 A B C f x0 z0 (funFib1 A B C f x0 z0 u) + +retFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) : + Path (fiber (B x0) (C x0) (f x0) z0) (funFib2 A B C f x0 z0 (funFib1 A B C f x0 z0 u)) u = + (comp ( B x0) u.1 [(l=1) -> u.1], + comp ( C x0) (u.2 @ i) [ (l=1) -> u.2 @ i, + (i = 0) -> z0, + (i = 1) -> f x0 (comp ( B x0) u.1 [ (j = 0) -> u.1, (l=1) -> u.1 ]) ]) + +equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (Sigma A B)) (cC : isContr (Sigma A C)) (x:A) + : isEquiv (B x) (C x) (f x) = + \ (z:C x) -> retIsContr (fiber (B x) (C x) (f x) z) (fiber (Sigma A B) (Sigma A C) (totalFun A B C f) (x,z)) + (funFib1 A B C f x z) + (funFib2 A B C f x z) + (retFunFib A B C f x z) + (isEquivContr (Sigma A B) (Sigma A C) cB cC (totalFun A B C f) (x,z)) + +contrSingl' (A : U) (a b : A) (p : Path A a b) : + Path ((x:A) * Path A x b) (b,<_>b) (a,p) = (p @ -i, p @ -i\/j) + +lemSinglContr' (A:U) (a:A) : isContr ((x:A) * Path A x a) = + ((a,<_>a),\ (z:(x:A) * Path A x a) -> contrSingl' A z.1 a z.2) + +thmUniv (t : (A X : U) -> Path U X A -> equiv X A) (A : U) : + (X : U) -> isEquiv (Path U X A) (equiv X A) (t A X) = + equivFunFib U (\(X : U) -> Path U X A) (\(X : U) -> equiv X A) + (t A) (lemSinglContr' U A) (univalenceAlt A) + +substTrans (A : U) (P : A -> U) (a b : A) (p : Path A a b) (e : P a) : P b = + transGen ( P (p @ i)) 0 e + +transEquiv' (A X : U) (p : Path U X A) : equiv X A = + substTrans U (\(Y : U) -> equiv Y A) A X ( p @ -i) (idEquiv A) + +univalence (A X : U) : isEquiv (Path U X A) (equiv X A) (transEquiv' A X) = + thmUniv transEquiv' A X + +corrUniv (A B : U) : Path U (Path U A B) (equiv A B) = + ua (Path U A B) (equiv A B) (transEquiv' B A,univalence B A) + +pi (A:U) (P:A->U) : U = (x:A) -> P x + +idPi (A:U) (B:A->U) (f g : pi A B) : Path U (Path (pi A B) f g) ((x:A) -> Path (B x) (f x) (g x)) = + isoPath (Path (pi A B) f g) ((x:A) -> Path (B x) (f x) (g x)) F G S T + where T0 : U = Path (pi A B) f g + T1 : U = (x:A) -> Path (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) : Path T1 (F (G p)) p = refl T1 p + T (p:T0) : Path 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 (Path (pi A B) f g) = + rem + where + T : U = (x:A) -> Path (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 (Path (pi A B) f g) = + subst U prop T (Path (pi A B) f g) (idPi A B f g@-i) rem1 + + +lemPathSig (A:U) (B : A -> U) (t u : Sigma A B) : + Path U (Path (Sigma A B) t u) ((p : Path A t.1 u.1) * PathP ( B (p @ i)) t.2 u.2) = + isoPath T0 T1 f g s t where + T0 : U = Path (Sigma A B) t u + T1 : U = (p:Path A t.1 u.1) * PathP ( 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) : Path T1 (f (g z)) z = refl T1 z + t (q:T0) : Path T0 (g (f q)) q = refl T0 q + +lemContr (A:U) (pA:prop A) (a:A) : isContr A = (a,rem) + where rem (y:A) : Path A a y = pA a y + +lem2 (A:U) (B:A-> U) (t u : Sigma A B) (p:Path A t.1 u.1) : + Path U (PathP (B (p@i)) t.2 u.2) (Path (B u.1) (transport (B (p@i)) t.2) u.2) = + funDepTr A B t.1 u.1 p t.2 u.2 + +lem3 (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : Sigma A B) (p:Path A t.1 u.1) : + isContr (PathP (B (p@i)) t.2 u.2) = lemContr T0 (substInv U prop T0 T1 rem rem1) rem2 + where P : Path U (B t.1) (B u.1) = B (p@i) + T0 : U = PathP P t.2 u.2 + T1 : U = Path (B u.1) (transport P t.2) u.2 + rem : Path 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) + +lem6 (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) : Path U ((x:A)*P x) A = isoPath 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).1) + s (z:T) : Path T (g (f z)) z = (z.1,((cA z.1).2 z.2)@ i) + t (x:A) : Path A (f (g x)) x = refl A x + +lemSigProp (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : Sigma A B) : Path U (Path (Sigma A B) t u) (Path A t.1 u.1) = + compPath U (Path (Sigma A B) t u) ((p:Path A t.1 u.1) * PathP ( B (p@i)) t.2 u.2) (Path A t.1 u.1) rem2 rem1 + where + T : U = Path A t.1 u.1 + C (p:T) : U = PathP ( B (p@i)) t.2 u.2 + rem (p : T) : isContr (C p) = lem3 A B pB t u p + rem1 : Path U ((p:T) * C p) T = lem6 T C rem + rem2 : Path U (Path (Sigma A B) t u) ((p:T) * C p) = lemPathSig A B t u + +eqEquivFst (A B : U) : (t u : equiv A B) -> + Path U (Path (equiv A B) t u) (Path (A -> B) t.1 u.1) + = lemSigProp (A -> B) (isEquiv A B) (propIsEquiv A B) + +groupoidPi (A : U) (B : A -> U) (h : (x : A) -> groupoid (B x)) (f g : pi A B) : + set (Path (pi A B) f g) = subst U set T (Path (pi A B) f g) ( idPi A B f g @ -i) rem1 + where + T : U = (x : A) -> Path (B x) (f x) (g x) + rem1 : set T = setPi A (\(x : A) -> Path (B x) (f x) (g x)) (\(x : A) -> h x (f x) (g x)) + +groupoidFun (A B : U) (sB : groupoid B) : groupoid (A -> B) = + groupoidPi A (\(x : A) -> B) (\(x : A) -> sB) + +groupoidPath (A B : U) (sB : groupoid B) : groupoid (Path U A B) = + substInv U groupoid (Path U A B) (equiv A B) (corrUniv A B) (rem A B sB) + where + rem (A B : U) (sB : groupoid B) (t u : equiv A B) : set (Path (equiv A B) t u) = + substInv U set (Path (equiv A B) t u) (Path (A -> B) t.1 u.1) + (eqEquivFst A B t u) (groupoidFun A B sB t.1 u.1) + +twogroupoidGROUPOID : twogroupoid GROUPOID = \(A B : GROUPOID) -> + let rem : groupoid (Path U A.1 B.1) = groupoidPath A.1 B.1 B.2 + rem1 : Path U (Path GROUPOID A B) (Path U A.1 B.1) = + lemSigProp U groupoid groupoidIsProp A B + in substInv U groupoid (Path GROUPOID A B) (Path U A.1 B.1) rem1 rem + +truncPath2 (A : ptType) : g2Trunc A.1 -> GROUPOID = + g2TruncRec A.1 GROUPOID twogroupoidGROUPOID + (\(x : A.1) -> (gTrunc (Path A.1 (pt A) x),gTruncGroupoid (Path A.1 (pt A) x))) + +kappaTwo (A : ptType) (p : (Omega (g2Truncpt A)).1) : gTrunc (Omega A).1 = + subst (g2Trunc A.1) (\(x : g2Trunc A.1) -> (truncPath2 A x).1) + (g2inc (pt A)) (g2inc (pt A)) p (ginc (<_> pt A)) + +kappaTwoPt (A : ptType) : + Path (gTrunc (Omega A).1) + (kappaTwo A (pt (Omega (g2Truncpt A)))) + (pt (gTruncpt (Omega A))) + = transGen (<_> (truncPath2 A (pt (g2Truncpt A))).1) i (ginc (<_> pt A)) + +-- Groupoid set +setFun (A B : U) (sB : set B) : set (A -> B) = + setPi A (\(x : A) -> B) (\(x : A) -> sB) + +setPath (A B : U) (sB : set B) : set (Path U A B) = + substInv U set (Path U A B) (equiv A B) (corrUniv A B) (rem A B sB) + where + rem (A B : U) (sB:set B) (t u:equiv A B) : prop (Path (equiv A B) t u) + = substInv U prop (Path (equiv A B) t u) (Path (A -> B) t.1 u.1) + (eqEquivFst A B t u) (setFun A B sB t.1 u.1) + +groupoidSET : groupoid SET = \(A B : SET) -> + let rem : set (Path U A.1 B.1) = setPath A.1 B.1 B.2 + rem1 : Path U (Path SET A B) (Path U A.1 B.1) = + lemSigProp U set setIsProp A B + in substInv U set (Path SET A B) (Path U A.1 B.1) rem1 rem + +truncPath1 (A : ptType) : gTrunc A.1 -> SET = + gTruncRec A.1 SET groupoidSET + (\(x : A.1) -> (sTrunc (Path A.1 (pt A) x),setTruncSet (Path A.1 (pt A) x))) + +kappaOne (A : ptType) (p : (Omega (gTruncpt A)).1) : sTrunc (Omega A).1 = + subst (gTrunc A.1) (\(x : gTrunc A.1) -> (truncPath1 A x).1) + (ginc (pt A)) (ginc (pt A)) p (sinc (<_> pt A)) + + +-------------------------------------------------------------------------------- +-- B.11 Down one more dimension + +-- e'_2 from 12 +pi2S2' (p : (Omega2 S2pt).1) : loopS1 = + let point : (Omega S2pt).1 = pt (Omega S2pt) + in subst (Omega S2pt).1 HopfOne point point p (<_> base) + +e2' : sTrunc (Omega2 S2pt).1 -> loopS1 = + sTruncRec (Omega2 S2pt).1 loopS1 setLoop pi2S2' + +-} -------------------------------------------------------------------------------- -- B.2 The definition @@ -389,6 +2074,26 @@ f4 : (Omega3 (joinpt S1pt S1)).1 -> (Omega3 S2pt).1 = -- (mapOmega3 (joinpt S1pt S1) S2pt alpha).1 mapOmegaRefl3 (joinpt S1pt S1) S2 alpha.1 +{- + +f5 : (Omega3 S2pt).1 -> (Omega3 (joinpt S1pt S1)).1 = h + +f6 : (Omega3 (joinpt S1pt S1)).1 -> (Omega3 S3pt).1 = + mapOmegaRefl3 (joinpt S1pt S1) S3 einv + +f7 : (Omega3 S3pt).1 -> (Omega2 (g2Truncpt S2pt)).1 = pi3S3 + +f8 : (Omega2 (g2Truncpt S2pt)).1 -> (Omega (gTruncpt (Omega S2pt))).1 = + (mapOmega (Omega (g2Truncpt S2pt)) (gTruncpt (Omega S2pt)) (kappaTwo S2pt, kappaTwoPt S2pt)).1 + +f9 : (Omega (gTruncpt (Omega S2pt))).1 -> sTrunc (Omega2 S2pt).1 = + kappaOne (Omega S2pt) + +f10 : sTrunc (Omega2 S2pt).1 -> loopS1 = e2' + +-- I think this is correct +f11 (p : loopS1) : Z = encode base p +-} -- WORKS test0To1 : (Omega2 S2pt).1 = f1 (f0 oneZ) @@ -399,14 +2104,38 @@ test0To2 : (Omega3 S3pt).1 = f2 test0To1 -- WORKS test0To31 : (Omega3 (joinpt boolpt S2)).1 = f31 test0To2 --- WORKS +-- WORKS (without endpoint correction) test0To32 : (Omega3 (joinpt boolpt (join bool S1))).1 = f32 test0To2 --- WORKS +-- WORKS (without endpoint correction) test0To33 : (Omega3 (joinpt (joinpt boolpt bool) S1)).1 = f33 test0To2 --- WORKS (~2min) +-- WORKS without endpoint correction (~1s) test0To3 : (Omega3 (joinpt S1pt S1)).1 = f3 test0To2 --- WORKS (2m54s) +-- WORKS without endpoint correction (~2s) test0To4 : (Omega3 S2pt).1 = f4 test0To3 + +{- + +-- ? (not finished) +test0To5 : (Omega3 (joinpt S1pt S1)).1 = f5 test0To4 + +-- ? (not finished) +test0To6 : (Omega3 S3pt).1 = f6 test0To5 + +-- ? (not finished) +test0To7 : (Omega2 (g2Truncpt S2pt)).1 = f7 test0To6 + +-- ? (not finished) +test0To8 : (Omega (gTruncpt (Omega S2pt))).1 = f8 test0To7 + +-- ? (not finished) +test0To9 : sTrunc (Omega2 S2pt).1 = f9 test0To8 + +-- ? (not finished) +test0To10 : loopS1 = f10 test0To9 + +-- This should be "pos (suc (suc zero))"... +brunerie : Z = f11 test0To10 +-}