# dlicata335/hott-agda

resuccitate partial torus proof from last fall

1 parent 1f4f341 commit 5ff8a94180eab79871dfdb835ea12542a97b2396 committed Mar 8, 2013
4 homotopy/PiNSN.agda
 @@ -13,7 +13,7 @@ module homotopy.PiNSN where open S using (S^ ; S-rec; S-elim) promote : ∀ {n} → (S^ n) → (Path{S^ (n +1)} S.base S.base) - promote{n} = S-rec id (loopSN1 n (S.loop (S n))) + promote{n} = S-rec id (loopSN1 n (S.loop (n +1))) decode' : ∀ {n} → Trunc (tlp n) (S^ n) @@ -24,7 +24,7 @@ module homotopy.PiNSN where P {n} x = Trunc (tlp n) (Path{S^ (n +1)} S.base x) S-loops : ∀ n -> (x : Trunc (tlp n) (S^ n)) → Loop n (Trunc (tlp n) (S^ n)) x - S-loops n = Trunc-elim (\ x -> Loop n (Trunc (tlp n) (S^ n)) x) + S-loops n = Trunc-elim _ (λ x → Loop-preserves-level n (tlp n) Trunc-level) (S-elim {n} (λ x → Loop n (Trunc (tlp n) (S^ n)) [ x ]) (ap^ n [_] (S.loop n))
