-module helix where\r
-\r
-import circle\r
-import retract\r
-\r
-encode (x:S1) (p:Id S1 base x) : helix x = subst S1 helix base x p zeroZ\r
-\r
-itLoop : nat -> loopS1 = split\r
- zero -> triv\r
- suc n -> compS1 (itLoop n) loop1\r
-\r
-itLoopNeg : nat -> loopS1 = split \r
- zero -> invLoop\r
- suc n -> compS1 (itLoopNeg n) invLoop\r
-\r
-loopIt : Z -> loopS1 = split\r
- inl n -> itLoopNeg n\r
- inr n -> itLoop n\r
-\r
-lemItNat (n:nat) : Id loopS1 (itLoop (suc n)) (transport (<i>Id S1 base (loop{S1} @ i)) (itLoop n)) = \r
- refl loopS1 (itLoop (suc n))\r
-\r
-lemItNeg : (n:nat) -> Id loopS1 (transport (<i>Id S1 base (loop{S1} @ i)) (loopIt (inl n))) (loopIt (sucZ (inl n))) = split\r
- zero -> lemInv S1 base base loop1\r
- suc n -> lemCompInv S1 base base base (itLoopNeg n) invLoop\r
-\r
-oneTurn (l: loopS1) : loopS1 = transport (<i>Id S1 base (loop{S1} @ i)) l\r
-\r
-lemItPos : (n:nat) -> Id loopS1 (oneTurn (loopIt (predZ (inr n)))) (loopIt (inr n)) = split\r
- zero -> lemInv S1 base base loop1\r
- suc n -> refl loopS1 (loopIt (inr (suc n)))\r
-\r
-lemItNeg (n:nat) : Id loopS1 (oneTurn (loopIt (predZ (inl n)))) (loopIt (inl n)) = \r
- lemCompInv S1 base base base (loopIt (inl n)) invLoop\r
-\r
-lemIt : (n:Z) -> Id loopS1 (oneTurn (loopIt (predZ n))) (loopIt n) = split\r
- inl n -> lemItNeg n\r
- inr n -> lemItPos n\r
-\r
-funDepTr (A0 A1:U) (p:Id U A0 A1) (u0:A0) (u1:A1) :\r
- Id U (IdP p u0 u1) (Id A1 (transport p u0) u1) =\r
- <i> IdP (<l>p @ (i\/l)) (transport (<l>p @ (i/\l)) u0) u1\r
-\r
-decode : (x:S1) -> helix x -> Id S1 base x = split\r
- base -> loopIt\r
- loop @ i -> rem @ i\r
- where T : U = Z -> loopS1\r
- p : Id U T T = <j> helix (loop{S1}@j) -> Id S1 base (loop{S1}@j)\r
- rem1 : Id (Z -> loopS1) (transport p loopIt) loopIt =\r
- funExt Z (\ (n:Z) -> loopS1) (transport (<j> helix (loop{S1}@j) -> Id S1 base (loop{S1}@j)) loopIt) loopIt lemIt\r
- rem : IdP p loopIt loopIt = transport (<j> (funDepTr T T p loopIt loopIt)@-j) rem1\r
-\r
-lemPropF (A:U)(P:A->U)(pP:(x:A) -> prop (P x))(a0 a1:A)(p:Id A a0 a1)(b0:P a0)(b1:P a1): IdS A P a0 a1 p b0 b1 =\r
- <i> (pP (p @ i) (transport (<j>P (p@i /\ j)) b0) (transport (<j>P (p@i \/ -j)) b1)) @ i\r
-\r
-lemPropFib (P:S1 -> U) (pP:(x:S1) -> prop (P x)) (bP: P base) : (x:S1) -> P x = split\r
- base -> bP\r
- loop @ i -> (lemPropF S1 P pP base base loop1 bP bP) @ i\r
-\r
-helixSet : (x:S1) -> set (helix x) = lemPropFib (\ (x:S1) -> set (helix x)) rem ZSet\r
- where rem (x:S1) : prop (set (helix x)) = setIsProp (helix x)\r
-\r
-retHelix (x:S1) (p : Id S1 base x) : Id (Id S1 base x) (decode x (encode x p)) p = \r
- transport (<i>Id (Id S1 base p@i) (decode p@i (encode p@i (<j>p@(i/\j)))) (<j>p@(i/\j))) (refl loopS1 triv)\r
-\r
-setLoop : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (retHelix base) ZSet\r
-\r
--- S1 is a groupoid\r
-isGroupoidS1 : groupoid S1 = lem\r
- where\r
- lem2 : (y : S1) -> set (Id S1 base y)\r
- = lemPropFib (\ (y:S1) -> set (Id S1 base y)) (\ (y:S1) -> setIsProp (Id S1 base y)) setLoop\r
-\r
- lem : (x y : S1) -> set (Id S1 x y)\r
- = lemPropFib (\ (x:S1) -> (y : S1) -> set (Id S1 x y)) pP lem2\r
- where \r
- pP (x:S1) : prop ((y:S1) -> set (Id S1 x y)) =\r
- propPi S1 (\ (y:S1) -> set (Id S1 x y)) (\ (y:S1) -> setIsProp (Id S1 x y))\r
-\r
-substInv (A : U) (P : A -> U) (a x : A) (p : Id A a x) : P x -> P a =\r
- subst A P x a (<i>p @ -i)\r
-\r
-lemSetTorus (E : S1 -> S1 -> U) (sE : set (E base base))\r
- (f : (y:S1) -> E base y) (g : (x:S1) -> E x base)\r
- (efg : Id (E base base) (f base) (g base)) : (x y:S1) -> E x y = split\r
- base -> f\r
- loop @ i -> lem2 @ i\r
- where\r
- F (x:S1) : U = (y:S1) -> E x y\r
-\r
- G (y x:S1) : U = E x y\r
-\r
- lem1 : (y:S1) -> IdS S1 (G y) base base loop1 (f y) (f y) = lemPropFib P pP bP\r
- where\r
- P (y:S1) : U = IdS S1 (G y) base base loop1 (f y) (f y)\r
-\r
- sbE : (y : S1) -> set (E base y)\r
- = lemPropFib (\ (y:S1) -> set (E base y)) (\ (y:S1) -> setIsProp (E base y)) sE\r
-\r
- pP (y:S1) : prop (P y) = rem3\r
- where\r
- rem1 : Id U (P y) (Id (E base y) (subst S1 (G y) base base loop1 (f y)) (f y))\r
- = funDepTr (G y base) (G y base) (<j>G y loop{S1}@j) (f y) (f y)\r
-\r
- rem2 : prop (Id (E base y) (subst S1 (G y) base base loop1 (f y)) (f y))\r
- = sbE y (subst S1 (G y) base base loop1 (f y)) (f y)\r
-\r
- rem3 : prop (P y)\r
- = substInv U prop (P y) (Id (E base y) (subst S1 (G y) base base loop1 (f y)) (f y)) rem1 rem2\r
- \r
- lem2 : IdS S1 (G base) base base loop1 (g base) (g base)\r
- = <j> g (loop1 @ j)\r
-\r
- bP : P base\r
- = substInv (E base base) (\ (u:E base base) -> IdS S1 (G base) base base loop1 u u) (f base) (g base) efg lem2\r
-\r
- lem2 : IdS S1 F base base loop1 f f = <j> \ (y:S1) -> (lem1 y) @ j\r
-\r
--- commutativity of mult, at last\r
-\r
-idL : (x : S1) -> Id S1 (mult base x) x = split\r
- base -> refl S1 base\r
- loop @ i -> <j> loop1 @ i\r
-\r
-multCom : (x y : S1) -> Id S1 (mult x y) (mult y x) =\r
- lemSetTorus E sE idL g efg\r
- where\r
- E (x y: S1) : U = Id S1 (mult x y) (mult y x)\r
- sE : set (E base base) = isGroupoidS1 base base\r
- g (x : S1) : E x base = inv S1 (mult base x) (mult x base) (idL x)\r
- efg : Id (E base base) (idL base) (g base) = refl (E base base) (idL base)\r
-\r
--- associativity\r
-\r
-multAssoc (x :S1) : (y z : S1) -> Id S1 (mult x (mult y z)) (mult (mult x y) z) = \r
- lemSetTorus E sE f g efg\r
- where\r
- E (y z : S1) : U = Id S1 (mult x (mult y z)) (mult (mult x y) z)\r
- sE : set (E base base) = isGroupoidS1 x x\r
- f (z : S1) : E base z = rem\r
- where \r
- rem1 : Id S1 (mult base z) z = multCom base z\r
-\r
- rem : Id S1 (mult x (mult base z)) (mult x z) = <i> mult x (rem1 @ i)\r
- g (y : S1) : E y base = refl S1 (mult x y)\r
- efg : Id (E base base) (f base) (g base) = refl (E base base) (f base)\r
-\r
--- inverse law\r
-\r
-lemPropRel (P:S1 -> S1 -> U) (pP:(x y:S1) -> prop (P x y)) (bP:P base base) : (x y:S1) -> P x y = \r
- lemPropFib (\ (x:S1) -> (y:S1) -> P x y)\r
- (\ (x:S1) -> propPi S1 (P x) (pP x))\r
- (lemPropFib (P base) (pP base) bP) \r
-\r
-invLaw : (x y : S1) ->\r
- Id (Id S1 (mult x y) (mult x y)) (refl S1 (mult x y))\r
- (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x)) = lemPropRel P pP bP \r
- where\r
- P (x y : S1) : U\r
- = Id (Id S1 (mult x y) (mult x y)) (refl S1 (mult x y))\r
- (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x))\r
-\r
- pP (x y : S1) : prop (P x y) =\r
- isGroupoidS1 (mult x y) (mult x y) (refl S1 (mult x y))\r
- (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x))\r
-\r
- bP : P base base = refl (Id S1 base base) (refl S1 base)\r
+module helix where
+
+import circle
+import retract
+
+encode (x:S1) (p:Id S1 base x) : helix x = subst S1 helix base x p zeroZ
+
+itLoop : nat -> loopS1 = split
+ zero -> triv
+ suc n -> compS1 (itLoop n) loop1
+
+itLoopNeg : nat -> loopS1 = split
+ zero -> invLoop
+ suc n -> compS1 (itLoopNeg n) invLoop
+
+loopIt : Z -> loopS1 = split
+ inl n -> itLoopNeg n
+ inr n -> itLoop n
+
+lemItNat (n:nat) : Id loopS1 (itLoop (suc n)) (transport (<i>Id S1 base (loop{S1} @ i)) (itLoop n)) =
+ refl loopS1 (itLoop (suc n))
+
+lemItNeg : (n:nat) -> Id loopS1 (transport (<i>Id 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
+
+oneTurn (l: loopS1) : loopS1 = transport (<i>Id S1 base (loop{S1} @ i)) l
+
+lemItPos : (n:nat) -> Id loopS1 (oneTurn (loopIt (predZ (inr n)))) (loopIt (inr n)) = split
+ zero -> lemInv S1 base base loop1
+ suc n -> refl loopS1 (loopIt (inr (suc n)))
+
+lemItNeg (n:nat) : Id loopS1 (oneTurn (loopIt (predZ (inl n)))) (loopIt (inl n)) =
+ lemCompInv S1 base base base (loopIt (inl n)) invLoop
+
+lemIt : (n:Z) -> Id loopS1 (oneTurn (loopIt (predZ n))) (loopIt n) = split
+ inl n -> lemItNeg n
+ inr n -> lemItPos n
+
+funDepTr (A0 A1:U) (p:Id U A0 A1) (u0:A0) (u1:A1) :
+ Id U (IdP p u0 u1) (Id A1 (transport p u0) u1) =
+ <i> IdP (<l>p @ (i\/l)) (transport (<l>p @ (i/\l)) u0) u1
+
+decode : (x:S1) -> helix x -> Id S1 base x = split
+ base -> loopIt
+ loop @ i -> rem @ i
+ where T : U = Z -> loopS1
+ p : Id U T T = <j> helix (loop{S1}@j) -> Id S1 base (loop{S1}@j)
+ rem1 : Id (Z -> loopS1) (transport p loopIt) loopIt = <j> \ (n:Z) -> (lemIt n)@j
+ rem : IdP p loopIt loopIt = transport (<j> (funDepTr T T p loopIt loopIt)@-j) rem1
+
+lemPropF (A:U)(P:A->U)(pP:(x:A) -> prop (P x))(a0 a1:A)(p:Id A a0 a1)(b0:P a0)(b1:P a1): IdS A P a0 a1 p b0 b1 =
+ <i> (pP (p @ i) (transport (<j>P (p@i /\ j)) b0) (transport (<j>P (p@i \/ -j)) b1)) @ i
+
+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)
+
+retHelix (x:S1) (p : Id S1 base x) : Id (Id S1 base x) (decode x (encode x p)) p =
+ transport (<i>Id (Id S1 base p@i) (decode p@i (encode p@i (<j>p@(i/\j)))) (<j>p@(i/\j))) (refl loopS1 triv)
+
+setLoop : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (retHelix base) ZSet
+
+-- S1 is a groupoid
+isGroupoidS1 : groupoid S1 = lem
+ where
+ lem2 : (y : S1) -> set (Id S1 base y)
+ = lemPropFib (\ (y:S1) -> set (Id S1 base y)) (\ (y:S1) -> setIsProp (Id S1 base y)) setLoop
+
+ lem : (x y : S1) -> set (Id S1 x y)
+ = lemPropFib (\ (x:S1) -> (y : S1) -> set (Id S1 x y)) pP lem2
+ where
+ pP (x:S1) : prop ((y:S1) -> set (Id S1 x y)) =
+ propPi S1 (\ (y:S1) -> set (Id S1 x y)) (\ (y:S1) -> setIsProp (Id S1 x y))
+
+substInv (A : U) (P : A -> U) (a x : A) (p : Id A a x) : P x -> P a =
+ subst A P x a (<i>p @ -i)
+
+lemSetTorus (E : S1 -> S1 -> U) (sE : set (E base base))
+ (f : (y:S1) -> E base y) (g : (x:S1) -> E x base)
+ (efg : Id (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) -> IdS S1 (G y) base base loop1 (f y) (f y) = lemPropFib P pP bP
+ where
+ P (y:S1) : U = IdS 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 : Id U (P y) (Id (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 (Id (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) (Id (E base y) (subst S1 (G y) base base loop1 (f y)) (f y)) rem1 rem2
+
+ lem2 : IdS 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) -> IdS S1 (G base) base base loop1 u u) (f base) (g base) efg lem2
+
+ lem2 : IdS S1 F base base loop1 f f = <j> \ (y:S1) -> (lem1 y) @ j
+
+-- commutativity of mult, at last
+
+idL : (x : S1) -> Id S1 (mult base x) x = split
+ base -> refl S1 base
+ loop @ i -> <j> loop1 @ i
+
+multCom : (x y : S1) -> Id S1 (mult x y) (mult y x) =
+ lemSetTorus E sE idL g efg
+ where
+ E (x y: S1) : U = Id 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 : Id (E base base) (idL base) (g base) = refl (E base base) (idL base)
+
+-- associativity
+
+multAssoc (x :S1) : (y z : S1) -> Id S1 (mult x (mult y z)) (mult (mult x y) z) =
+ lemSetTorus E sE f g efg
+ where
+ E (y z : S1) : U = Id 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 : Id S1 (mult base z) z = multCom base z
+
+ rem : Id 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 : Id (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) ->
+ Id (Id S1 (mult x y) (mult x y)) (refl S1 (mult x y))
+ (compId 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
+ = Id (Id S1 (mult x y) (mult x y)) (refl S1 (mult x y))
+ (compId 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))
+ (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x))
+
+ bP : P base base = refl (Id S1 base base) (refl S1 base)
+
projects / cubicaltt.git / commitdiff