Permalink
Fetching contributors…
Cannot retrieve contributors at this time
329 lines (249 sloc) 14.8 KB
-- The loop space of the circle is equal to Z
module helix where
import circle
import equiv
import pi
oneTurn (l: loopS1) : loopS1 = compS1 l loop1
backTurn (l: loopS1) : loopS1 = compS1 l invLoop
compInv (A:U) (a:A) : (x:A) (p:Path A a x) -> Path (Path A x x) (<_>x) (compPath A x a x (<i>p@-i) p) =
J A a (\ (x:A) (p:Path A a x) -> Path (Path A x x) (<_>x) (compPath A x a x (<i>p@-i) p)) rem
where rem : Path (Path A a a) (<_>a) (<i>comp (<_>A) a [(i=0) -> <_>a,(i=1) -> <_>a]) =
<j i>comp (<_>A) a [(j=0) -> <_>a,(i=0) -> <_>a,(i=1) -> <_>a]
compInvS1 : Path loopS1 (refl S1 base) (compS1 invLoop loop1) = compInv S1 base base loop1
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) (<i>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) (<i>p@-i))) rem
where rem : Path (Path A a b) q
(<i>comp (<_>A) (comp (<_>A) (q@i) [(i=0) -> <_>a,(i=1) -> <_>b]) [(i=0) -> <_>a,(i=1) -> <_>b]) =
<j i>comp (<_>A) (comp (<_>A) (q@i) [(j=0) -> <_>q@i,(i=0) -> <_>a,(i=1) -> <_>b]) [(j=0) -> <_>q@i,(i=0) -> <_>a,(i=1) -> <_>b]
-- constant transport
transC (A:U) (a:A) : A = comp (<_>A) a []
-- it is equal to the identity function
lemTransC (A:U) (a:A) : Path A (transC A a) a = <i>comp (<_>A) a [(i=1) -> <_>a]
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 (<i>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 (<i>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) -> transC (G a) (fa u)) (\ (u:F a) -> ga (transC (F a) u)))
(Path (F a -> G a) fa ga) =
<j>Path (F a -> G a) (\ (u:F a) -> lemTransC (G a) (fa u)@j) (\ (u : F a) -> ga (lemTransC (F a) u@j))
-- special case
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 (<i>F (p@i) -> G (p@i)) fa ga =
comp (lemFib1 A F G a fa a p ga) (<i>\ (u:F a) -> h u@i) []
compPathL (A:U) (a b:A) (p : Path A a b) : Path (Path A a b) p (compPath A a b b p (<_>b)) =
<j i>comp (<_>A) (p @ i) [(i=0) -> <_> a, (i = 1) -> <_>b, (j=0) -> <_>(p@i) ]
lemFib2 (A:U) (F:A->U) (a b:A) (p:Path A a b) (u:F a) :
(c:A) (q:Path A b c) -> Path (F c) (subst A F b c q (subst A F a b p u)) (subst A F a c (compPath A a b c p q) u) =
J A b (\ (c:A) (q:Path A b c) -> Path (F c) (subst A F b c q (subst A F a b p u)) (subst A F a c (compPath A a b c p q) u))
rem
where
rem1 : Path (F b) (subst A F a b p u) (subst A F b b (<_>b) (subst A F a b p u)) = <i>lemTransC (F b) (subst A F a b p u)@-i
rem2 : Path (F b) (subst A F a b p u) (subst A F a b (compPath A a b b p (<_>b)) u) =
<i>subst A F a b (compPathL A a b p@i) u
rem : Path (F b) (subst A F b b (<_>b) (subst A F a b p u)) (subst A F a b (compPath A a b b p (<_>b)) u) =
comp (<i>Path (F b) (rem1@i) (rem2@i)) (<_>subst A F a b p u) []
testIsoPath (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) (a:A) : Path B (f a) (trans A B (isoPath A B f g s t) a) =
<i>comp (<_>B) (comp (<_>B) (f a) [(i=0) -> <_> f a]) [(i=0) -> <_> f a]
testH (n:Z) : Z = subst S1 helix base base loop1 n
testHelix : Path (Z->Z) sucZ (subst S1 helix base base loop1) =
<i>\(n:Z) -> testIsoPath Z Z sucZ predZ sucpredZ predsucZ n@i
encode (x:S1) (p:Path S1 base x) : helix x = subst S1 helix base x p zeroZ
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
inl n -> itLoopNeg n
inr n -> itLoop n
lemItNeg : (n:nat) -> Path loopS1 (transport (<i>Path S1 base (loop{S1} @ i)) (loopIt (inl n))) (loopIt (sucZ (inl n))) = split
zero -> lemInv S1 base base loop1
suc n -> lemCompInv S1 base base base (itLoopNeg n) invLoop
l0 : loopS1 = <i>base
l1 : loopS1 = oneTurn l0
test1ItPos (n:nat) : U = Path loopS1 (loopIt (sucZ (inr n))) (oneTurn ((loopIt (inr n))))
lem1ItPos : (n:nat) -> Path loopS1 (loopIt (sucZ (inr n))) (oneTurn ((loopIt (inr n)))) = split
zero -> refl loopS1 l1
suc p -> <i>oneTurn (lem1ItPos p@i)
test1ItNeg (n:nat) : U = Path loopS1 (loopIt (sucZ (inl n))) (oneTurn ((loopIt (inl n))))
lem1ItNeg : (n:nat) -> Path loopS1 (loopIt (sucZ (inl n))) (oneTurn (loopIt (inl n))) = split
zero -> compInvS1
suc p -> compInv S1 base base (loopIt (inl p)) base invLoop
lem1It : (n:Z) -> Path loopS1 (loopIt (sucZ n)) (oneTurn (loopIt n)) = split
inl n -> lem1ItNeg n
inr n -> lem1ItPos n
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 = <j> helix (loop1@j) -> Path S1 base (loop1@j)
rem2 (n:Z) : Path loopS1 (oneTurn (loopIt n)) (loopIt (sucZ n)) = <i>lem1It n@-i
rem1 (n:Z) : Path loopS1 (subst S1 G base base loop1 (loopIt n)) (loopIt (subst S1 helix base base loop1 n)) =
comp (<i> Path loopS1 (oneTurn (loopIt n)) (loopIt (testHelix@i n))) (rem2 n) []
rem : PathP p loopIt loopIt = corFib1 S1 helix G base loopIt loopIt loop1 rem1
encodeDecode (x:S1) (p : Path S1 base x) : Path (Path S1 base x) (decode x (encode x p)) p =
transport (<i>Path (Path S1 base (p@i)) (decode (p@i) (encode (p@i) (<j>p@(i/\j)))) (<j>p@(i/\j))) (refl loopS1 triv)
-- encodeDecode : (c : S1) (p : Path S1 base c) -> Path (Path S1 base c) (decode c (encode c p)) p =
-- J S1 base (\ (c : S1) (p : Path S1 base c) -> Path (Path S1 base c) (decode c (encode c p)) p)
-- (<_> (<_> base))
lemTransOneTurn (n:nat) : Path Z (transport (<i>helix (loop1@i)) (inr n)) (inr (suc n)) =
<i>inr (suc (comp (<_>nat) (comp (<_>nat) n [(i=1) -> <_>n]) [(i=1) -> <_>n]))
lemTransBackTurn (n:nat) : Path Z (transport (<i>helix (loop1@-i)) (inl n)) (inl (suc n)) =
<i>inl (suc (comp (<_>nat) (comp (<_>nat) n [(i=1) -> <_>n]) [(i=1) -> <_>n]))
corFib2 (u:Z) (l:loopS1) : Path Z (transport (<i>helix (oneTurn l@i)) u)
(transport (<i>helix (loop1@i)) (transport (<i>helix (l@i)) u)) =
<i>lemFib2 S1 helix base base l u base loop1@-i
corFib3 (u:Z) (l:loopS1) : Path Z (transport (<i>helix (backTurn l@i)) u)
(transport (<i>helix (loop1@-i)) (transport (<i>helix (l@i)) u)) =
<i>lemFib2 S1 helix base base l u base (<j>loop1@-j)@-i
decodeEncodeBasePos : (n : nat) -> Path Z (transport (<x> helix (itLoop n @ x)) (inr zero)) (inr n) = split
zero -> <_> inr zero
suc n -> comp (<j>Path Z (transport (<i>helix (oneTurn l@i)) (inr zero)) (lemTransOneTurn n@j)) rem3 []
where l : loopS1 = itLoop n
rem1 : Path Z (transport (<i> helix (l@i)) (inr zero)) (inr n) = decodeEncodeBasePos n
rem2 : Path Z (transport (<i>helix (oneTurn l@i)) (inr zero))
(transport (<i>helix (loop1@i)) (transport (<i>helix (l@i)) (inr zero))) =
corFib2 (inr zero) l
rem3 : Path Z (transport (<i>helix (oneTurn l@i)) (inr zero))
(transport (<i>helix (loop1@i)) (inr n)) =
comp (<j>Path Z (transport (<i>helix (oneTurn l@i)) (inr zero))
(transport (<i>helix (loop1@i)) (rem1@j))) rem2 []
decodeEncodeBaseNeg : (n : nat) -> Path Z (transport (<x> helix (itLoopNeg n @ x)) (inr zero)) (inl n) = split
zero -> <_> inl zero
suc n -> comp (<j>Path Z (transport (<i>helix (backTurn l@i)) (inr zero)) (lemTransBackTurn n@j)) rem3 []
where l : loopS1 = itLoopNeg n
rem1 : Path Z (transport (<i> helix (l@i)) (inr zero)) (inl n) = decodeEncodeBaseNeg n
rem2 : Path Z (transport (<i>helix (backTurn l@i)) (inr zero))
(transport (<i>helix (loop1@-i)) (transport (<i>helix (l@i)) (inr zero))) =
corFib3 (inr zero) l
rem3 : Path Z (transport (<i>helix (backTurn l@i)) (inr zero))
(transport (<i>helix (loop1@-i)) (inl n)) =
comp (<j>Path Z (transport (<i>helix (backTurn l@i)) (inr zero))
(transport (<i>helix (loop1@-i)) (rem1@j))) rem2 []
decodeEncodeBase : (n : Z) -> Path Z (encode base (decode base n)) n = split
inl n -> decodeEncodeBaseNeg n
inr n -> decodeEncodeBasePos n
-- the loop space of the circle is equal to Z
loopS1equalsZ : Path U loopS1 Z =
isoPath loopS1 Z (encode base) (decode base) decodeEncodeBase (encodeDecode base)
setLoop : set loopS1 = substInv U set loopS1 Z loopS1equalsZ 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 loop1 bP bP) @ i
helixSet : (x:S1) -> set (helix x) = lemPropFib (\ (x:S1) -> set (helix x)) rem ZSet
where rem (x:S1) : prop (set (helix x)) = setIsProp (helix x)
-- S1 is a groupoid
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))
substInv (A : U) (P : A -> U) (a x : A) (p : Path A a x) : P x -> P a =
subst A P x a (<i>p @ -i)
funDepTr (A0 A1:U) (p:Path U A0 A1) (u0:A0) (u1:A1) :
Path U (PathP p u0 u1) (Path A1 (transport p u0) u1) =
<i> PathP (<l>p @ (i\/l)) (comp (<l>p @ (i/\l)) u0 [(i=0) -> <_>u0]) u1
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
G (y x:S1) : U = E x y
lem1 : (y:S1) -> PathS S1 (G y) base base loop1 (f y) (f y) = lemPropFib P pP bP
where
P (y:S1) : U = PathS S1 (G y) base base loop1 (f y) (f y)
sbE : (y : S1) -> set (E base y)
= lemPropFib (\ (y:S1) -> set (E base y)) (\ (y:S1) -> setIsProp (E base y)) sE
pP (y:S1) : prop (P y) = rem3
where
rem1 : Path U (P y) (Path (E base y) (subst S1 (G y) base base loop1 (f y)) (f y))
= funDepTr (G y base) (G y base) (<j>G y (loop{S1} @ j)) (f y) (f y)
rem2 : prop (Path (E base y) (subst S1 (G y) base base loop1 (f y)) (f y))
= sbE y (subst S1 (G y) base base loop1 (f y)) (f y)
rem3 : prop (P y)
= substInv U prop (P y) (Path (E base y) (subst S1 (G y) base base loop1 (f y)) (f y)) rem1 rem2
lem2 : PathS S1 (G base) base base loop1 (g base) (g base)
= <j> g (loop1 @ j)
bP : P base
= substInv (E base base) (\ (u:E base base) -> PathS S1 (G base) base base loop1 u u) (f base) (g base) efg lem2
lem2 : PathS S1 F base base loop1 f f = <j> \ (y:S1) -> (lem1 y) @ j
-- commutativity of mult, at last
idL : (x : S1) -> Path S1 (mult base x) x = split
base -> refl S1 base
loop @ i -> <j> loop1 @ i
multCom : (x y : S1) -> Path S1 (mult x y) (mult y x) =
lemSetTorus E sE idL g efg
where
E (x y: S1) : U = Path S1 (mult x y) (mult y x)
sE : set (E base base) = isGroupoidS1 base base
g (x : S1) : E x base = inv S1 (mult base x) (mult x base) (idL x)
efg : Path (E base base) (idL base) (g base) = refl (E base base) (idL base)
-- associativity
multAssoc (x :S1) : (y z : S1) -> Path S1 (mult x (mult y z)) (mult (mult x y) z) =
lemSetTorus E sE f g efg
where
E (y z : S1) : U = Path S1 (mult x (mult y z)) (mult (mult x y) z)
sE : set (E base base) = isGroupoidS1 x x
f (z : S1) : E base z = rem
where
rem1 : Path S1 (mult base z) z = multCom base z
rem : Path S1 (mult x (mult base z)) (mult x z) = <i> mult x (rem1 @ i)
g (y : S1) : E y base = refl S1 (mult x y)
efg : Path (E base base) (f base) (g base) = refl (E base base) (f base)
-- inverse law
lemPropRel (P:S1 -> S1 -> U) (pP:(x y:S1) -> prop (P x y)) (bP:P base base) : (x y:S1) -> P x y =
lemPropFib (\ (x:S1) -> (y:S1) -> P x y)
(\ (x:S1) -> propPi S1 (P x) (pP x))
(lemPropFib (P base) (pP base) bP)
invLaw : (x y : S1) ->
Path (Path S1 (mult x y) (mult x y)) (refl S1 (mult x y))
(compPath S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x)) = lemPropRel P pP bP
where
P (x y : S1) : U
= Path (Path S1 (mult x y) (mult x y)) (refl S1 (mult x y))
(compPath S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x))
pP (x y : S1) : prop (P x y) =
isGroupoidS1 (mult x y) (mult x y) (refl S1 (mult x y))
(compPath S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x))
bP : P base base =
comp (<i>Path (Path S1 base base) (refl S1 base) (<j>comp (<_>S1) base [(i=0) -> refl S1 base, (j=0) -> refl S1 base, (j=1) -> refl S1 base]))
(refl (Path S1 base base) (refl S1 base)) []
-- the multiplication is invertible
multIsEquiv : (x:S1) -> isEquiv S1 S1 (mult x) = lemPropFib P pP bP
where P (x:S1) : U = isEquiv S1 S1 (mult x)
pP (x:S1) : prop (P x) = propIsEquiv S1 S1 (mult x)
rem : Path (S1 -> S1) (idfun S1) (mult base) = <i>\ (x:S1) -> idL x @ -i
bP : P base = subst (S1->S1) (isEquiv S1 S1) (idfun S1) (mult base) rem (idIsEquiv S1)
-- inverse of multiplication by x
invMult (x y:S1) : S1 = (multIsEquiv x y).1.1
invS1 (x:S1) : S1 = invMult x base
lemInvS1 : Path S1 (invS1 base) base =
<i> comp (<_>S1) (comp (<_>S1) base [(i=1) -> refl S1 base]) [(i=1) -> refl S1 base]
loopInvS1 : U = Path S1 (invS1 base) (invS1 base)
rePar (l: loopInvS1) : loopS1 = transport (<i>Path S1 (lemInvS1@i) (lemInvS1@i)) l
test2 : Z = winding (rePar (<i>invS1 (loop2@i)))
-- EVAL: inl (suc zero) Time: 1m26.400s
test21 : Z = winding (rePar (<i>invS1 (compS1 loop2 loop1 @i)))
-- EVAL: inl (suc (suc zero)) Time: 4m30.717s
test12 : Z = winding (rePar (<i>invS1 (compS1 loop1 loop2 @i)))
-- EVAL: inl (suc (suc zero)) Time: 9m40.535s
test4 : Z = winding (rePar (<i>invS1 (compS1 loop2 loop2 @i)))
-- EVAL: inl (suc (suc (suc zero))) Time: 14m5.128s
test0 : Z = winding (rePar (<i>invMult (loop2@i) (loop2@i)))
-- EVAL: inr zero Time: 1m39.599s
-- Alternative proof that loopS1 is a set (requires retract.ctt):
-- setLoop' : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (enoceDecode base) ZSet