From: Anders Mörtberg Date: Sun, 9 Jul 2017 22:58:17 +0000 (+0200) Subject: pi4s3 (first 5 maps) X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=e1e158d2103f0b441ed27ad4b2c0c123d7d710d7;p=cubicaltt.git pi4s3 (first 5 maps) --- diff --git a/examples/brunerie.ctt b/examples/brunerie.ctt new file mode 100644 index 0000000..d09daff --- /dev/null +++ b/examples/brunerie.ctt @@ -0,0 +1,412 @@ +module brunerie where + +data bool = false | true +data nat = zero | suc (n : nat) + +idfun (A : U) (a : A) : A = a + +{- Z is represented as: + + +2 = pos (suc (suc zero)) + +1 = pos (suc zero) + 0 = pos zero + -1 = neg zero + -2 = neg (suc zero) + +-} +data Z = pos (n : nat) | neg (n : nat) + +twoZ : Z = pos (suc (suc zero)) +oneZ : Z = pos (suc zero) +zeroZ : Z = pos zero +moneZ : Z = neg zero +mtwoZ : Z = neg (suc zero) + +Path (A : U) (a0 a1 : A) : U = PathP ( A) a0 a1 + +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 + +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 ] + +-- p ; p^-1 = 1 +compPathInv (A : U) (a b : A) (p : Path A a b) : + Path (Path A a a) (compPath A a b a p ( p @ -i)) (<_> a) = + comp (<_> A) (p @ j /\ -k) + [ (j = 0) -> <_> a + , (j = 1) -> p @ -i /\ -k + , (k = 1) -> <_> a ] + +-- p^-1 ; p = 1 +compInvPath (A : U) (a b : A) (p : Path A a b) : + Path (Path A b b) (compPath A b a b ( p @ -i) p) (<_> b) = + comp (<_> A) (p @ -i \/ j) + [ (i = 0) -> <_> b + , (j = 1) -> <_> b + , (i = 1) -> p @ j \/ k ] + + +-------------------------------------------------------------------------------- +-- B.3 Suspension and spheres + +-- The circle +data S1 = base + | loop [ (i=0) -> base + , (i=1) -> base] + +loopS1 : U = Path S1 base base +loopP : loopS1 = loop{S1} @ i +invLoop : loopS1 = loopP @ -i +compS1 : loopS1 -> loopS1 -> loopS1 = compPath S1 base base base + +triv : loopS1 = base +oneTurn (l : loopS1) : loopS1 = compS1 l loopP +backTurn (l : loopS1) : loopS1 = compS1 l invLoop + +itLoop : nat -> loopS1 = split + zero -> triv + suc n -> oneTurn (itLoop n) + +itLoopNeg : nat -> loopS1 = split + zero -> invLoop + suc n -> backTurn (itLoopNeg n) + +loopIt : Z -> loopS1 = split + pos n -> itLoop n + neg n -> itLoopNeg n + +-- Suspension +data susp (A : U) = north + | south + | merid (a : A) [ (i=0) -> north + , (i=1) -> south ] + +meridP (A : U) (a : A) : Path (susp A) north south = + merid{susp A} a @ i + + +-- The 2 and 3 spheres. Maybe define directly instead? +S2 : U = susp S1 +S3 : U = susp S2 + + +-------------------------------------------------------------------------------- +-- B.4 Pointed types, pointed maps and loop spaces + +-- Pointed types +ptType : U = (A : U) * A +pt (A : ptType) : A.1 = A.2 + +boolpt : ptType = (bool,true) +susppt (A : U) : ptType = (susp A,north) +S1pt : ptType = (S1,base) +S2pt : ptType = susppt S1 +S3pt : ptType = susppt S2 + +ptMap (A B : ptType) : U = (f : A.1 -> B.1) * (Path B.1 (f (pt A)) (pt B)) + +-- The first 3 loop spaces of a pointed type. +-- TODO: Maybe defined these by induction on n as in experiments/pointed.ctt? +Omega (A : ptType) : ptType = (Path A.1 (pt A) (pt A),<_> pt A) +Omega2 (A : ptType) : ptType = Omega (Omega A) +Omega3 (A : ptType) : ptType = Omega2 (Omega A) + +kanOp (A : U) (a : A) (p : Path A a a) (b : A) (q : Path A a b) : Path A b b = + comp (<_> A) (p @ i) [ (i = 0) -> q, (i = 1) -> q ] + +kanOpRefl (A : U) (a b : A) (q : Path A a b) : + Path (Path A b b) (kanOp A a ( a) b q) (<_> b) = + comp (<_> A) (q @ j) [ (i = 0) -> q @ j \/ k + , (i = 1) -> q @ j \/ k + , (j = 1) -> b ] + +mapOmega (A B : ptType) (f : ptMap A B) : ptMap (Omega A) (Omega B) = (g,pg) + where + g (p : (Omega A).1) : (Omega B).1 = + kanOp B.1 (f.1 (pt A)) (f.1 (p@i)) (pt B) f.2 + pg : Path (Omega B).1 (g (pt (Omega A))) (pt (Omega B)) = + kanOpRefl B.1 (f.1 (pt A)) (pt B) f.2 + +mapOmega2 (A B : ptType) (f : ptMap A B) : ptMap (Omega2 A) (Omega2 B) = + mapOmega (Omega A) (Omega B) (mapOmega A B f) + +mapOmega3 (A B : ptType) (f : ptMap A B) : ptMap (Omega3 A) (Omega3 B) = + mapOmega (Omega2 A) (Omega2 B) (mapOmega2 A B f) + +-- Simplified mapOmega when the function is pointed by reflexivity +mapOmegaRefl (A : ptType) (B : U) (h : A.1 -> B) (p : (Omega A).1) : + (Omega (B, h (pt A))).1 = h (p @ i) + +mapOmegaRefl2 (A : ptType) (B : U) (h : A.1 -> B) (p : (Omega2 A).1) : + (Omega2 (B, h (pt A))).1 = h (p @ i @ j) + -- mapOmegaRefl (Omega A) (Omega (B,h (pt A))).1 (mapOmegaRefl A B h) p + +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 + +phi (A : ptType) : ptMap A (Omega (susppt A.1)) = (g,pg) + where + g (a : A.1) : (Omega (susppt A.1)).1 = + let p1 : Path (susp A.1) north south = meridP A.1 a + p2 : Path (susp A.1) south north = meridP A.1 (pt A) @ -i + in compPath (susp A.1) north south north p1 p2 + pg : Path (Omega (susppt A.1)).1 (g (pt A)) (pt (Omega (susppt A.1))) = + let p : Path (Path (susp A.1) north north) (g (pt A)) (<_> north) = + compPathInv (susp A.1) north south (meridP A.1 (pt A)) + in p + + +-------------------------------------------------------------------------------- +-- B.6 The 3-sphere and the join of two circles + +data join (A B : U) = inl (a : A) + | inr (b : B) + | push (a : A) (b : B) [ (i = 0) -> inl a + , (i = 1) -> inr b ] + +pushP (A B : U) (a : A) (b : B) : Path (join A B) (inl a) (inr b) = + push {join A B} a b @ i + +joinpt (A : ptType) (B : U) : ptType = (join A.1 B,inl (pt A)) + + +-- B.6.1 Join and associativity + +r2lInr (A B C : U) : join B C -> join (join A B) C = split + inl b -> inl (inr b) + inr c -> inr c + push b c @ i -> pushP (join A B) C (inr b) c @ i + +r2lPushInl (A B C : U) (a : A) (b : B) : + Path (join (join A B) C) (inl (inl a)) (inl (inr b)) = inl (pushP A B a b @ i) + +r2lSquare (A B C : U) (a : A) (b : B) (c : C) : + PathP ( Path (join (join A B) C) (inl (pushP A B a b @ i)) (inr c)) + (pushP (join A B) C (inl a) c) (pushP (join A B) C (inr b) c) + = pushP (join A B) C (pushP A B a b @ i) c @ j + +opr2l (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 b c c q (<_> c) p r) : + Square A a a b c (<_> a) r q p = + comp (<_> A) (p @ i) [ (i = 0) -> q @ j /\ k + , (i = 1) -> p @ j \/ -k + , (j = 0) -> p @ i /\ -k + , (j = 1) -> sq @ k @ i ] + +r2lPushPush (A B C : U) (a : A) (b : B) (c : C) : + Square (join (join A B) C) (inl (inl a)) (inl (inl a)) (inl (inr b)) (inr c) + (<_> inl (inl a)) (pushP (join A B) C (inr b) c) + (r2lPushInl A B C a b) (pushP (join A B) C (inl a) c) = + opr2l (join (join A B) C) (inl (inl a)) (inl (inr b)) (inr c) + (pushP (join A B) C (inl a) c) (r2lPushInl A B C a b) + (pushP (join A B) C (inr b) c) (r2lSquare A B C a b c) + +r2lPush (A B C : U) (a : A) : + (bc : join B C) -> Path (join (join A B) C) (inl (inl a)) (r2lInr A B C bc) = split + inl b -> r2lPushInl A B C a b + inr c -> pushP (join A B) C (inl a) c + push b c @ i -> r2lPushPush A B C a b c @ i + +joinassoc1 (A B C : U) : join A (join B C) -> join (join A B) C = split + inl a -> inl (inl a) + inr bc -> r2lInr A B C bc + push a bc @ i -> r2lPush A B C a bc @ i + + +-- 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 + + +mapJoin (A A' B B' : U) (f : A -> A') (g : B -> B') : join A B -> join A' B' = split + inl a -> inl (f a) + 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 + +psi (A : U) : susp A -> join bool A = split + north -> inl true + south -> inl false + merid a @ i -> compPath (join bool A) (inl true) (inr a) (inl false) + (pushP bool A true a) ( pushP bool A false a @ -i) @ i + +psiinv (A : U) : join bool A -> susp A = split + inl b -> + let case : (b : bool) -> susp A = split + false -> south + true -> north + in case b + inr a -> south + push b a @ i -> + let case (a : A) : (b : bool) -> Path (susp A) (psiinv A (inl b)) south = 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? + +suspBoolToS1 : susp bool -> S1 = split + north -> base + south -> base + merid b @ i -> + let case : bool -> Path S1 base base = split + false -> loopP + true -> <_> base + in case b @ i + +s1ToSuspBool : S1 -> susp bool = split + base -> north + loop @ i -> compPath (susp bool) north south north + (meridP bool false) ( meridP bool true @ -i) @ i + +c (x : join bool bool) : S1 = suspBoolToS1 (psiinv bool x) + +cinv (x : S1) : join bool bool = psi bool (s1ToSuspBool x) + +-- B.6.3 Equivalence between S3 and join S1 S1 + +-- The map e +e (x : S3) : join S1 S1 = + let x1 : join bool S2 = psi S2 x + x2 : join bool (join bool S1) = + mapJoin bool bool S2 (join bool S1) (idfun bool) (psi S1) x1 + x3 : join (join bool bool) S1 = joinassoc1 bool bool S1 x2 + res : join S1 S1 = mapJoin (join bool bool) S1 S1 S1 c (idfun S1) x3 + in res + +-- einv : join S1 S1 -> S3 = undefined + + +-------------------------------------------------------------------------------- +-- B.7 The main map + +-- A modified version of the main map alpha, which is equal to the +-- other one (to be checked) but pointed by reflexivity +prealpha : join S1 S1 -> S2 = split + inl x -> north + inr y -> north + push x y @ i -> + -- A: I think there must be a bug in the old version when + -- typechecking path constructors (we use merid{S2} there...) + compPath S2 north south north (meridP S1 x) ( meridP S1 y @ -i) @ i + +alpha : ptMap (joinpt S1pt S1) S2pt = (prealpha, <_> north) + + + +-------------------------------------------------------------------------------- +-- B.8 The map defining pi3(S2) + +-- B.8.1 The Hopf fibration + +-- B.8.2 Looping a fibration + +-- B.8.3 Looping the Hopf fibration + +h : ptMap (Omega3 S2pt) (Omega3 (joinpt S1pt S1)) = undefined + + + + + +-------------------------------------------------------------------------------- +-- B.2 The definition + +f0 : Z -> loopS1 = loopIt + +f1 : loopS1 -> (Omega2 S2pt).1 = (mapOmega S1pt (Omega S2pt) (phi S1pt)).1 + +f2 : (Omega2 S2pt).1 -> (Omega3 S3pt).1 = (mapOmega2 S2pt (Omega S3pt) (phi S2pt)).1 + +f3 : (Omega3 S3pt).1 -> (Omega3 (joinpt S1pt S1)).1 = mapOmegaRefl3 S3pt (join S1 S1) e + +-- Decompose f3 and test the 3 first submaps separately: +f31 : (Omega3 S3pt).1 -> (Omega3 (joinpt boolpt S2)).1 = + mapOmegaRefl3 S3pt (join bool S2) (psi S2) + +f32 : (Omega3 S3pt).1 -> (Omega3 (joinpt boolpt (join bool S1))).1 = + mapOmegaRefl3 S3pt (join bool (join bool S1)) + (\(x : S3) -> mapJoin bool bool S2 (join bool S1) (idfun bool) (psi S1) + (psi S2 x)) + +f33 : (Omega3 S3pt).1 -> (Omega3 (joinpt (joinpt boolpt bool) S1)).1 = + mapOmegaRefl3 S3pt (join (join bool bool) S1) + (\(x : S3) -> joinassoc1 bool bool S1 + (mapJoin bool bool S2 (join bool S1) (idfun bool) (psi S1) + (psi S2 x))) + +f4 : (Omega3 (joinpt S1pt S1)).1 -> (Omega3 S2pt).1 = + -- (mapOmega3 (joinpt S1pt S1) S2pt alpha).1 + mapOmegaRefl3 (joinpt S1pt S1) S2 alpha.1 + + +-- WORKS +test0To1 : (Omega2 S2pt).1 = f1 (f0 oneZ) + +-- WORKS +test0To2 : (Omega3 S3pt).1 = f2 test0To1 + +-- WORKS +test0To31 : (Omega3 (joinpt boolpt S2)).1 = f31 test0To2 + +-- WORKS +test0To32 : (Omega3 (joinpt boolpt (join bool S1))).1 = f32 test0To2 + +-- WORKS +test0To33 : (Omega3 (joinpt (joinpt boolpt bool) S1)).1 = f33 test0To2 + +-- WORKS (~2min) +test0To3 : (Omega3 (joinpt S1pt S1)).1 = f3 test0To2 + +-- WORKS (2m54s) +test0To4 : (Omega3 S2pt).1 = f4 test0To3