83 homotopy/TS1S1.agda
 @@ -0,0 +1,83 @@ +{-# OPTIONS --type-in-type --without-K #-} + +open import lib.Prelude + +module homotopy.TS1S1 where + + open S¹ using (S¹ ; S¹-rec ; S¹-elim) + module T = Torus + open T using (T ; T-rec ; T-elim) + + rearrange : ∀ {A : Type} (x : A) (p : Path x x) (q : Path x x) + → (Path (transport (λ x → Path x x) q p) p) ≃ Path (p ∘ q) (q ∘ p) + rearrange x p q = transport (λ x' → Path x' x') q p ≃ p ≃〈 ap (BackPath _) (transport-Path (λ x' → x') (λ x' → x') q p) 〉 + ap (\ x -> x) q ∘ p ∘ ! (ap (\ x -> x) q) ≃ p ≃〈 ap (BackPath _) (ap (λ x' → x' ∘ p ∘ ! x') (ap-id q)) 〉 + q ∘ p ∘ ! q ≃ p ≃〈 ap (BackPath _) (∘-assoc q p (! q)) 〉 + (q ∘ p) ∘ ! q ≃ p ≃〈 move-right-right-!≃ (q ∘ p) q p 〉 + q ∘ p ≃ p ∘ q ≃〈 flip≃ 〉 + p ∘ q ≃ q ∘ p ∎ + + map-out : {X : Type} -> (S¹ × S¹ -> X) ≃ (T -> X) + map-out {X} = + ((S¹ × S¹ → X) ≃〈 (uncurry≃ S¹ (\ _ -> S¹) (\ _ -> X)) 〉 + (S¹ -> (S¹ -> X)) ≃〈 ap (λ t → S¹ → t) S¹.ump 〉 + (S¹ -> Σ[ x ∶ X ] (Path x x)) ≃〈 S¹.ump 〉 + (Σ[ p ∶ (Σ[ x ∶ X ] (Path x x)) ] (Path p p)) ≃〈 Σassoc.path 〉 + (Σ[ x ∶ X ] (Σ[ p ∶ Path x x ] (Path (x , p) (x , p)))) ≃〈 apΣ' id-equiv (λ x → apΣ' id-equiv (λ p → ! ΣPath.path)) 〉 + (Σ[ x ∶ X ] (Σ[ p ∶ Path x x ] (Σ[ q ∶ Path x x ] (Path (transport (λ x → Path x x) q p) p)))) ≃〈 apΣ' id-equiv (λ x → apΣ' id-equiv (λ p → apΣ' id-equiv (λ q → rearrange x p q))) 〉 + (Σ[ x ∶ X ] (Σ[ p ∶ Path x x ] (Σ[ q ∶ Path x x ] Path (p ∘ q) (q ∘ p)))) ≃〈 ua (_ , T.ump) 〉 + (T → X) ∎) + + t2c : T -> S¹ × S¹ + t2c = T-rec (S¹.base , S¹.base) (pair×≃ id S¹.loop) (pair×≃ S¹.loop id) {!!} + + map-out-posto : ∀ {X} (f : S¹ × S¹ -> X) -> coe map-out f ≃ f o t2c + map-out-posto {X} f = {!!} where + fact1 : coe (uncurry≃ S¹ (\ _ -> S¹) (\ _ -> X)) f ≃ (λ x y → f (x , y)) + fact1 = ap≃ (type≃β _) + + term2 = (λ x → f (x , S¹.base) , ap (λ y → f (x , y)) S¹.loop) + fact2 : coe (ap (λ t → S¹ → t) S¹.ump) (λ x y → f (x , y)) ≃ term2 + fact2 = coe (ap (λ t → S¹ → t) S¹.ump) (λ x y → f (x , y)) ≃〈 ! (ap≃ (transport-ap-assoc (λ t → S¹ → t) S¹.ump)) 〉 + transport (\ x -> S¹ -> x) S¹.ump (λ x y → f (x , y)) ≃〈 transport-→-post S¹.ump (λ x y → f (x , y)) 〉 + (\ x -> coe S¹.ump (λ y → f (x , y))) ≃〈 λ≃ (λ x → ap≃ (type≃β S¹.ump-eqv)) 〉 + (λ x → f (x , S¹.base) , ap (λ y → f (x , y)) S¹.loop) ∎ + + term3 = (f (S¹.base , S¹.base) , ap (λ y → f (S¹.base , y)) S¹.loop) , + ap term2 S¹.loop + fact3 : (coe S¹.ump term2) ≃ term3 + fact3 = ap≃ (type≃β S¹.ump-eqv) + + term4 = f (S¹.base , S¹.base) , (ap (λ y → f (S¹.base , y)) S¹.loop) , ap term2 S¹.loop + fact4 : coe Σassoc.path term3 ≃ term4 + fact4 = ap≃ (type≃β Σassoc.eqv){term3} + + term5 = f (S¹.base , S¹.base) , (ap (λ y → f (S¹.base , y)) S¹.loop) , fst≃ (ap term2 S¹.loop) , snd≃ (ap term2 S¹.loop) + fact5 : coe (apΣ' id-equiv (λ x → apΣ' id-equiv (λ p → ! ΣPath.path))) term4 ≃ term5 + fact5 = {!!} + + term6 = f (S¹.base , S¹.base) , + (ap (λ y → f (S¹.base , y)) S¹.loop) , + fst≃ (ap term2 S¹.loop) , + coe (rearrange _ (ap (λ y → f (S¹.base , y)) S¹.loop) (fst≃ (ap term2 S¹.loop))) (snd≃ (ap term2 S¹.loop)) + fact6 : coe (apΣ' id-equiv (λ x → apΣ' id-equiv (λ p → apΣ' id-equiv (λ q → rearrange x p q)))) term5 ≃ term6 + fact6 = {!!} + + LHS-reduced = T-rec (f (S¹.base , S¹.base)) + (ap (λ y → f (S¹.base , y)) S¹.loop) + (ap (λ x → f (x , S¹.base)) S¹.loop) + {!coe (rearrange _ (ap (λ y → f (S¹.base , y)) S¹.loop) (fst≃ (ap term2 S¹.loop))) (snd≃ (ap term2 S¹.loop))!} + fact7 : coe (ua (_ , T.ump)) term6 ≃ LHS-reduced + fact7 = {!!} ∘ ap≃ (type≃β (_ , T.ump)) {term6} + + RHS-reduced : f o t2c ≃ T-rec (f (S¹.base , S¹.base)) (ap f (pair×≃ id S¹.loop)) + (ap f (pair×≃ S¹.loop id)) {!!} + RHS-reduced = {!T.Tη {_}{f} !} + + theorem : IsEquiv{T} {(S¹ × S¹)} t2c + theorem = {!transport IsEquiv ? (coe-is-equiv (map-out{S¹ × S¹}))!} + fact1 : (S¹ × S¹ -> S¹ × S¹) ≃ (T -> S¹ × S¹) + fact1 = + + fact2 : IsEquiv{S¹ × S¹}{S¹ × S¹} (\ x -> x) + fact2 = snd id-equiv
2 homotopy/Theorems.agda
 @@ -1,7 +1,9 @@ -- wrapper to type check everything that's done + import homotopy.Pi1Either + -- homotopy groups of spheres import homotopy.Pi1S1
 @@ -71,7 +71,7 @@ module homotopy.Whitehead where (nA : NType (tlp n) A) (nB : NType (tlp n) B) (f : A → B) (zero : IsEquiv {Trunc (tl 0) A} {Trunc (tl 0) B} (Trunc-func f)) - (pis : ∀ k x → IsEquiv{Trunc (tl 0) (Loop k A x)}{Trunc (tl 0) (Loop k B (f x))} (Trunc-func (ap^ k f))) + (pis : ∀ k x → IsEquiv{π k A x}{π k B (f x)} (Trunc-func (ap^ k f))) -> IsEquiv f whitehead One nA nB f zero pis = SplitEquiv.iseqv f zero
6 lib/First.agda
 @@ -114,6 +114,12 @@ module lib.First where → Path β (γ ∘ α) move-right-right-! id id γ x = x + move-right-right-!≃ : {A : Type} {M N P : A} + (β : Path N P) (α : Path N M) (γ : Path M P) + → Path (β ∘ ! α) γ + ≃ Path β (γ ∘ α) + move-right-right-!≃ id id γ = id + rassoc-1-3-1 : ∀ {A} {M1 M2 M3 M4 M5 M6 : A} (a56 : Path M5 M6) (a45 : Path M4 M5) (a34 : Path M3 M4) (a23 : Path M2 M3) (a12 : Path M1 M2) → Path (a56 ∘ (a45 ∘ a34 ∘ a23) ∘ a12) (a56 ∘ a45 ∘ a34 ∘ a23 ∘ a12)
4 lib/Functions.agda
 @@ -54,6 +54,10 @@ module lib.Functions where -> transport (\ X -> X -> C) δ f ≃ (f o (transport (\ X -> X) (! δ))) transport-→-pre id f = id + transport-→-post : ∀ {C A B : Set} (δ : B ≃ C) (f : A -> B) + -> transport (\ X -> A -> X) δ f ≃ (transport (\ X -> X) δ o f) + transport-→-post id f = id + transport-→-from-square : ∀ {A} (B C : A → Type) {a a' : A} (α : a ≃ a') (f : B a -> C a) (g : B a' -> C a') -> transport C α o f ≃ g o (transport B α)
33 lib/Prods.agda
 @@ -120,6 +120,39 @@ module lib.Prods where → (hp : (x : A) → HProp (B x)) (p' : Path{Σ B} p q) → (coe (! (ΣSubsetPath {p = p} {q = q} hp)) p') ≃ fst≃ p' + + + module Σassoc where + + rassoc : {X : Type} + -> {A : X -> Type} + -> {B : (Σ[ x ∶ X ] (A x)) -> Type} + -> (Σ[ p ∶ (Σ[ x ∶ X ] (A x)) ] (B p)) + -> Σ[ x  ∶ X ] (Σ[ l1 ∶ A x ] (B (x , l1))) + rassoc ((fst , snd) , snd') = fst , (snd , snd') + + lassoc : {X : Type} + -> {A : X -> Type} + -> {B : (Σ[ x ∶ X ] (A x)) -> Type} + -> Σ[ x ∶ X ] (Σ[ l1 ∶ A x ] (B (x , l1))) + -> (Σ[ p ∶ (Σ[ x ∶ X ] (A x)) ] (B p)) + lassoc (fst , fst' , snd) = (fst , fst') , snd + + eqv : {X : Type} + -> {A : X -> Type} + -> {B : (Σ[ x ∶ X ] (A x)) -> Type} + -> Equiv (Σ[ p ∶ (Σ[ x ∶ X ] (A x)) ] (B p)) + (Σ[ x  ∶ X ] (Σ[ l1 ∶ A x ] (B (x , l1)))) + eqv = improve (hequiv rassoc lassoc (λ y → id) (λ x → id)) + + path : {X : Type} + -> {A : X -> Type} + -> {B : (Σ[ x ∶ X ] (A x)) -> Type} + -> (Σ[ p ∶ (Σ[ x ∶ X ] (A x)) ] (B p)) + ≃ (Σ[ x  ∶ X ] (Σ[ l1 ∶ A x ] (B (x , l1)))) + path = ua eqv + + Σlevel : ∀ {n} {A : Type} {B : A → Type} → NType n A → ((x : A) → NType n (B x))
186 lib/spaces/Circle.agda
 @@ -4,106 +4,106 @@ open import lib.BasicTypes module lib.spaces.Circle where +module S¹ where + private + module S where + private + data S¹' : Type where + Base : S¹' + + S¹ : Type + S¹ = S¹' + + base : S¹ + base = Base + + postulate {- HoTT Axiom -} + loop : Path base base + + S¹-rec : {C : Type} + -> (c : C) + -> (α : c ≃ c) + -> S¹ -> C + S¹-rec a _ Base = a + + S¹-elim : (C : S¹ -> Type) + -> (c : C base) + (α : Path (transport C loop c) c) + -> (x : S¹) -> C x + S¹-elim _ x _ Base = x - - module S¹ where - private - data S¹' : Set where - Base : S¹' - - S¹ : Set - S¹ = S¹' - - base : S¹ - base = Base - - postulate {- HoTT Axiom -} - loop : Path base base - - S¹-rec : {C : Set} - -> (c : C) - -> (α : c ≃ c) - -> S¹ -> C - S¹-rec a _ Base = a - - S¹-elim : (C : S¹ -> Set) - -> (c : C base) - (α : Path (transport C loop c) c) - -> (x : S¹) -> C x - S¹-elim _ x _ Base = x - - S¹-induction : (C : S¹ -> Set) - -> (c : C base) - (α : Path (transport C loop c) c) - -> (x : S¹) -> C x - S¹-induction = S¹-elim - - postulate {- HoTT Axiom -} - βloop/rec : {C : Set} - -> (c : C) - -> (α : Path c c) - -> Path (ap (S¹-rec c α) loop) α - - βloop/elim : {C : S¹ -> Set} - -> (c : C base) (α : Path (transport C loop c) c) - -> Path (apd (S¹-induction C c α) loop) α - - open S¹ + S¹-induction : (C : S¹ -> Type) + -> (c : C base) + (α : Path (transport C loop c) c) + -> (x : S¹) -> C x + S¹-induction = S¹-elim + + postulate {- HoTT Axiom -} + βloop/rec : {C : Type} + -> (c : C) + -> (α : Path c c) + -> Path (ap (S¹-rec c α) loop) α + + βloop/elim : {C : S¹ -> Type} + -> (c : C base) (α : Path (transport C loop c) c) + -> Path (apd (S¹-induction C c α) loop) α + + open S public -- Equivalence between (S¹ -> X) and Σe X (\ x → Id x x) - module S¹-Lemmas where - - S¹η-rec : {C : Set} - (M : S¹ -> C) - (N : S¹) - -> M N ≃ (S¹-rec (M base) (ap M loop) N) - S¹η-rec {C} M N = S¹-elim (λ x → M x ≃ S¹-rec (M base) (ap M loop) x) - id - (!-inv-r (ap M loop) - ∘ ap (λ x → ap M loop ∘ x) (∘-unit-l (! (ap M loop))) - ∘ ap (λ x → x ∘ id ∘ ! (ap M loop)) (βloop/rec {C} (M base) (ap M loop)) - ∘ transport-Path M (S¹-rec (M base) (ap M loop)) loop id - ) - N - - S¹η : {C : S¹ -> Set} - (M : (x : S¹) -> C x) + η-rec : {C : Type} + (M : S¹ -> C) (N : S¹) - -> M N ≃ (S¹-elim C (M base) (apd M loop) N) - S¹η {C} M N = S¹-elim (λ x → M x ≃ S¹-elim C (M base) (apd M loop) x) - id - (!-inv-r (apd M loop) - ∘ ap (λ x → apd M loop ∘ x) (∘-unit-l (! (apd M loop))) - ∘ ap (λ x → x ∘ id ∘ ! (apd M loop)) (βloop/elim {C} (M base) (apd M loop)) - ∘ transport-Path-d M (S¹-elim _ (M base) (apd M loop)) loop id) - N - - fromgen : {X : Set} -> Σ[ x ∶ X ] (Id x x) -> (S¹ -> X) - fromgen (fst , snd) = S¹-rec fst snd - - togen : {X : Set} -> (S¹ -> X) -> Σ[ x ∶ X ] (Id x x) - togen {X} f = f base , ap f loop - - fromto : {X : Set} -> (fromgen o togen) ≃ (λ (f : S¹ -> X) → f) - fromto {X} = λ≃ (λ f → λ≃ (λ x → ! (S¹η-rec f x))) - - tofrom : {X : Set} -> (togen o fromgen) ≃ (λ (f : Σ[ x ∶ X ] (Id x x)) → f) - tofrom {X} = λ≃ (λ x → - (fst x , ap (S¹-rec (fst x) (snd x)) loop) - ≃〈 ap (λ y → fst x , y) (βloop/rec (fst x) (snd x)) 〉 - (fst x , snd x) - ≃〈 id 〉 - id) - - free : {X : Set} -> (S¹ -> X) ≃ (Σ[ x ∶ X ] (Id x x)) - free {X} = ua (improve (hequiv togen - fromgen - (λ x → ap≃ fromto) - (λ y → ap≃ tofrom))) + -> M N ≃ (S¹-rec (M base) (ap M loop) N) + η-rec {C} M N = S¹-elim (λ x → M x ≃ S¹-rec (M base) (ap M loop) x) + id + (!-inv-r (ap M loop) + ∘ ap (λ x → ap M loop ∘ x) (∘-unit-l (! (ap M loop))) + ∘ ap (λ x → x ∘ id ∘ ! (ap M loop)) (βloop/rec {C} (M base) (ap M loop)) + ∘ transport-Path M (S¹-rec (M base) (ap M loop)) loop id + ) + N + + η-elim : {C : S¹ -> Type} + (M : (x : S¹) -> C x) + (N : S¹) + -> M N ≃ (S¹-elim C (M base) (apd M loop) N) + η-elim {C} M N = S¹-elim (λ x → M x ≃ S¹-elim C (M base) (apd M loop) x) + id + (!-inv-r (apd M loop) + ∘ ap (λ x → apd M loop ∘ x) (∘-unit-l (! (apd M loop))) + ∘ ap (λ x → x ∘ id ∘ ! (apd M loop)) (βloop/elim {C} (M base) (apd M loop)) + ∘ transport-Path-d M (S¹-elim _ (M base) (apd M loop)) loop id) + N + + fromgen : {X : Type} -> Σ[ x ∶ X ] (Id x x) -> (S¹ -> X) + fromgen (fst , snd) = S¹-rec fst snd + + togen : {X : Type} -> (S¹ -> X) -> Σ[ x ∶ X ] (Id x x) + togen {X} f = f base , ap f loop + + fromto : {X : Type} -> (fromgen o togen) ≃ (λ (f : S¹ -> X) → f) + fromto {X} = λ≃ (λ f → λ≃ (λ x → ! (η-rec f x))) + + tofrom : {X : Type} -> (togen o fromgen) ≃ (λ (f : Σ[ x ∶ X ] (Id x x)) → f) + tofrom {X} = λ≃ (λ x → + (fst x , ap (S¹-rec (fst x) (snd x)) loop) + ≃〈 ap (λ y → fst x , y) (βloop/rec (fst x) (snd x)) 〉 + (fst x , snd x) + ≃〈 id 〉 + id) + + ump-eqv : {X : Type} → Equiv (S¹ -> X) (Σ[ x ∶ X ] (Id x x)) + ump-eqv = (improve (hequiv togen + fromgen + (λ x → ap≃ fromto) + (λ y → ap≃ tofrom))) + + ump : {X : Type} -> (S¹ -> X) ≃ (Σ[ x ∶ X ] (Id x x)) + ump {X} = ua ump-eqv - open S¹
194 lib/spaces/Torus.agda
 @@ -5,107 +5,111 @@ open import lib.WEq module lib.spaces.Torus where - module Torus where - private - data T' : Set where - Base : T' - - T : Set - T = T' - - base : T - base = Base - - postulate {- HoTT Axiom -} - loop₁ : base ≃ base - loop₂ : base ≃ base - f : (loop₁ ∘ loop₂) ≃ (loop₂ ∘ loop₁) - - T-rec : {C : Set} - -> (a : C) - -> (p q : a ≃ a) - -> (f' : (p ∘ q) ≃ (q ∘ p)) - -> T -> C - T-rec a _ _ _ Base = a - - CommutatorDep : {C : T -> Set} - (a' : C base) - (p' : transport C loop₁ a' ≃ a') - (q' : transport C loop₂ a' ≃ a') -> Set - CommutatorDep {C} a' p' q' = - transport (λ x → transport C x a' ≃ a') f - (p' ∘ (ap (transport C loop₁) q') ∘ ap≃ (transport-∘ C loop₁ loop₂)) - ≃ q' ∘ (ap (transport C loop₂) p') ∘ ap≃ (transport-∘ C loop₂ loop₁) - - T-elim : {C : T -> Set} - (a' : C base) - (p' : transport C loop₁ a' ≃ a') - (q' : transport C loop₂ a' ≃ a') - (f' : CommutatorDep {C} a' p' q') - -> (x : T) -> C x - T-elim a _ _ _ Base = a - - postulate {- HoTT Axiom -} - βloop₁/rec : {C : Set} - -> (a : C) - -> (p q : a ≃ a) - -> (f : (p ∘ q) ≃ (q ∘ p)) - -> ap (T-rec a p q f) loop₁ ≃ p - - βloop₂/rec : {C : Set} - -> (a : C) - -> (p q : a ≃ a) - -> (f : (p ∘ q) ≃ (q ∘ p)) - -> ap (T-rec a p q f) loop₂ ≃ q - - ap-f : {X : Set} - -> (p : T -> X) - -> Id (ap p (loop₁ ∘ loop₂)) (ap p (loop₂ ∘ loop₁)) ≃ - Id (ap p loop₁ ∘ ap p loop₂) (ap p loop₂ ∘ ap p loop₁) - ap-f p = - Id (ap p (loop₁ ∘ loop₂)) (ap p (loop₂ ∘ loop₁)) - ≃〈 ap2 (λ x x' → Id x x') - (ap-∘ p loop₁ loop₂) - (ap-∘ p loop₂ loop₁) 〉 - Id (ap p loop₁ ∘ ap p loop₂) (ap p loop₂ ∘ ap p loop₁) ∎ - - f-aps : {C : Set} +module Torus where + private + module T where + private + data T' : Set where + Base : T' + + T : Set + T = T' + + base : T + base = Base + + postulate {- HoTT Axiom -} + loop₁ : base ≃ base + loop₂ : base ≃ base + f : (loop₁ ∘ loop₂) ≃ (loop₂ ∘ loop₁) + + T-rec : {C : Set} -> (a : C) -> (p q : a ≃ a) -> (f' : (p ∘ q) ≃ (q ∘ p)) - -> Id (ap (T-rec a p q f') (loop₁ ∘ loop₂)) (ap (T-rec a p q f') (loop₂ ∘ loop₁)) - ≃ Id (p ∘ q) (q ∘ p) - f-aps a p q f' = - (Id (ap (T-rec a p q f') (loop₁ ∘ loop₂)) - (ap (T-rec a p q f') (loop₂ ∘ loop₁))) - ≃〈 ap-f (T-rec a p q f') 〉 - (Id (ap (T-rec a p q f') loop₁ ∘ ap (T-rec a p q f') loop₂) - (ap (T-rec a p q f') loop₂ ∘ ap (T-rec a p q f') loop₁)) - ≃〈 ap2 (λ x y → Id x y) - (ap2 (λ x x' → x ∘ x') (βloop₁/rec a p q f') (βloop₂/rec a p q f')) - (ap2 (λ x x' → x ∘ x') (βloop₂/rec a p q f') (βloop₁/rec a p q f')) 〉 - (Id (p ∘ q) (q ∘ p)) ∎ - - postulate {- HoTT Axiom -} - βf/rec : {C : Set} - -> (a : C) - -> (p q : a ≃ a) - -> (f' : (p ∘ q) ≃ (q ∘ p)) - -> ap (ap (T-rec a p q f')) f ≃ transport (λ x → x) (! (f-aps a p q f')) f' + -> T -> C + T-rec a _ _ _ Base = a + + CommutatorDep : {C : T -> Set} + (a' : C base) + (p' : transport C loop₁ a' ≃ a') + (q' : transport C loop₂ a' ≃ a') -> Set + CommutatorDep {C} a' p' q' = + transport (λ x → transport C x a' ≃ a') f + (p' ∘ (ap (transport C loop₁) q') ∘ ap≃ (transport-∘ C loop₁ loop₂)) + ≃ q' ∘ (ap (transport C loop₂) p') ∘ ap≃ (transport-∘ C loop₂ loop₁) + + T-elim : {C : T -> Set} + (a' : C base) + (p' : transport C loop₁ a' ≃ a') + (q' : transport C loop₂ a' ≃ a') + (f' : CommutatorDep {C} a' p' q') + -> (x : T) -> C x + T-elim a _ _ _ Base = a + + postulate {- HoTT Axiom -} + βloop₁/rec : {C : Set} + -> (a : C) + -> (p q : a ≃ a) + -> (f : (p ∘ q) ≃ (q ∘ p)) + -> ap (T-rec a p q f) loop₁ ≃ p + + βloop₂/rec : {C : Set} + -> (a : C) + -> (p q : a ≃ a) + -> (f : (p ∘ q) ≃ (q ∘ p)) + -> ap (T-rec a p q f) loop₂ ≃ q + + ap-f : {X : Set} + -> (p : T -> X) + -> Id (ap p (loop₁ ∘ loop₂)) (ap p (loop₂ ∘ loop₁)) ≃ + Id (ap p loop₁ ∘ ap p loop₂) (ap p loop₂ ∘ ap p loop₁) + ap-f p = + Id (ap p (loop₁ ∘ loop₂)) (ap p (loop₂ ∘ loop₁)) + ≃〈 ap2 (λ x x' → Id x x') + (ap-∘ p loop₁ loop₂) + (ap-∘ p loop₂ loop₁) 〉 + Id (ap p loop₁ ∘ ap p loop₂) (ap p loop₂ ∘ ap p loop₁) ∎ + + f-aps : {C : Set} + -> (a : C) + -> (p q : a ≃ a) + -> (f' : (p ∘ q) ≃ (q ∘ p)) + -> Id (ap (T-rec a p q f') (loop₁ ∘ loop₂)) (ap (T-rec a p q f') (loop₂ ∘ loop₁)) + ≃ Id (p ∘ q) (q ∘ p) + f-aps a p q f' = + (Id (ap (T-rec a p q f') (loop₁ ∘ loop₂)) + (ap (T-rec a p q f') (loop₂ ∘ loop₁))) + ≃〈 ap-f (T-rec a p q f') 〉 + (Id (ap (T-rec a p q f') loop₁ ∘ ap (T-rec a p q f') loop₂) + (ap (T-rec a p q f') loop₂ ∘ ap (T-rec a p q f') loop₁)) + ≃〈 ap2 (λ x y → Id x y) + (ap2 (λ x x' → x ∘ x') (βloop₁/rec a p q f') (βloop₂/rec a p q f')) + (ap2 (λ x x' → x ∘ x') (βloop₂/rec a p q f') (βloop₁/rec a p q f')) 〉 + (Id (p ∘ q) (q ∘ p)) ∎ + + postulate {- HoTT Axiom -} + βf/rec : {C : Set} + -> (a : C) + -> (p q : a ≃ a) + -> (f' : (p ∘ q) ≃ (q ∘ p)) + -> ap (ap (T-rec a p q f')) f ≃ transport (λ x → x) (! (f-aps a p q f')) f' + + postulate {- HoTT Axiom -} + -- FIXME: prove using dependent elim instead + Tη : {X : Set} {g : T -> X} -> + g ≃ (T-rec (g base) (ap g loop₁) (ap g loop₂) (ap-∘ g loop₂ loop₁ ∘ ap (ap g) f ∘ ! (ap-∘ g loop₁ loop₂))) - postulate {- HoTT Axiom -} - -- FIXME: prove using dependent elim instead - Tη : {X : Set} {g : T -> X} -> - g ≃ (T-rec (g base) (ap g loop₁) (ap g loop₂) (ap-∘ g loop₂ loop₁ ∘ ap (ap g) f ∘ ! (ap-∘ g loop₁ loop₂))) + open T public + T-rec' : {X : Set} + -> (Σ[ x ∶ X ] (Σ[ l1 ∶ Id x x ] (Σ[ l2 ∶ Id x x ] Id (l1 ∘ l2) (l2 ∘ l1)))) + -> (T -> X) + T-rec' (x , l1 , l2 , comm) = T-rec x l1 l2 comm - module T-Lemmas where - open Torus - - rec-to-torus-X : {X : Set} - -> (Σ[ x ∶ X ] (Σ[ l1 ∶ Id x x ] (Σ[ l2 ∶ Id x x ] Id (l1 ∘ l2) (l2 ∘ l1)))) - -> (T -> X) - rec-to-torus-X (x , l1 , l2 , comm) = T-rec x l1 l2 comm + postulate + ump : ∀ {X} → IsEquiv (T-rec'{X}) + {- rec-to-torus-X-isWEq : ∀ {X} -> WEqBy _ _ (rec-to-torus-X{X})
25 oldlib/applications/torus2/TS1S1-helpers.agda
 @@ -114,31 +114,6 @@ module applications.torus2.TS1S1-helpers where curry-iso : ∀ {A B C : Set} -> (A × B -> C) ≃ (A -> B -> C) curry-iso = ua (isoToAdj (curry , isiso uncurry curry-uncurry-id uncurry-curry-id)) - -- Generalized associativity proof for dependent sums - dep-sum-assoc : {X : Set} - -> {A : X -> Set} - -> {B : (Σ[ x ∶ X ] (A x)) -> Set} - -> (Σ[ p ∶ (Σ[ x ∶ X ] (A x)) ] (B p)) - -> Σ[ x  ∶ X ] (Σ[ l1 ∶ A x ] (B (x , l1))) - dep-sum-assoc ((fst , snd) , snd') = fst , (snd , snd') - - dep-sum-unassoc : {X : Set} - -> {A : X -> Set} - -> {B : (Σ[ x ∶ X ] (A x)) -> Set} - -> Σ[ x ∶ X ] (Σ[ l1 ∶ A x ] (B (x , l1))) - -> (Σ[ p ∶ (Σ[ x ∶ X ] (A x)) ] (B p)) - dep-sum-unassoc (fst , fst' , snd) = (fst , fst') , snd - - dep-sum-assoc-equiv : {X : Set} - -> {A : X -> Set} - -> {B : (Σ[ x ∶ X ] (A x)) -> Set} - -> (Σ[ p ∶ (Σ[ x ∶ X ] (A x)) ] (B p)) - ≃ (Σ[ x  ∶ X ] (Σ[ l1 ∶ A x ] (B (x , l1)))) - dep-sum-assoc-equiv = ua (isoToAdj (dep-sum-assoc , - isiso dep-sum-unassoc - (λ y → Refl) - (λ x → Refl))) - -- Isomorphism to perform a resp inside Σ's Σ-A-A' : {X : Set} -> {A A' : X -> Set}