From: Anders Mörtberg Date: Mon, 4 May 2015 23:55:45 +0000 (+0200) Subject: Add pi4s3 until test0To5 X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=bfc8a84d5ec467ebf5f11f2a55e7fa6cd54f762b;p=cubicaltt.git Add pi4s3 until test0To5 --- diff --git a/examples/hopf.ctt b/examples/hopf.ctt index b4a02f4..d3a8f47 100644 --- a/examples/hopf.ctt +++ b/examples/hopf.ctt @@ -1,10 +1,60 @@ -module hopf where - -import truncS2 -import mult - -hopf : S2 -> U = split - north -> S1 - south -> S1 - merid x @ i -> eqS1 x @ i - +module hopf where + +import truncS2 +import mult +import pointed +import join + +hopf : S2 -> U = split + north -> S1 + south -> S1 + merid x @ i -> eqS1 x @ i + +funExt1 (C B : U) (F : C -> U) (a :C) : (b : C) (p : Id C a b) + (f : F a -> B) (g : F b -> B) + (h : (x : F a) -> Id B (f x) (g (subst C F a b p x))) + -> IdS C (\ (z:C) -> F z -> B) a b p f g = + J C a (\ (b:C) (p:Id C a b) -> (f : F a -> B) (g : F b -> B) + (h : (x : F a) -> Id B (f x) (g (subst C F a b p x))) + -> IdS C (\ (z:C) -> F z -> B) a b p f g) rem + where rem (f g : F a -> B) (h : (x : F a) -> Id B (f x) (g x)) : Id (F a -> B) f g = + \(x:F a) -> h x @ i + +t : (x : S2) -> hopf x -> join S1 S1 = split + north -> \ (a:S1) -> inl a + south -> \ (a:S1) -> inr a + merid x @ i -> funExt1 S2 (join S1 S1) hopf north south (merid{S2} x@j) (\ (y:S1) -> inl y) (\ (y:S1) -> inr y) + (\ (y:S1) -> pushC{join S1 S1} y (mult x y)@j) @ i + +totalHopfToJoin (xy:(x : S2) * hopf x) : join S1 S1 = t xy.1 xy.2 + +one : nat = suc zero +two : nat = suc one +three : nat = suc two + +S3 : U = susp S2 +ptS3 : ptType = (S3,north) +ptS2 : ptType = (S2,north) +ptS1 : ptType = (S1,base) + +hopfOne : (itOmega one ptS2).1 -> U = itFibOmega one ptS2 hopf base + +hopfTwo : (itOmega two ptS2).1 -> U = itFibOmega two ptS2 hopf base + +hopfThree : (itOmega three ptS2).1 -> U = itFibOmega three ptS2 hopf base + +ptJoin (pA:ptType) (B:U) : ptType = (join pA.1 B, inl (pt pA)) + +fibContrHopfThree (p : (itOmega three ptS2).1) : hopfThree p = + truncFibOmega (itOmega two ptS2) hopfTwo (refl (Id S1 base base) (refl S1 base)) zero + (truncFibOmega (Omega ptS2) hopfOne (refl S1 base) one + (truncFibOmega ptS2 hopf base two isGroupoidS1 (refl S2 north)) + (refl (Omega ptS2).1 (pt (Omega ptS2)))) p + + +-- The map h from 9.3 +hopfLoop (p : (itOmega three ptS2).1) : (itOmega three (ptJoin ptS1 S1)).1 = + itMapOmegaRefl three (Sigma S2 hopf, (north,base)) (join S1 S1) totalHopfToJoin + (itTotalFibOmega three ptS2 hopf base (p, fibContrHopfThree p)) + + diff --git a/examples/join.ctt b/examples/join.ctt new file mode 100644 index 0000000..62cec98 --- /dev/null +++ b/examples/join.ctt @@ -0,0 +1,119 @@ +module join where + +import prelude +import susp + +data join (A B:U) = inl (a:A) | inr (b:B) | pushC (a:A) (b:B) [(i=0) -> inl a, (i=1) -> inr b] + +push (A B:U) (a:A) (b:B) : Id (join A B) (inl a) (inr b) = pushC{join A B} a b@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) + pushC a b @ i -> push A (join B C) a (inl b) @ i + +l2rPushInr (A B C : U) (b : B) (c : C) : Id (join A (join B C)) (inr (inl b)) (inr (inr c)) = + inr (push B C b c@i) + +l2rSquare (A B C : U) (a : A) (b : B) (c : C) : + IdP ( Id (join A (join B C)) (inl a) (inr (push B C b c@i))) + (push A (join B C) a (inl b)@i) (push A (join B C) a (inr c)@i) = + push A (join B C) a (push B C b c@i)@j + +opl2r (A : U) (a b c : A) (p : Id A a c) (q : Id A a b) (r : Id A b c) + (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 = + 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)) (push A (join B C) a (inl b)) + (inr (inr c)) (inr (inr c)) (refl (join A (join B C)) (inr (inr c))) + (push 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)) + (push A (join B C) a (inr c)) (push 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) -> + Id (join A (join B C)) (l2rInl A B C u) (inr (inr c)) = split + inl a -> push A (join B C) a (inr c) + inr b -> l2rPushInr A B C b c + pushC a b @ i -> l2rPushPush A B C a b c @ i + +l2r (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) + pushC p q @i -> l2rPush A B C q p @i + + +-- Map from [join A (join B C)] to [join (join A B) C] + +r2lInr (A B C : U) : join B C -> join (join A B) C = split + inl b -> inl (inr b) + inr c -> inr c + pushC b c @i -> push (join A B) C (inr b) c @i + +r2lPushInl (A B C : U) (a : A) (b : B) : Id (join (join A B) C) (inl (inl a)) (inl (inr b)) = + 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) + +r2lSquare (A B C : U) (a : A) (b : B) (c : C) : + IdP ( Id (join (join A B) C) (inl (push A B a b@i)) (inr c)) + (push (join A B) C (inl a) c) (push (join A B) C (inr b) c) + = push (join A B) C (push A B a b@i) c@ j + +opr2l (A : U) (a b c : A) (p : Id A a c) (q : Id A a b) + (r : Id A b c) + (sq : Square A a b q c c (refl A c) p r) : + Square A a a (refl A a) b c r q p = + comp A (sq@j@i) [(j=0) -> p@(i/\-k),(i=1) -> p@(j\/-k)] + +r2lPushPush (A B C : U) (a : A) (b : B) (c : C) : + Square (join (join A B) C) + (inl (inl a)) (inl (inl a)) (refl (join (join A B) C) (inl (inl a))) + (inl (inr b)) (inr c) (push (join A B) C (inr b) c) + (r2lPushInl A B C a b) + (push (join A B) C (inl a) c) = + opr2l (join (join A B) C) (inl (inl a)) (inl (inr b)) (inr c) + (push (join A B) C (inl a) c) (r2lPushInl A B C a b) (push (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) -> Id (join (join A B) C) (inl (inl a)) (r2lInr A B C bc) = split + inl b -> r2lPushInl A B C a b + inr c -> push (join A B) C (inl a) c + pushC b c @ i -> r2lPushPush A B C a b c @ i + +r2l (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 + pushC a bc @i -> r2lPush A B C a bc @i + + + +-- Other stuff + +mapJoin (A B C D : U) (f : A -> C) (g : B -> D) : join A B -> join C D = split + inl a -> inl (f a) + inr b -> inr (g b) + pushC a b @i -> push C D (f a) (g b)@i + +-- Suspension and join with the booleans +suspJoin (A : U) : susp A -> join bool A = split + north -> inl true + south -> inl false + merid a @ i -> compId (join bool A) (inl true) (inr a) (inl false) + (push bool A true a) + ((push bool A false a)@-i) @ i + +case1 (A:U) : bool -> susp A = split + false -> south + true -> north + +suspJoinInv (A : U) : join bool A -> susp A = split + inl b -> case1 A b + inr a -> south + pushC b a @i -> case2 a b @ i + where case2 (a:A) : (b : bool) -> Id (susp A) (suspJoinInv A (inl b)) south = split + false -> refl (susp A) south + true -> merid{susp A} a @i diff --git a/examples/pi4s3.ctt b/examples/pi4s3.ctt new file mode 100644 index 0000000..9b17e30 --- /dev/null +++ b/examples/pi4s3.ctt @@ -0,0 +1,89 @@ +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 (merid{S2} x@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 (p@-i)) (refl A a) = + comp A (p@-i/\j) [(j=1) -> 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 + (merid{susp A.1} x@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 (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 diff --git a/examples/pointed.ctt b/examples/pointed.ctt new file mode 100644 index 0000000..273b99e --- /dev/null +++ b/examples/pointed.ctt @@ -0,0 +1,101 @@ +module pointed where + +import nat +import sigma + +-- Pointed types +ptType : U = (X : U) * X + +pt (Z : ptType) : Z.1 = Z.2 + +-- Maps between pointed types +isPtMap (A B : ptType) (f : A.1 -> B.1) : U = Id B.1 (f (pt A)) (pt B) + +ptMap (A B : ptType) : U = (f : A.1 -> B.1) * isPtMap A B f + +-- The loop space of a pointed type +Omega (Z : ptType) : ptType = (Id Z.1 (pt Z) (pt Z),refl Z.1 (pt Z)) + +kanOp (A : U) (a : A) (p : Id A a a) (b : A) (q : Id A a b) : Id A b b = + comp A (p@i) [(i=0) -> q, (i=1) -> q] + +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) = + comp A (comp A a [(j=0) -> q@(i/\k),(j=1)-> q@(i/\k)]) + [(j=0)-> q@(i\/k),(j=1)->q@(i\/k), (i=0) -> q] + +mapOmega (A B : ptType) (h : ptMap A B) : ptMap (Omega A) (Omega B) = + (omf,omf0) + where a : A.1 = pt A + b : B.1 = pt B + + f : A.1 -> B.1 = h.1 + f0 : Id B.1 (f a) b = h.2 + + omf (p : (Omega A).1) : (Omega B).1 = kanOp B.1 (f a) (f (p@i)) b f0 + omf0 : Id (Omega B).1 (omf (refl A.1 a)) (refl B.1 b) = kanOpRefl B.1 (f a) b f0@-i + +-- 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) + +-- Iterated loop space +itOmega : nat -> ptType -> ptType = split + zero -> \ (A:ptType) -> A + suc n -> \(A:ptType) -> itOmega n (Omega A) + +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) + +itMapOmegaRefl : (n : nat) (A : ptType) (B : U) (h : A.1 -> B) -> (itOmega n A).1 -> (itOmega n (B, h (pt A))).1 + = split + zero -> \ (A : ptType) (B : U) (h : A.1 -> B) -> h + suc n -> \ (A : ptType) (B : U) (h : A.1 -> B) -> itMapOmegaRefl n (Omega A) (Omega (B, h (pt A))).1 (mapOmegaRefl A B h) + +-- Looping a fibration (9.2) + +fibOmega (B : ptType) (P : B.1 -> U) (f : P (pt B)) (p : (Omega B).1) : U = + IdS B.1 P (pt B) (pt B) p f f + +totalFibOmega (B : ptType) (P : B.1 -> U) (f : P (pt B)) + (p : sig (Omega B).1 (fibOmega B P f)) : (Omega (sig B.1 P, (pt B, f))).1 + = (p.1@i,p.2@i) -- pairPath B.1 P (pt B) (pt B) f f p.1 p.2 + +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) (refl (P (pt B)) f) + +itTotalFibOmega : (n : nat) (B : ptType) (P : B.1 -> U) (f : P (pt B)) (x:sig (itOmega n B).1 (itFibOmega n B P f)) + -> (itOmega n (sig B.1 P, (pt B, f))).1 + = split + zero -> \ (B : ptType) (P : B.1 -> U) (f : P (pt B)) (x:sig B.1 P) -> x + suc n -> \ (B : ptType) (P : B.1 -> U) (f : P (pt B)) + (x:sig (itOmega n (Omega B)).1 (itFibOmega n (Omega B) (fibOmega B P f) (refl (P (pt B)) f))) -> + let + BOm : ptType = Omega B + POm : BOm.1 -> U = fibOmega B P f + fOm : Id (P (pt B)) f f = refl (P (pt B)) f + ih : (sig (itOmega n BOm).1 (itFibOmega n BOm POm fOm)) -> + (itOmega n (sig BOm.1 POm, (pt BOm, fOm))).1 + = itTotalFibOmega n (Omega B) (fibOmega B P f) (refl (P (pt B)) f) + in (itMapOmega n (sig BOm.1 POm, (pt BOm, fOm)) + (Omega (sig B.1 P, (pt B, f))) + (totalFibOmega B P f, + refl (Omega (sig B.1 P, (pt B, f))).1 + (refl (sig B.1 P) (pt B, f)))).1 + (ih x) + +-- TODO: better name! +-- isContr : U -> U +-- isContr A = (a : A) * ((x : A) -> Id A a x) + +inhOrTrunc (A:U) : nat -> U = split + zero -> A + suc n -> (x y : A) -> inhOrTrunc (Id A x y) n + +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 + = substInv U (\ (X:U) -> inhOrTrunc X n) + (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) + (funDepTr (P (pt B)) (P (pt B)) (P (p@i)) f f) (tr (subst B.1 P (pt B) (pt B) p f) f)