-module hopf where
-
-import truncS2
-import mult
-
-hopf : S2 -> U = split
- north -> S1
- south -> S1
- merid x @ i -> eqS1 x @ i
-
+module hopf where\r
+\r
+import truncS2\r
+import mult\r
+import pointed\r
+import join\r
+\r
+hopf : S2 -> U = split\r
+ north -> S1\r
+ south -> S1\r
+ merid x @ i -> eqS1 x @ i\r
+\r
+funExt1 (C B : U) (F : C -> U) (a :C) : (b : C) (p : Id C a b)\r
+ (f : F a -> B) (g : F b -> B)\r
+ (h : (x : F a) -> Id B (f x) (g (subst C F a b p x)))\r
+ -> IdS C (\ (z:C) -> F z -> B) a b p f g = \r
+ J C a (\ (b:C) (p:Id C a b) -> (f : F a -> B) (g : F b -> B)\r
+ (h : (x : F a) -> Id B (f x) (g (subst C F a b p x)))\r
+ -> IdS C (\ (z:C) -> F z -> B) a b p f g) rem\r
+ where rem (f g : F a -> B) (h : (x : F a) -> Id B (f x) (g x)) : Id (F a -> B) f g = \r
+ <i>\(x:F a) -> h x @ i\r
+\r
+t : (x : S2) -> hopf x -> join S1 S1 = split\r
+ north -> \ (a:S1) -> inl a\r
+ south -> \ (a:S1) -> inr a\r
+ merid x @ i -> funExt1 S2 (join S1 S1) hopf north south (<j>merid{S2} x@j) (\ (y:S1) -> inl y) (\ (y:S1) -> inr y)\r
+ (\ (y:S1) -> <j>pushC{join S1 S1} y (mult x y)@j) @ i\r
+\r
+totalHopfToJoin (xy:(x : S2) * hopf x) : join S1 S1 = t xy.1 xy.2\r
+\r
+one : nat = suc zero\r
+two : nat = suc one\r
+three : nat = suc two\r
+\r
+S3 : U = susp S2\r
+ptS3 : ptType = (S3,north)\r
+ptS2 : ptType = (S2,north)\r
+ptS1 : ptType = (S1,base)\r
+\r
+hopfOne : (itOmega one ptS2).1 -> U = itFibOmega one ptS2 hopf base\r
+\r
+hopfTwo : (itOmega two ptS2).1 -> U = itFibOmega two ptS2 hopf base\r
+\r
+hopfThree : (itOmega three ptS2).1 -> U = itFibOmega three ptS2 hopf base\r
+\r
+ptJoin (pA:ptType) (B:U) : ptType = (join pA.1 B, inl (pt pA))\r
+\r
+fibContrHopfThree (p : (itOmega three ptS2).1) : hopfThree p = \r
+ truncFibOmega (itOmega two ptS2) hopfTwo (refl (Id S1 base base) (refl S1 base)) zero\r
+ (truncFibOmega (Omega ptS2) hopfOne (refl S1 base) one\r
+ (truncFibOmega ptS2 hopf base two isGroupoidS1 (refl S2 north))\r
+ (refl (Omega ptS2).1 (pt (Omega ptS2)))) p\r
+\r
+\r
+-- The map h from 9.3\r
+hopfLoop (p : (itOmega three ptS2).1) : (itOmega three (ptJoin ptS1 S1)).1 = \r
+ itMapOmegaRefl three (Sigma S2 hopf, (north,base)) (join S1 S1) totalHopfToJoin\r
+ (itTotalFibOmega three ptS2 hopf base (p, fibContrHopfThree p))\r
+\r
+\r
--- /dev/null
+module join where\r
+\r
+import prelude\r
+import susp\r
+\r
+data join (A B:U) = inl (a:A) | inr (b:B) | pushC (a:A) (b:B) <i> [(i=0) -> inl a, (i=1) -> inr b]\r
+\r
+push (A B:U) (a:A) (b:B) : Id (join A B) (inl a) (inr b) = <i>pushC{join A B} a b@i\r
+\r
+-- Map from [join (join A B) C] to [join A (join B C)]\r
+\r
+l2rInl (A B C : U) : join A B -> join A (join B C) = split\r
+ inl a -> inl a\r
+ inr b -> inr (inl b)\r
+ pushC a b @ i -> push A (join B C) a (inl b) @ i\r
+\r
+l2rPushInr (A B C : U) (b : B) (c : C) : Id (join A (join B C)) (inr (inl b)) (inr (inr c)) = \r
+ <i>inr (push B C b c@i)\r
+\r
+l2rSquare (A B C : U) (a : A) (b : B) (c : C) :\r
+ IdP (<i> Id (join A (join B C)) (inl a) (inr (push B C b c@i)))\r
+ (<i>push A (join B C) a (inl b)@i) (<i>push A (join B C) a (inr c)@i) =\r
+ <i j>push A (join B C) a (push B C b c@i)@j\r
+\r
+opl2r (A : U) (a b c : A) (p : Id A a c) (q : Id A a b) (r : Id A b c) \r
+ (sq : Square A a a (refl A a) b c r q p) : Square A a b q c c (refl A c) p r =\r
+ <i j>comp A (sq@j@i) [(i=0) -> <k>p@(j/\k),(j=1) -> <k>p@(i\/k)]\r
+\r
+l2rPushPush (A B C : U) (a : A) (b : B) (c : C) :\r
+ Square (join A (join B C))\r
+ (inl a) (inr (inl b)) (push A (join B C) a (inl b))\r
+ (inr (inr c)) (inr (inr c)) (refl (join A (join B C)) (inr (inr c)))\r
+ (push A (join B C) a (inr c))\r
+ (l2rPushInr A B C b c) = \r
+ opl2r (join A (join B C)) (inl a) (inr (inl b)) (inr (inr c))\r
+ (push A (join B C) a (inr c)) (push A (join B C) a (inl b)) (l2rPushInr A B C b c)\r
+ (l2rSquare A B C a b c)\r
+\r
+l2rPush (A B C : U) (c : C) : (u : join A B) ->\r
+ Id (join A (join B C)) (l2rInl A B C u) (inr (inr c)) = split\r
+ inl a -> push A (join B C) a (inr c)\r
+ inr b -> l2rPushInr A B C b c\r
+ pushC a b @ i -> l2rPushPush A B C a b c @ i\r
+\r
+l2r (A B C : U) : join (join A B) C -> join A (join B C) = split\r
+ inl jab -> l2rInl A B C jab\r
+ inr c -> inr (inr c)\r
+ pushC p q @i -> l2rPush A B C q p @i\r
+\r
+\r
+-- Map from [join A (join B C)] to [join (join A B) C]\r
+\r
+r2lInr (A B C : U) : join B C -> join (join A B) C = split\r
+ inl b -> inl (inr b)\r
+ inr c -> inr c\r
+ pushC b c @i -> push (join A B) C (inr b) c @i\r
+\r
+r2lPushInl (A B C : U) (a : A) (b : B) : Id (join (join A B) C) (inl (inl a)) (inl (inr b)) = \r
+ <i>inl (push A B a b@i) -- r2lPushInl A B C a b = mapOnPath (join A B) (join (join A B) C) inl (inl a) (inr b) (push a b)\r
+\r
+r2lSquare (A B C : U) (a : A) (b : B) (c : C) :\r
+ IdP (<i> Id (join (join A B) C) (inl (push A B a b@i)) (inr c))\r
+ (push (join A B) C (inl a) c) (push (join A B) C (inr b) c)\r
+ = <i j>push (join A B) C (push A B a b@i) c@ j \r
+\r
+opr2l (A : U) (a b c : A) (p : Id A a c) (q : Id A a b)\r
+ (r : Id A b c)\r
+ (sq : Square A a b q c c (refl A c) p r) :\r
+ Square A a a (refl A a) b c r q p = \r
+ <i j>comp A (sq@j@i) [(j=0) -> <k>p@(i/\-k),(i=1) -> <k>p@(j\/-k)]\r
+\r
+r2lPushPush (A B C : U) (a : A) (b : B) (c : C) :\r
+ Square (join (join A B) C)\r
+ (inl (inl a)) (inl (inl a)) (refl (join (join A B) C) (inl (inl a)))\r
+ (inl (inr b)) (inr c) (push (join A B) C (inr b) c)\r
+ (r2lPushInl A B C a b)\r
+ (push (join A B) C (inl a) c) = \r
+ opr2l (join (join A B) C) (inl (inl a)) (inl (inr b)) (inr c)\r
+ (push (join A B) C (inl a) c) (r2lPushInl A B C a b) (push (join A B) C (inr b) c)\r
+ (r2lSquare A B C a b c)\r
+\r
+r2lPush (A B C : U) (a : A) : (bc : join B C) -> Id (join (join A B) C) (inl (inl a)) (r2lInr A B C bc) = split\r
+ inl b -> r2lPushInl A B C a b\r
+ inr c -> push (join A B) C (inl a) c\r
+ pushC b c @ i -> r2lPushPush A B C a b c @ i\r
+\r
+r2l (A B C : U) : join A (join B C) -> join (join A B) C = split\r
+ inl a -> inl (inl a)\r
+ inr bc -> r2lInr A B C bc\r
+ pushC a bc @i -> r2lPush A B C a bc @i\r
+\r
+\r
+\r
+-- Other stuff\r
+\r
+mapJoin (A B C D : U) (f : A -> C) (g : B -> D) : join A B -> join C D = split\r
+ inl a -> inl (f a)\r
+ inr b -> inr (g b)\r
+ pushC a b @i -> push C D (f a) (g b)@i\r
+\r
+-- Suspension and join with the booleans\r
+suspJoin (A : U) : susp A -> join bool A = split\r
+ north -> inl true\r
+ south -> inl false\r
+ merid a @ i -> compId (join bool A) (inl true) (inr a) (inl false)\r
+ (push bool A true a)\r
+ (<i>(push bool A false a)@-i) @ i\r
+\r
+case1 (A:U) : bool -> susp A = split\r
+ false -> south\r
+ true -> north \r
+\r
+suspJoinInv (A : U) : join bool A -> susp A = split\r
+ inl b -> case1 A b\r
+ inr a -> south\r
+ pushC b a @i -> case2 a b @ i\r
+ where case2 (a:A) : (b : bool) -> Id (susp A) (suspJoinInv A (inl b)) south = split\r
+ false -> refl (susp A) south\r
+ true -> <i>merid{susp A} a @i\r
--- /dev/null
+module pi4s3 where
+
+import join
+import hopf
+
+ptJoin (pA : ptType) (B:U) : ptType = (join pA.1 B, inl (pt pA))
+
+ptbool : ptType = (bool,true)
+
+bjbToS1 (x:join bool bool) : S1 = s1ToCircle (suspJoinInv bool x)
+
+bjbToS1Inv (x : S1) : join bool bool = suspJoin bool (circleToS1 x)
+
+-- The map e^-1 from 7.3
+s3ToS1JoinS1Inv (x : join S1 S1) : S3 =
+ suspJoinInv S2
+ (mapJoin bool (join bool S1) bool S2 (\(b:bool) -> b) (suspJoinInv S1)
+ (l2r bool bool S1
+ (mapJoin S1 S1 (join bool bool) S1 bjbToS1Inv (\(z:S1) -> z) x)))
+
+
+-- The map e from 7.3
+s3ToS1JoinS1 (x:S3) : join S1 S1 =
+ mapJoin (join bool bool) S1 S1 S1 bjbToS1 (\(z:S1) -> z)
+ (r2l bool bool S1
+ (mapJoin bool S2 bool (join bool S1) (\(b:bool) -> b) (suspJoin S1)
+ (suspJoin S2 x)))
+
+
+-- A modified version of the main map alpha from 8, which is equal to the
+-- other one (to be checked) but pointed by reflexivity
+alpha : join S1 S1 -> S2 = split
+ inl x -> north
+ inr y -> north
+ pushC x y @ i -> compId S2 north south north (<i>merid{S2} x@i) (<i>merid{S2} y@-i)@i
+
+ptAlpha : ptMap (ptJoin ptS1 S1) ptS2 = (alpha, refl S2 north)
+
+-- Let’s define the twelve maps first
+
+f0 : Z -> loopS1 = loopIt
+
+compInvRight (A:U) (a b:A) (p:Id A a b) : Id (Id A a a) (compId A a b a p (<i>p@-i)) (refl A a) =
+ <i j>comp A (p@-i/\j) [(j=1) -> <k>p@(-k/\-i)]
+
+ptSusp (A : U) : ptType = (susp A, north)
+
+sigma (A : ptType) : ptMap A (Omega (ptSusp A.1))=
+ (s,s0)
+ where s (x:A.1) : Id (susp A.1) north north
+ = compId (susp A.1) north south north
+ (<i>merid{susp A.1} x@i)
+ (<i>(merid{susp A.1} (pt A))@-i)
+
+ s0 : Id (Omega (ptSusp A.1)).1
+ (s (pt A))
+ (refl (susp A.1) north)
+ = compInvRight (susp A.1) north south (<i>merid{susp A.1} (pt A)@i)
+
+f1 : loopS1 -> (itOmega two ptS2).1 = (mapOmega ptS1 (Omega ptS2) (sigma ptS1)).1
+
+f2 : (itOmega two ptS2).1 -> (itOmega three ptS3).1 =
+ (itMapOmega two ptS2 (Omega ptS3) (sigma ptS2)).1
+
+f3 : (itOmega three ptS3).1 -> (itOmega three (ptJoin ptS1 S1)).1
+ = itMapOmegaRefl three ptS3 (join S1 S1) s3ToS1JoinS1
+
+f4 : (itOmega three (ptJoin ptS1 S1)).1 -> (itOmega three ptS2).1
+ = itMapOmegaRefl three (ptJoin ptS1 S1) S2 ptAlpha.1
+
+f5 : (itOmega three ptS2).1 -> (itOmega three (ptJoin ptS1 S1)).1
+ = hopfLoop
+
+oneZ : Z = sucZ zeroZ
+
+-- WORKS
+test0To1 : (itOmega two ptS2).1 = f1 (f0 oneZ)
+
+-- WORKS
+test0To2 : (itOmega three ptS3).1 = f2 test0To1
+
+-- WORKS
+test0To3 : (itOmega three (ptJoin ptS1 S1)).1 = f3 test0To2
+
+-- WORKS
+test0To4 : (itOmega three ptS2).1 = f4 test0To3
+
+-- NOT SURE (takes a long time)
+test0To5 : (itOmega three (ptJoin ptS1 S1)).1 = f5 test0To4
--- /dev/null
+module pointed where\r
+\r
+import nat\r
+import sigma\r
+\r
+-- Pointed types\r
+ptType : U = (X : U) * X\r
+\r
+pt (Z : ptType) : Z.1 = Z.2\r
+\r
+-- Maps between pointed types\r
+isPtMap (A B : ptType) (f : A.1 -> B.1) : U = Id B.1 (f (pt A)) (pt B)\r
+\r
+ptMap (A B : ptType) : U = (f : A.1 -> B.1) * isPtMap A B f\r
+\r
+-- The loop space of a pointed type\r
+Omega (Z : ptType) : ptType = (Id Z.1 (pt Z) (pt Z),refl Z.1 (pt Z))\r
+\r
+kanOp (A : U) (a : A) (p : Id A a a) (b : A) (q : Id A a b) : Id A b b = \r
+ <i>comp A (p@i) [(i=0) -> q, (i=1) -> q]\r
+\r
+kanOpRefl (A : U) (a b : A) (q : Id A a b) : Id (Id A b b) (refl A b) (kanOp A a (refl A a) b q) = \r
+ <i j>comp A (comp A a [(j=0) -> <k>q@(i/\k),(j=1)-> <k>q@(i/\k)]) \r
+ [(j=0)-> <k>q@(i\/k),(j=1)-><k>q@(i\/k), (i=0) -> q]\r
+\r
+mapOmega (A B : ptType) (h : ptMap A B) : ptMap (Omega A) (Omega B) =\r
+ (omf,omf0)\r
+ where a : A.1 = pt A\r
+ b : B.1 = pt B\r
+\r
+ f : A.1 -> B.1 = h.1\r
+ f0 : Id B.1 (f a) b = h.2\r
+\r
+ omf (p : (Omega A).1) : (Omega B).1 = kanOp B.1 (f a) (<i>f (p@i)) b f0\r
+ omf0 : Id (Omega B).1 (omf (refl A.1 a)) (refl B.1 b) = <i>kanOpRefl B.1 (f a) b f0@-i\r
+\r
+-- Simplified mapOmega when the function is pointed by reflexivity\r
+mapOmegaRefl (A : ptType) (B : U) (h : A.1 -> B) (p: (Omega A).1) : (Omega (B, h (pt A))).1 =\r
+ <i>h (p@i)\r
+\r
+-- Iterated loop space\r
+itOmega : nat -> ptType -> ptType = split\r
+ zero -> \ (A:ptType) -> A\r
+ suc n -> \(A:ptType) -> itOmega n (Omega A)\r
+\r
+itMapOmega : (n : nat) (A B : ptType) (h : ptMap A B) -> ptMap (itOmega n A) (itOmega n B) = split\r
+ zero -> \ (A B : ptType) (h : ptMap A B) -> h\r
+ suc n -> \ (A B : ptType) (h : ptMap A B) -> itMapOmega n (Omega A) (Omega B) (mapOmega A B h)\r
+\r
+itMapOmegaRefl : (n : nat) (A : ptType) (B : U) (h : A.1 -> B) -> (itOmega n A).1 -> (itOmega n (B, h (pt A))).1\r
+ = split\r
+ zero -> \ (A : ptType) (B : U) (h : A.1 -> B) -> h\r
+ suc n -> \ (A : ptType) (B : U) (h : A.1 -> B) -> itMapOmegaRefl n (Omega A) (Omega (B, h (pt A))).1 (mapOmegaRefl A B h)\r
+\r
+-- Looping a fibration (9.2)\r
+\r
+fibOmega (B : ptType) (P : B.1 -> U) (f : P (pt B)) (p : (Omega B).1) : U =\r
+ IdS B.1 P (pt B) (pt B) p f f\r
+\r
+totalFibOmega (B : ptType) (P : B.1 -> U) (f : P (pt B)) \r
+ (p : sig (Omega B).1 (fibOmega B P f)) : (Omega (sig B.1 P, (pt B, f))).1\r
+ = <i>(p.1@i,p.2@i) -- pairPath B.1 P (pt B) (pt B) f f p.1 p.2\r
+\r
+itFibOmega : (n : nat) (B : ptType) (P : B.1 -> U) (f : P (pt B)) -> (itOmega n B).1 -> U\r
+ = split\r
+ zero -> \ (B : ptType) (P : B.1 -> U) (f : P (pt B)) -> P\r
+ suc n -> \ (B : ptType) (P : B.1 -> U) (f : P (pt B)) -> itFibOmega n (Omega B) (fibOmega B P f) (refl (P (pt B)) f)\r
+\r
+itTotalFibOmega : (n : nat) (B : ptType) (P : B.1 -> U) (f : P (pt B)) (x:sig (itOmega n B).1 (itFibOmega n B P f)) \r
+ -> (itOmega n (sig B.1 P, (pt B, f))).1\r
+ = split\r
+ zero -> \ (B : ptType) (P : B.1 -> U) (f : P (pt B)) (x:sig B.1 P) -> x\r
+ suc n -> \ (B : ptType) (P : B.1 -> U) (f : P (pt B))\r
+ (x:sig (itOmega n (Omega B)).1 (itFibOmega n (Omega B) (fibOmega B P f) (refl (P (pt B)) f))) -> \r
+ let\r
+ BOm : ptType = Omega B\r
+ POm : BOm.1 -> U = fibOmega B P f\r
+ fOm : Id (P (pt B)) f f = refl (P (pt B)) f\r
+ ih : (sig (itOmega n BOm).1 (itFibOmega n BOm POm fOm)) ->\r
+ (itOmega n (sig BOm.1 POm, (pt BOm, fOm))).1\r
+ = itTotalFibOmega n (Omega B) (fibOmega B P f) (refl (P (pt B)) f)\r
+ in (itMapOmega n (sig BOm.1 POm, (pt BOm, fOm))\r
+ (Omega (sig B.1 P, (pt B, f)))\r
+ (totalFibOmega B P f,\r
+ refl (Omega (sig B.1 P, (pt B, f))).1\r
+ (refl (sig B.1 P) (pt B, f)))).1\r
+ (ih x)\r
+\r
+-- TODO: better name!\r
+-- isContr : U -> U\r
+-- isContr A = (a : A) * ((x : A) -> Id A a x)\r
+\r
+inhOrTrunc (A:U) : nat -> U = split\r
+ zero -> A\r
+ suc n -> (x y : A) -> inhOrTrunc (Id A x y) n\r
+\r
+truncFibOmega (B : ptType) (P : B.1 -> U) (f : P (pt B)) (n : nat) \r
+ (tr:inhOrTrunc (P (pt B)) (suc n)) (p : (Omega B).1) : inhOrTrunc (fibOmega B P f p) n \r
+ = substInv U (\ (X:U) -> inhOrTrunc X n)\r
+ (IdS B.1 P (pt B) (pt B) p f f) (Id (P (pt B)) (subst B.1 P (pt B) (pt B) p f) f)\r
+ (funDepTr (P (pt B)) (P (pt B)) (<i>P (p@i)) f f) (tr (subst B.1 P (pt B) (pt B) p f) f)\r
projects / cubicaltt.git / commitdiff