From 4473169b7bd020a68db7f4a9b493e00c37614397 Mon Sep 17 00:00:00 2001 From: Perry Hart Date: Sun, 15 Dec 2024 18:03:19 -0600 Subject: [PATCH] 2-coherence of truncation, newer Agda version, etc. (#9) * first commit * adding basic A-homotopy operations * adding truncation functor on coslices * finished 2-coherence proof * update Dockerfile * update to Agda 2.6.4.3 * define ptd homotopy via == instead of =-= * new name for helper function * fix function name --- Colimit-code/Aux/Coslice.agda | 60 ++++- Colimit-code/Aux/Diagram.agda | 2 +- Colimit-code/Map-Nat/CosColimitMap18.agda | 14 +- Colimit-code/Map-Nat/CosColimitPstCmp.agda | 22 +- Colimit-code/README.md | 2 +- Colimit-code/Trunc-Cos/TruncAdj.agda | 107 +++++++++ Colimit-code/cos-colim.agda-lib | 1 + Dockerfile | 6 +- HoTT-Agda/README.md | 2 +- HoTT-Agda/core/lib/PathFunctor.agda | 8 + HoTT-Agda/core/lib/PathOver.agda | 10 +- HoTT-Agda/core/lib/types/Homogeneous.agda | 49 ++-- HoTT-Agda/core/lib/types/Pointed.agda | 40 ++-- HoTT-Agda/core/lib/types/Suspension.agda | 22 +- HoTT-Agda/core/lib/types/Truncation.agda | 226 ++++++++++++++++++ .../theorems/homotopy/SuspAdjointLoop.agda | 40 ++-- Pullback-stability/README.md | 2 +- README.md | 2 +- 18 files changed, 507 insertions(+), 108 deletions(-) create mode 100644 Colimit-code/Trunc-Cos/TruncAdj.agda create mode 100644 HoTT-Agda/core/lib/types/Truncation.agda diff --git a/Colimit-code/Aux/Coslice.agda b/Colimit-code/Aux/Coslice.agda index 24cc01d..833e9cb 100644 --- a/Colimit-code/Aux/Coslice.agda +++ b/Colimit-code/Aux/Coslice.agda @@ -29,9 +29,9 @@ infixr 40 <_>_∘_ infixr 30 [_,_]_∼_ [_,_]_∼_ : ∀ {i j k} (A : Type j) (X : Coslice i j A) {Y : Coslice k j A} → - < A > X *→ Y → < A > X *→ Y → Type (lmax (lmax i k) j) + < A > X *→ Y → < A > X *→ Y → Type (lmax (lmax i k) j) [ A , *[ X , f ] ] ( h₁ , p₁ )∼( h₂ , p₂ ) = Σ ((x : X) → h₁ x == h₂ x) - (λ H → ((a : A) → (! (H (f a)) ∙ (p₁ a) == p₂ a) )) + (λ H → ((a : A) → (! (H (f a)) ∙ (p₁ a) == p₂ a))) module MapsCos {j : ULevel} (A : Type j) where @@ -46,5 +46,59 @@ module MapsCos {j : ULevel} (A : Type j) where infixr 30 <_>_∼_ <_>_∼_ : ∀ {i k} (X : Coslice i j A) {Y : Coslice k j A} → - < A > X *→ Y → < A > X *→ Y → Type (lmax (lmax i k) j) + X *→ Y → X *→ Y → Type (lmax (lmax i k) j) < X > h ∼ g = [ A , X ] h ∼ g + + *→-assoc : ∀ {i k l ℓ} {X : Coslice i j A} {Y : Coslice k j A} {Z : Coslice l j A} + {W : Coslice ℓ j A} (h₃ : Z *→ W) (h₂ : Y *→ Z) (h₁ : X *→ Y) → + < X > (h₃ ∘* h₂) ∘* h₁ ∼ h₃ ∘* (h₂ ∘* h₁) + fst (*→-assoc h₃ h₂ h₁) x = idp + snd (*→-assoc h₃ h₂ h₁) a = + ap (λ p → p ∙ ap (fst h₃) (snd h₂ a) ∙ snd h₃ a) (ap-∘ (fst h₃) (fst h₂) (snd h₁ a)) ∙ + ! (ap2-∙-∙ (fst h₃) (fst h₂) (snd h₁ a) (snd h₂ a) (snd h₃ a)) + + -- post-composition + post-∘*-∼ : ∀ {i k l} {X : Coslice i j A} {Y : Coslice k j A} {Z : Coslice l j A} + {h₁ h₂ : X *→ Y} (f : Y *→ Z) → < X > h₁ ∼ h₂ → < X > f ∘* h₁ ∼ f ∘* h₂ + fst (post-∘*-∼ f H) x = ap (fst f) (fst H x) + snd (post-∘*-∼ {X = X} {h₁ = h₁} f H) a = + ap (λ p → p ∙ ap (fst f) (snd h₁ a) ∙ snd f a) (!-ap (fst f) (fst H (fun X a))) ∙ + ! (∙-assoc (ap (fst f) (! (fst H (fun X a)))) (ap (fst f) (snd h₁ a)) (snd f a)) ∙ + ap (λ p → p ∙ snd f a) (∙-ap (fst f) (! (fst H (fun X a))) (snd h₁ a)) ∙ + ap (λ p → ap (fst f) p ∙ snd f a) (snd H a) + + -- pre-composition + pre-∘*-∼ : ∀ {i k l} {X : Coslice i j A} {Y : Coslice k j A} {Z : Coslice l j A} + {h₁ h₂ : X *→ Y} (f : Z *→ X) → < X > h₁ ∼ h₂ → < Z > h₁ ∘* f ∼ h₂ ∘* f + fst (pre-∘*-∼ f H) x = fst H (fst f x) + snd (pre-∘*-∼ {X = X} {Z = Z} {h₁ = h₁} {h₂} f H) a = + (! (∙-assoc (! (fst H (fst f (fun Z a)))) (ap (fst h₁) (snd f a)) (snd h₁ a)) ∙ + ap (λ p → p ∙ snd h₁ a) (hmtpy-nat-!-sq (fst H) (snd f a)) ∙ + ∙-assoc (ap (fst h₂) (snd f a)) (! (fst H (fun X a))) (snd h₁ a)) ∙ + ap (λ p → ap (fst h₂) (snd f a) ∙ p) (snd H a) + + -- concatenation + infixr 40 _∼∘-cos_ + _∼∘-cos_ : ∀ {i k} {X : Coslice i j A} {Y : Coslice k j A} → + {h₁ h₂ h₃ : X *→ Y} → + < X > h₁ ∼ h₂ → < X > h₂ ∼ h₃ → < X > h₁ ∼ h₃ + _∼∘-cos_ {X = X} {h₁ = h₁} (H₁ , H₂) (K₁ , K₂) = + (λ x → H₁ x ∙ K₁ x) , + (λ a → + (ap (λ p → p ∙ snd h₁ a) (!-∙ (H₁ (fun X a)) (K₁ (fun X a))) ∙ + ∙-assoc (! (K₁ (fun X a))) (! (H₁ (fun X a))) (snd h₁ a)) ∙ + ap (λ p → ! (K₁ (fun X a)) ∙ p) (H₂ a) ∙ K₂ a) + + -- identity + cos∼id : ∀ {i k} {X : Coslice i j A} {Y : Coslice k j A} (h : X *→ Y) + → < X > h ∼ h + fst (cos∼id h) = λ x → idp + snd (cos∼id h) = λ a → idp + + -- homotopy of homotopies of A-maps + infixr 30 <_>_∼∼_ + <_>_∼∼_ : ∀ {i k} (X : Coslice i j A) {Y : Coslice k j A} {h₁ h₂ : X *→ Y} → + < X > h₁ ∼ h₂ → < X > h₁ ∼ h₂ → Type (lmax k (lmax i j)) + <_>_∼∼_ X {h₁ = h₁} H₁ H₂ = + Σ (fst H₁ ∼ fst H₂) + λ K → (a : A) → ap (λ p → ! p ∙ snd h₁ a) (! (K (fun X a))) ∙ snd H₁ a == snd H₂ a diff --git a/Colimit-code/Aux/Diagram.agda b/Colimit-code/Aux/Diagram.agda index a09ab61..c440fe8 100644 --- a/Colimit-code/Aux/Diagram.agda +++ b/Colimit-code/Aux/Diagram.agda @@ -106,5 +106,5 @@ module _ {ℓi ℓj k} {A : Type ℓj} {Γ : Graph ℓv ℓe} {F : CosDiag ℓi PostComp : ∀ {k'} {D : Coslice k' ℓj A} → CosCocone A F C → (< A > C *→ D) → CosCocone A F D comp (PostComp K (f , fₚ)) i = f ∘ (fst (comp K i)) , λ a → ap f (snd (comp K i) a) ∙ fₚ a comTri (PostComp K (f , fₚ)) {y = j} {x = i} g = (λ x → ap f (fst (comTri K g) x)) , - λ a → ap-cp-revR f (fst (comp K j)) (snd (F <#> g) a) (fst (comTri K g) (fun (F # i) a)) ∙ + λ a → ap-cp-revR f (fst (comp K j)) (snd (F <#> g) a) (fst (comTri K g) (fun (F # i) a)) ∙ ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri K g) a)) diff --git a/Colimit-code/Map-Nat/CosColimitMap18.agda b/Colimit-code/Map-Nat/CosColimitMap18.agda index fbf0ca8..0710287 100644 --- a/Colimit-code/Map-Nat/CosColimitMap18.agda +++ b/Colimit-code/Map-Nat/CosColimitMap18.agda @@ -109,7 +109,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type ap (λ p → ap f p ∙ idp) (ap (λ p → ! (ap right (! (ap (cin j) (ap (fst (G <#> g)) τ₁₀ ∙ τ₁₃ ∙ idp)) ∙ p)) ∙ idp) (apCommSq2 (λ x → cin j (fst (G <#> g) x)) (λ v → cin j (fst (G <#> g) v)) (λ x → idp) τ₁₀) ∙ !-!-!-∘-∘-∘-rid (cin j) (fst (G <#> g)) (λ v → cin j (fst (G <#> g) v)) right τ₁₀ τ₁₃ idp idp idp ∙ idp)) ∙ - ap-∘-∙ f (right ∘ (λ v → cin j (fst (G <#> g) v))) τ₁₀ (ap (right ∘ cin j) τ₁₃ ∙ idp) + ap-∘-∙-∙ f (right ∘ (λ v → cin j (fst (G <#> g) v))) τ₁₀ (ap (right ∘ cin j) τ₁₃ ∙ idp) == !-!-∙-pth (ap (λ x → f (right (cin j x))) (ap (fst (G <#> g)) τ₁₀ ∙ τ₁₃ ∙ idp)) idp ∙ ap (λ p → p ∙ ap (λ x → f (right (cin j x))) (ap (fst (G <#> g)) τ₁₀ ∙ τ₁₃ ∙ idp) ∙ idp) (hmtpy-nat-! (λ x → idp) τ₁₀) ∙ @@ -145,7 +145,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type (apCommSq2 (λ x → cin j (fst (G <#> g) x)) (cin i) (cglue g) τ₁₀) ∙ !-!-!-∘-∘-∘-rid (cin j) (fst (G <#> g)) (cin i) right τ₁₀ τ₁₃ idp idp (cglue g (fun (G # i) a)) ∙ idp)) ∙ - ap-∘-∙ f (right ∘ cin i) τ₁₀ (! (ap right (cglue g (fun (G # i) a))) ∙ ap (right ∘ cin j) τ₁₃ ∙ idp) + ap-∘-∙-∙ f (right ∘ cin i) τ₁₀ (! (ap right (cglue g (fun (G # i) a))) ∙ ap (right ∘ cin j) τ₁₃ ∙ idp) == !-!-∙-pth (ap (λ x → f (right (cin j x))) (ap (fst (G <#> g)) τ₁₀ ∙ τ₁₃ ∙ idp)) (ap f (ap right (cglue g (fst (nat δ i) (fun (F # i) a))))) ∙ @@ -169,7 +169,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type (apCommSq2 (λ x → cin j (fst (G <#> g) x)) h H τ₁₀) ∙ !-!-!-∘-∘-∘-rid (cin j) (fst (G <#> g)) h right τ₁₀ τ₁₃ idp idp (H (fun (G # i) a)) ∙ idp)) ∙ - ap-∘-∙ f (right ∘ h) τ₁₀ (! (ap right (H (fun (G # i) a))) ∙ ap (right ∘ cin j) τ₁₃ ∙ idp) + ap-∘-∙-∙ f (right ∘ h) τ₁₀ (! (ap right (H (fun (G # i) a))) ∙ ap (right ∘ cin j) τ₁₃ ∙ idp) == !-!-∙-pth (ap (λ x → f (right (cin j x))) (ap (fst (G <#> g)) τ₁₀ ∙ τ₁₃ ∙ idp)) (ap f (ap right (H (fst (nat δ i) (fun (F # i) a))))) ∙ @@ -197,7 +197,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type ap (λ p → ! (ap right (! (ap (cin j) (ap (fst (G <#> g)) τ₁₀ ∙ τ₁₃ ∙ idp)) ∙ p)) ∙ idp) (apCommSq2 (λ x → cin j (fst (G <#> g) x)) (cin i) (cglue g) τ₁₀) ∙ !-!-!-∘-∘-∘-rid (cin j) (fst (G <#> g)) (cin i) right τ₁₀ τ₁₃ idp idp (cglue g (fun (G # i) a)) ∙ idp)) ∙ - ap-∘-∙ f (right ∘ cin i) τ₁₀ (! (ap right (cglue g (fun (G # i) a))) ∙ + ap-∘-∙-∙ f (right ∘ cin i) τ₁₀ (! (ap right (cglue g (fun (G # i) a))) ∙ ap (right ∘ cin j) τ₁₃ ∙ idp) == !-!-∙-pth (ap (λ x → f (right (cin j x))) σ₁) @@ -240,7 +240,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type (cglue g (fst (nat δ i) (fun (F # i) a))))) ∙ idp) ∙ ap (f ∘ right ∘ cin j ∘ fst (nat δ j)) τ₅ ∙ ap (f ∘ right ∘ cin j) τ₆ ∙ ap f τ₇ ∙ τ₈) - (ap-∘-∙ f (right ∘ cin j) τ₆ τ₇) ◃∙ + (ap-∘-∙-∙ f (right ∘ cin j) τ₆ τ₇) ◃∙ long-path-red τ₅ (ap (f ∘ right ∘ cin j) τ₆ ∙ ap f τ₇ ∙ τ₈) (ap f (ap (λ x → right (cin j x)) τ₆ ∙ @@ -264,7 +264,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type right τ₁₀ τ₁₃ τ₅ τ₆ (cglue g (fun (G # i) a)) τ₇ ∙ ap (_∙_ (ap (λ x → right (cin i x)) τ₁₀)) τ₁)) ◃∙ - ap-∘-∙ f (right ∘ cin i) τ₁₀ τ₁₁ ◃∎ + ap-∘-∙-∙ f (right ∘ cin i) τ₁₀ τ₁₁ ◃∎ =ₛ (!-!-∙-pth (ap (λ x → f (right (cin j x))) (comSq δ g (fun (F # i) a))) (ap f (ap right (cglue g (fst (nat δ i) (fun (F # i) a))))) ∙ @@ -309,7 +309,7 @@ module ConstrMap19 {ℓv ℓe ℓ ℓF ℓG} {Γ : Graph ℓv ℓe} {A : Type CosColim-NatSq2 : CosCocEq F T (Map-to-Lim-map F (f , fₚ) K-diag) (Diag-to-Lim-map (PostComp ColCoC (f , fₚ))) W CosColim-NatSq2 i x = idp - u CosColim-NatSq2 i a = ap-∘-∙ f (right ∘ cin i) (snd (nat δ i) a) (! (glue (cin i a))) + u CosColim-NatSq2 i a = ap-∘-∙-∙ f (right ∘ cin i) (snd (nat δ i) a) (! (glue (cin i a))) Λ CosColim-NatSq2 {i} {j} g = (λ x → ap-∘-∘-!-∙-rid f right (cin j) (comSq δ g x) (cglue g (fst (nat δ i) x))) , λ a → NatSq2-Λ-coher g a (snd (F <#> g) a) (snd (nat δ j) a) (! (glue (cin j a))) (fₚ a) (snd (nat δ i) a) (snd (G <#> g) a) (comSq-coher δ g a) diff --git a/Colimit-code/Map-Nat/CosColimitPstCmp.agda b/Colimit-code/Map-Nat/CosColimitPstCmp.agda index 827fe1f..6c3b9fd 100644 --- a/Colimit-code/Map-Nat/CosColimitPstCmp.agda +++ b/Colimit-code/Map-Nat/CosColimitPstCmp.agda @@ -14,9 +14,9 @@ module CosColimitPstCmp where module _ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁} {B : Type ℓ₂} {C : Type ℓ₃} (h : B → C) (f : A → B) where - ap-∘-∙ : {x y : A} (p₁ : x == y) {z : B} (p₂ : f y == z) {c : C} {s : h z == c} + ap-∘-∙-∙ : {x y : A} (p₁ : x == y) {z : B} (p₂ : f y == z) {c : C} {s : h z == c} → ap h (ap f p₁ ∙ p₂) ∙ s == ap (h ∘ f) p₁ ∙ ap h p₂ ∙ s - ap-∘-∙ idp p₂ = idp + ap-∘-∙-∙ idp p₂ = idp ap-∘-rid : {x y : A} (p : x == y) → ap h (ap f p) ∙ idp == ap (h ∘ f) p ap-∘-rid idp = idp @@ -71,7 +71,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type ap φ₁ (ap f p₁) ∙ idp) ∙ ap (φ₁ ∘ f ∘ right ∘ cin j) p₂ ∙ ap (φ₁ ∘ f) p₃ ∙ ap φ₁ p₄ ∙ p₅)) - (ap-∘-∙ φ₁ f p₃ p₄) ◃∙ + (ap-∘-∙-∙ φ₁ f p₃ p₄) ◃∙ long-path-red p₂ (ap (φ₁ ∘ f) p₃ ∙ ap φ₁ p₄ ∙ p₅) @@ -98,7 +98,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type ap (λ p → ap φ₁ p ∙ φ₂ a) (ap-cp-revR f (right ∘ cin j) p₂ p₁ ∙ ap (λ p → p ∙ fₚ a) (ap (ap f) τ))) ◃∙ - ap-∘-∙ φ₁ f σ (fₚ a) ◃∎ + ap-∘-∙-∙ φ₁ f σ (fₚ a) ◃∎ =ₛ (ap-cp-revR (φ₁ ∘ f) (right ∘ cin j) p₂ p₁ ∙ @@ -107,14 +107,14 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type NatSq-1-Λ-red2 {i} {j} g a idp idp p₃ idp = =ₛ-in (lemma p₃ (fₚ a)) where lemma : {z : P} (p : right (cin j (fst (F <#> g) (fun (F # i) a))) == z) (c : f z == fun T a) - → ↯ (NatSq-1-Λ-aux g a idp idp p c (φ₂ a)) ∙ ap-∘-∙ φ₁ f p c == idp + → ↯ (NatSq-1-Λ-aux g a idp idp p c (φ₂ a)) ∙ ap-∘-∙-∙ φ₁ f p c == idp lemma idp c = idp -- τ = (snd (comTri ColCoC g) a) CosColim-NatSq1 : CosCocEq F U (Map-to-Lim-map (PostComp ColCoC (f , fₚ))) (PostComp ColCoC (φ ∘* (f , fₚ))) W CosColim-NatSq1 = λ i x → idp - u CosColim-NatSq1 = λ i a → ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) + u CosColim-NatSq1 = λ i a → ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) Λ CosColim-NatSq1 {i} {j} g = (λ x → ap-∘-rid φ₁ f (fst (comTri ColCoC g) x)) , λ a → lemma a where lemma : (a : A) → @@ -133,7 +133,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type ap φ₁ (ap f (fst (comTri ColCoC g) (fun (F # i) a))) ∙ idp) ∙ ap (φ₁ ∘ f ∘ fst (comp ColCoC j)) (snd (F <#> g) a) ∙ ap (φ₁ ∘ f) (snd (comp ColCoC j) a) ∙ - snd (φ ∘* f , fₚ) a) (ap-∘-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙ + snd (φ ∘* f , fₚ) a) (ap-∘-∙-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙ long-path-red (snd (F <#> g) a) (ap (φ₁ ∘ f) (! (glue (cin j a))) ∙ ap (fst φ) (fₚ a) ∙ snd φ a) (ap (fst φ) (ap f (! (glue (cin j a))) ∙ fₚ a) ∙ snd φ a) (ap φ₁ (ap f (ap right (cglue g (fun (F # i) a))))) idp ◃∙ -- here @@ -143,7 +143,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type (ap-cp-revR f (fst (comp ColCoC j)) (snd (F <#> g) a) (fst (comTri ColCoC g) (fun (F # i) a)) ∙ ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri ColCoC g) a)))) ◃∙ - ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎ + ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎ =ₛ (ap-cp-revR (φ₁ ∘ f) (fst (comp ColCoC j)) (snd (F <#> g) a) (fst (comTri ColCoC g) (fun (F # i) a)) ∙ @@ -165,7 +165,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type ap φ₁ (ap f (fst (comTri ColCoC g) (fun (F # i) a))) ∙ idp) ∙ ap (φ₁ ∘ f ∘ fst (comp ColCoC j)) (snd (F <#> g) a) ∙ ap (φ₁ ∘ f) (snd (comp ColCoC j) a) ∙ - snd (φ ∘* f , fₚ) a) (ap-∘-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙ + snd (φ ∘* f , fₚ) a) (ap-∘-∙-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙ long-path-red (snd (F <#> g) a) (ap (φ₁ ∘ f) (! (glue (cin j a))) ∙ ap (fst φ) (fₚ a) ∙ snd φ a) (ap (fst φ) (ap f (! (glue (cin j a))) ∙ fₚ a) ∙ snd φ a) (ap φ₁ (ap f (ap right (cglue g (fun (F # i) a))))) idp ◃∙ @@ -175,7 +175,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type (ap-cp-revR f (fst (comp ColCoC j)) (snd (F <#> g) a) (fst (comTri ColCoC g) (fun (F # i) a)) ∙ ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri ColCoC g) a)))) ◃∙ - ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎ + ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎ =ₛ⟨ 0 & 4 & NatSq-1-Λ-red g a (ap right (cglue g (fun (F # i) a))) (snd (F <#> g) a) (! (glue (cin j a))) (fₚ a) (φ₂ a) ⟩ ↯ (NatSq-1-Λ-aux g a (ap right (cglue g (fun (F # i) a))) (snd (F <#> g) a) (! (glue (cin j a))) (fₚ a) (φ₂ a)) ◃∙ ap (λ q → q) (ap-cp-revR φ₁ (f ∘ fst (comp ColCoC j)) (snd (F <#> g) a) @@ -184,7 +184,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type (ap-cp-revR f (fst (comp ColCoC j)) (snd (F <#> g) a) (fst (comTri ColCoC g) (fun (F # i) a)) ∙ ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri ColCoC g) a)))) ◃∙ - ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎ + ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎ =ₛ⟨ NatSq-1-Λ-red2 g a (ap right (cglue g (fun (F # i) a))) (snd (F <#> g) a) (! (glue (cin j a))) (snd (comTri ColCoC g) a) ⟩ (ap-cp-revR (φ₁ ∘ f) (fst (comp ColCoC j)) (snd (F <#> g) a) (fst (comTri ColCoC g) (fun (F # i) a)) ∙ diff --git a/Colimit-code/README.md b/Colimit-code/README.md index a40194a..f2d21cd 100644 --- a/Colimit-code/README.md +++ b/Colimit-code/README.md @@ -50,7 +50,7 @@ check the entire development in a reasonable amount of time. ## Manual Type-Checking -1. Install Agda 2.6.3. +1. Install Agda 2.6.4.3. 2. Install the stripped, modified HoTT-Agda library under `../HoTT-Agda`. 3. Type-check the file `Main-Theorem/CosColim-Adjunction.agda`. diff --git a/Colimit-code/Trunc-Cos/TruncAdj.agda b/Colimit-code/Trunc-Cos/TruncAdj.agda new file mode 100644 index 0000000..104e55c --- /dev/null +++ b/Colimit-code/Trunc-Cos/TruncAdj.agda @@ -0,0 +1,107 @@ +{-# OPTIONS --without-K --rewriting --overlapping-instances #-} + +open import lib.Basics +open import lib.types.Truncation +open import Coslice + +module TruncAdj where + +module _ {j} (A : Type j) where + + open MapsCos A + + module _ (n : ℕ₋₂) where + + -- truncation functor on coslices + + Trunc-cos : ∀ {i} → (Coslice i j A) → (Coslice i j A) + ty (Trunc-cos *[ ty , fun ]) = Trunc n ty + Coslice.fun (Trunc-cos *[ ty , fun ]) a = [ fun a ] + + Trunc-cos-fmap : ∀ {i k} {X : Coslice i j A} {Y : Coslice k j A} + → ((X *→ Y) → (Trunc-cos X *→ Trunc-cos Y)) + Trunc-cos-fmap F = Trunc-fmap (fst F) , λ a → ap [_] (snd F a) + + Trunc-cos-fmap-∘ : ∀ {i k ℓ} {X : Coslice i j A} {Y : Coslice k j A} {Z : Coslice ℓ j A} + → (g : Y *→ Z) (f : X *→ Y) + → < Trunc-cos X > Trunc-cos-fmap (g ∘* f) ∼ Trunc-cos-fmap g ∘* Trunc-cos-fmap f + fst (Trunc-cos-fmap-∘ g f) = Trunc-elim (λ _ → idp) + snd (Trunc-cos-fmap-∘ g f) a = + ap-∘-∙ [_] (fst g) (snd f a) (snd g a) ∙ + ap (λ p → p ∙ ap [_] (snd g a)) (ap-∘ (Trunc-elim (λ x → [ fst g x ])) [_] (snd f a)) + + -- hom map of the adjunction + Trunc-cos-hom : ∀ {i k} {X : Coslice i j A} {Y : Coslice k j A} + {{p : has-level n (ty Y)}} → (Trunc-cos X *→ Y) → (X *→ Y) + fst (Trunc-cos-hom f) = fst f ∘ [_] + snd (Trunc-cos-hom f) a = snd f a + + -- naturality of hom map + Trunc-cos-∘-nat : ∀ {i k ℓ} {X : Coslice i j A} {Y : Coslice k j A} {Z : Coslice ℓ j A} + {{p : has-level n (ty Y)}} (f : Z *→ X) (h : Trunc-cos X *→ Y) + → < Z > Trunc-cos-hom h ∘* f ∼ Trunc-cos-hom (h ∘* Trunc-cos-fmap f) + fst (Trunc-cos-∘-nat f h) x = idp + snd (Trunc-cos-∘-nat f h) a = ap (λ p → p ∙ snd h a) (ap-∘ (fst h) [_] (snd f a)) + + ap-Trunc-cos-hom : ∀ {i k} {X : Coslice i j A} {Y : Coslice k j A} {{p : has-level n (ty Y)}} + {h₁ h₂ : Trunc-cos X *→ Y} → < Trunc-cos X > h₁ ∼ h₂ → < X > Trunc-cos-hom h₁ ∼ Trunc-cos-hom h₂ + fst (ap-Trunc-cos-hom H) x = fst H [ x ] + snd (ap-Trunc-cos-hom H) a = snd H a + + -- Our custom ap function behaves as expected + ap-Trunc-cos-hom-id : ∀ {i k} {X : Coslice i j A} {Y : Coslice k j A} {{p : has-level n (ty Y)}} + (f : Trunc-cos X *→ Y) → < X > ap-Trunc-cos-hom (cos∼id f) ∼∼ cos∼id (Trunc-cos-hom f) + fst (ap-Trunc-cos-hom-id f) x = idp + snd (ap-Trunc-cos-hom-id f) a = idp + + -- Truncation on coslices is a 2-coherent left adjoint + + module _ {i₁ i₂ i₃ i₄} + {X : Coslice i₁ j A} {Y : Coslice i₂ j A} {Z : Coslice i₃ j A} {W : Coslice i₄ j A} + {{p : has-level n (ty Y)}} + (f₂ : Z *→ X) (f₃ : W *→ Z) (f₁ : Trunc-cos X *→ Y) where + + two-coher-Trunc-cos : + < W > + (pre-∘*-∼ f₃ (Trunc-cos-∘-nat f₂ f₁)) ∼∘-cos + Trunc-cos-∘-nat f₃ (f₁ ∘* Trunc-cos-fmap f₂) ∼∘-cos + ap-Trunc-cos-hom (*→-assoc f₁ (Trunc-cos-fmap f₂) (Trunc-cos-fmap f₃)) + ∼∼ + *→-assoc (Trunc-cos-hom f₁) f₂ f₃ ∼∘-cos + Trunc-cos-∘-nat (f₂ ∘* f₃) f₁ ∼∘-cos + ap-Trunc-cos-hom (post-∘*-∼ f₁ (Trunc-cos-fmap-∘ f₂ f₃)) + fst two-coher-Trunc-cos x = idp + snd two-coher-Trunc-cos a = lemma a (snd f₃ a) + where + lemma : (a : A) {w : ty Z} (τ : w == fun Z a) → + ap (λ q → q) ((ap (λ p₁ → p₁ ∙ ap (λ x → fst f₁ [ x ]) + (snd f₂ a) ∙ snd f₁ a) + (hmtpy-nat-!-sq (λ x → idp) τ) ∙ + ∙-assoc (ap (λ z → fst f₁ [ fst f₂ z ]) τ) idp + (ap (λ x → fst f₁ [ x ]) (snd f₂ a) ∙ snd f₁ a)) ∙ + ap (_∙_ (ap (λ z → fst f₁ [ fst f₂ z ]) τ)) + (ap (λ p₁ → p₁ ∙ snd f₁ a) (ap-∘ (fst f₁) [_] (snd f₂ a)))) ∙ + ap (λ q → q) (ap (λ p₁ → p₁ ∙ ap (fst f₁) + (ap [_] (snd f₂ a)) ∙ snd f₁ a) + (ap-∘ (λ x → fst f₁ (Trunc-elim (λ x₁ → [ fst f₂ x₁ ]) x)) + [_] τ)) ∙ + ap (λ p₁ → p₁ ∙ ap (fst f₁) (ap [_] (snd f₂ a)) ∙ snd f₁ a) + (ap-∘ (fst f₁) (Trunc-elim (λ x → [ fst f₂ x ])) + (ap [_] τ)) ∙ + ! (ap2-∙-∙ (fst f₁) (Trunc-elim (λ x → [ fst f₂ x ])) + (ap [_] τ) (ap [_] (snd f₂ a)) (snd f₁ a)) + == + ap (λ q → q) (ap (λ p₁ → p₁ ∙ ap (λ x → fst f₁ [ x ]) + (snd f₂ a) ∙ snd f₁ a) + (ap-∘ (λ x → fst f₁ [ x ]) (fst f₂) τ) ∙ + ! (ap2-∙-∙ (λ x → fst f₁ [ x ]) (fst f₂) τ + (snd f₂ a) (snd f₁ a))) ∙ + ap (λ q → q) (ap (λ p₁ → p₁ ∙ snd f₁ a) + (ap-∘ (fst f₁) [_] (ap (fst f₂) τ ∙ snd f₂ a))) ∙ + ap (λ p₁ → ap (fst f₁) p₁ ∙ snd f₁ a) + (ap-∘-∙ [_] (fst f₂) τ (snd f₂ a) ∙ + ap (λ p₁ → p₁ ∙ ap [_] (snd f₂ a)) + (ap-∘ (Trunc-elim (λ x → [ fst f₂ x ])) [_] τ)) + lemma a idp = + ap (λ p → p ∙ idp) (ap-idf (ap (λ q → q) + (ap (λ p₁ → p₁ ∙ snd f₁ a) (ap-∘ (fst f₁) [_] (snd f₂ a))))) diff --git a/Colimit-code/cos-colim.agda-lib b/Colimit-code/cos-colim.agda-lib index 1de2656..1b1aa2e 100644 --- a/Colimit-code/cos-colim.agda-lib +++ b/Colimit-code/cos-colim.agda-lib @@ -6,3 +6,4 @@ include: R-L-R Aux Main-Theorem + Trunc-Cos diff --git a/Dockerfile b/Dockerfile index 21c6a4f..3b22924 100644 --- a/Dockerfile +++ b/Dockerfile @@ -6,8 +6,8 @@ ARG GHC_VERSION=9.4.7 FROM fossa/haskell-static-alpine:ghc-${GHC_VERSION} AS agda WORKDIR /build/agda -# Agda 2.6.3 -ARG AGDA_VERSION=b499d12412bac32ab1af9f470463ed9dc54f8907 +# Agda 2.6.4.3 +ARG AGDA_VERSION=714c7d2c76c5ffda3180e95c28669259f0dc5b5c RUN \ git init && \ git remote add origin https://github.com/agda/agda.git && \ @@ -49,6 +49,8 @@ WORKDIR /build/HoTT-Agda RUN /dist/agda --library-file=/dist/libraries ./theorems/homotopy/SuspAdjointLoop.agda WORKDIR /build/Colimit-code +RUN /dist/agda --library-file=/dist/libraries ./Trunc-Cos/TruncAdj.agda + RUN /dist/agda --library-file=/dist/libraries ./R-L-R/CC-Equiv-RLR-0.agda RUN /dist/agda --library-file=/dist/libraries ./R-L-R/CC-Equiv-RLR-1.agda RUN /dist/agda --library-file=/dist/libraries ./R-L-R/CC-Equiv-RLR-2.agda diff --git a/HoTT-Agda/README.md b/HoTT-Agda/README.md index c9cc8fb..842f400 100644 --- a/HoTT-Agda/README.md +++ b/HoTT-Agda/README.md @@ -10,7 +10,7 @@ lemmas. The structure of the source code is described below. Setup ----- -The library is compatible with Agda 2.6.3. To use it, you need a recent version of Agda and to include at +The library is compatible with Agda 2.6.4.3. To use it, you need a recent version of Agda and to include at least the path to `hott-core.agda-lib` in your Agda library list. Agda Options diff --git a/HoTT-Agda/core/lib/PathFunctor.agda b/HoTT-Agda/core/lib/PathFunctor.agda index e380111..080321d 100644 --- a/HoTT-Agda/core/lib/PathFunctor.agda +++ b/HoTT-Agda/core/lib/PathFunctor.agda @@ -139,10 +139,18 @@ module _ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → ap-∘ : {x y : A} (p : x == y) → ap (g ∘ f) p == ap g (ap f p) ap-∘ idp = idp + ap-∘-∙ : {x y : A} (p : x == y) {b : B} (q : f y == b) + → ap g (ap f p ∙ q) == ap (g ∘ f) p ∙ ap g q + ap-∘-∙ idp q = idp + ap-∘-∘ : ∀ {l} {D : Type l} (h : D → A) {x y : D} (p : x == y) → ap (g ∘ f ∘ h) p == ap g (ap f (ap h p)) ap-∘-∘ h idp = idp + ap2-∙-∙ : {x y : A} (p₁ : x == y) {b : B} (p₂ : f y == b) {c : C} (p₃ : g b == c) + → ap g (ap f p₁ ∙ p₂) ∙ p₃ == ap g (ap f p₁) ∙ ap g p₂ ∙ p₃ + ap2-∙-∙ idp p₂ p₃ = idp + !ap-∘=∘-ap : {x y : A} (p : x == y) → ! (ap-∘ p) == ∘-ap p !ap-∘=∘-ap idp = idp diff --git a/HoTT-Agda/core/lib/PathOver.agda b/HoTT-Agda/core/lib/PathOver.agda index a20e710..52ea716 100644 --- a/HoTT-Agda/core/lib/PathOver.agda +++ b/HoTT-Agda/core/lib/PathOver.agda @@ -385,10 +385,10 @@ module _ {i j} {X : Ptd i} {Y : Ptd j} where infixr 30 _⊙-comp_ _⊙-comp_ : (f g : X ⊙→ Y) → Type (lmax i j) - _⊙-comp_ f g = Σ (fst f ∼ fst g) λ H → ! (H (pt X)) ∙ snd f =-= snd g + _⊙-comp_ f g = Σ (fst f ∼ fst g) λ H → ! (H (pt X)) ∙ snd f == snd g - comp-⊙∼ : {f g : X ⊙→ Y} (H : f ⊙∼ g) → ! (fst H (pt X)) ∙ snd f =-= snd g - comp-⊙∼ {f = f} H = ! (transp-cst=idf-l (fst H (pt X)) (snd f)) ◃∙ to-transp (snd H) ◃∎ + comp-⊙∼ : {f g : X ⊙→ Y} (H : f ⊙∼ g) → ! (fst H (pt X)) ∙ snd f == snd g + comp-⊙∼ {f = f} H = ! (transp-cst=idf-l (fst H (pt X)) (snd f)) ∙ to-transp (snd H) ⊙-to-comp : {f g : X ⊙→ Y} → f ⊙∼ g → f ⊙-comp g ⊙-to-comp H = fst H , comp-⊙∼ H @@ -396,11 +396,11 @@ module _ {i j} {X : Ptd i} {Y : Ptd j} where comp-to-⊙ : {f g : X ⊙→ Y} → f ⊙-comp g → f ⊙∼ g fst (comp-to-⊙ H) = fst H snd (comp-to-⊙ {f} H) = - from-transp (_== pt Y) (fst H (pt X)) (transp-cst=idf-l (fst H (pt X)) (snd f) ∙ ↯ (snd H)) + from-transp (_== pt Y) (fst H (pt X)) (transp-cst=idf-l (fst H (pt X)) (snd f) ∙ snd H) ⊙id-to-comp : {f g : X ⊙→ Y} (p : f == g) → f ⊙-comp g fst (⊙id-to-comp idp) = λ x → idp - snd (⊙id-to-comp idp) = idp ◃∎ + snd (⊙id-to-comp idp) = idp {- Various other lemmas -} diff --git a/HoTT-Agda/core/lib/types/Homogeneous.agda b/HoTT-Agda/core/lib/types/Homogeneous.agda index 5a8e9dc..24e2542 100644 --- a/HoTT-Agda/core/lib/types/Homogeneous.agda +++ b/HoTT-Agda/core/lib/types/Homogeneous.agda @@ -46,7 +46,7 @@ module _ {i} {X : Type i} where has-sect⊙.sect⊙-eq (⊙∼-eval-sect (homog auto homog-idf)) = ⊙λ= (comp-to-⊙ ((λ x → app= (ap (fst ∘ ⊙Ω-fmap) homog-idf ∙ ap fst ⊙Ω-fmap-idf) x) , - pathseq)) + ↯ pathseq)) where lemma : {m : ⊙[ X , f z ] ⊙→ ⊙[ X , f z ]} (τ : m == ⊙idf ⊙[ X , f z ]) → ! (ap (λ u → u idp) (ap (fst ∘ ⊙Ω-fmap) τ) ∙ idp) ∙ @@ -117,58 +117,58 @@ module _ {i} {X : Type i} where ∼⊙homog= : (x : X) {g : Z → X} {fₚ : f z == x} {gₚ : g z == x} {H₁ H₂ : f == g} - {H₁ₚ : ! (app= H₁ z) ∙ fₚ =-= gₚ} - {H₂ₚ : ! (app= H₂ z) ∙ fₚ =-= gₚ} + {H₁ₚ : ! (app= H₁ z) ∙ fₚ == gₚ} + {H₂ₚ : ! (app= H₂ z) ∙ fₚ == gₚ} → H₁ == H₂ → (app= H₁ , H₁ₚ) ⊙→∼ (app= H₂ , H₂ₚ) fst (∼⊙homog= x {fₚ = idp} {H₁ = idp} {H₁ₚ = H₁ₚ} {H₂ₚ} idp) = λ x₁ → app= (fst (r-inv (⊙∼-evalΩ-sect η)) - (ap-post∙idp∘!-inv (↯ (H₁ₚ) ∙ ! (↯ (H₂ₚ))))) x₁ + (ap-post∙idp∘!-inv (H₁ₚ ∙ ! (H₂ₚ)))) x₁ snd (∼⊙homog= x {fₚ = idp} {H₁ = idp} {H₁ₚ = H₁ₚ} {H₂ₚ} idp) = post↯-rotate-in (=ₛ-in (ap (ap (λ p → ! p ∙ idp)) (app= (ap fst (sect⊙-eq (⊙∼-evalΩ-sect η))) - (ap-post∙idp∘!-inv (↯ (H₁ₚ) ∙ ! (↯ (H₂ₚ))))) ∙ + (ap-post∙idp∘!-inv (H₁ₚ ∙ ! (H₂ₚ)))) ∙ <–-inv-r (ap-equiv (post∙idp∘!-is-equiv) idp idp) - (↯ (H₁ₚ) ∙ ! (↯ (H₂ₚ))))) + (H₁ₚ ∙ ! (H₂ₚ)))) ∼⊙homog∼ : (x : X) {g : Z → X} {fₚ : f z == x} {gₚ : g z == x} {H₁ H₂ : f ∼ g} - {H₁ₚ : ! (H₁ z) ∙ fₚ =-= gₚ} - {H₂ₚ : ! (H₂ z) ∙ fₚ =-= gₚ} + {H₁ₚ : ! (H₁ z) ∙ fₚ == gₚ} + {H₂ₚ : ! (H₂ z) ∙ fₚ == gₚ} → H₁ ∼ H₂ → (H₁ , H₁ₚ) ⊙→∼ (H₂ , H₂ₚ) fst (∼⊙homog∼ x {fₚ = idp} {gₚ} {H₁} {H₂} {H₁ₚ} {H₂ₚ} K) t = ! (app=-β H₁ t) ∙ fst (∼⊙homog= x {fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂} - {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎} - {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎} + {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ H₁ₚ)} + {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ H₂ₚ)} (ap λ= (λ= K))) t ∙ app=-β H₂ t snd (∼⊙homog∼ x {fₚ = idp} {gₚ} {H₁} {H₂} {H₁ₚ} {H₂ₚ} K) = ap (λ p → ! p ∙ idp) (! (app=-β H₁ z) ∙ fst (∼⊙homog= (f z) {fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂} - {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎} - {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎} + {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ H₁ₚ)} + {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ H₂ₚ)} (ap λ= (λ= K))) z ∙ app=-β H₂ z) ◃∙ - H₂ₚ + H₂ₚ ◃∎ =ₛ₁⟨ 0 & 1 & ap-!∙∙ (λ p → ! p ∙ idp) (app=-β H₁ z) (fst (∼⊙homog= (f z) {fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂} - {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎} - {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎} + {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ H₁ₚ)} + {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ H₂ₚ)} (ap λ= (λ= K))) z) (app=-β H₂ z) ⟩ ↯ (! (ap (λ p → ! p ∙ idp) (app=-β H₁ z)) ◃∙ ap (λ p → ! p ∙ idp) (fst (∼⊙homog= (f z) {fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂} - {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎} - {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎} + {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ H₁ₚ)} + {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ H₂ₚ)} (ap λ= (λ= K))) z) ◃∙ - ap (λ p → ! p ∙ idp) (app=-β H₂ z) ◃∎) ◃∙ H₂ₚ + ap (λ p → ! p ∙ idp) (app=-β H₂ z) ◃∎) ◃∙ H₂ₚ ◃∎ =ₛ⟨ pre-rotate-in-↯-assoc (snd (∼⊙homog= x {fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂} - {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎} - {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎} + {H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ H₁ₚ)} + {H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ H₂ₚ)} (ap λ= (λ= K)))) ⟩ - H₁ₚ ∎ₛ + H₁ₚ ◃∎ ∎ₛ -- All loop spaces are coherently homogeneous. @@ -183,12 +183,13 @@ module _ {i} {X : Type i} {x : X} where snd (auto loop-homog q) = post∙-is-equiv (! p ∙ q) homog-idf loop-homog = ⊙λ= (comp-to-⊙ ((λ x₁ → ap (λ c → x₁ ∙ c) (!-inv-l p) ∙ ∙-unit-r x₁) , - !-inv-l-r-unit-assoc p ◃∎)) + !-inv-l-r-unit-assoc p)) ∼⊙Ωhomog∼ : ∀ {j} {Z : Ptd j} {p : x == x} {f g : Z ⊙→ ⊙[ x == x , p ]} {H₁ H₂ : fst f ∼ fst g} - {H₁ₚ : ! (H₁ (pt Z)) ∙ snd f =-= snd g} - {H₂ₚ : ! (H₂ (pt Z)) ∙ snd f =-= snd g} + {H₁ₚ : ! (H₁ (pt Z)) ∙ snd f == snd g} + {H₂ₚ : ! (H₂ (pt Z)) ∙ snd f == snd g} → H₁ ∼ H₂ → (H₁ , H₁ₚ) ⊙→∼ (H₂ , H₂ₚ) ∼⊙Ωhomog∼ {Z = Z} {p} {f} K = ∼⊙homog∼ (loop-homog {p = fst f (pt Z)}) p K + diff --git a/HoTT-Agda/core/lib/types/Pointed.agda b/HoTT-Agda/core/lib/types/Pointed.agda index ee58a71..582ef22 100644 --- a/HoTT-Agda/core/lib/types/Pointed.agda +++ b/HoTT-Agda/core/lib/types/Pointed.agda @@ -60,27 +60,27 @@ module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} where → ((h ⊙∘ g) ⊙∘ f) ⊙-comp (h ⊙∘ (g ⊙∘ f)) fst (⊙∘-assoc-comp (h , hpt) (g , gpt) (f , fpt)) = λ x → idp snd (⊙∘-assoc-comp (h , hpt) (g , gpt) (f , fpt)) = - ! (∙-assoc (ap (h ∘ g) fpt) (ap h gpt) hpt) ◃∙ - ap (λ p → p ∙ hpt) (ap (λ p → p ∙ ap h gpt) (ap-∘ h g fpt)) ◃∙ - ap (λ p → p ∙ hpt) (∙-ap h (ap g fpt) gpt) ◃∎ + ! (∙-assoc (ap (h ∘ g) fpt) (ap h gpt) hpt) ∙ + ap (λ p → p ∙ hpt) (ap (λ p → p ∙ ap h gpt) (ap-∘ h g fpt)) ∙ + ap (λ p → p ∙ hpt) (∙-ap h (ap g fpt) gpt) -- pre- and post-comp on (unfolded) homotopies of pointed maps ⊙∘-post : {f₁ f₂ : X ⊙→ Y} (g : Y ⊙→ Z) (H : f₁ ⊙-comp f₂) → g ⊙∘ f₁ ⊙-comp g ⊙∘ f₂ fst (⊙∘-post g H) = λ x → ap (fst g) (fst H x) snd (⊙∘-post {f₁} g H) = - ! (∙-assoc (! (ap (fst g) (fst H (pt X)))) (ap (fst g) (snd f₁)) (snd g)) ◃∙ - ap (λ p → p ∙ snd g) (!-ap-∙ (fst g) (fst H (pt X)) (snd f₁)) ◃∙ - ap (λ p → p ∙ snd g) (ap (ap (fst g)) (↯ (snd H))) ◃∎ + ! (∙-assoc (! (ap (fst g) (fst H (pt X)))) (ap (fst g) (snd f₁)) (snd g)) ∙ + ap (λ p → p ∙ snd g) (!-ap-∙ (fst g) (fst H (pt X)) (snd f₁)) ∙ + ap (λ p → p ∙ snd g) (ap (ap (fst g)) (snd H)) ⊙∘-pre : {f₁ f₂ : X ⊙→ Y} (g : Z ⊙→ X) (H : f₁ ⊙-comp f₂) → f₁ ⊙∘ g ⊙-comp f₂ ⊙∘ g fst (⊙∘-pre g H) = λ x → fst H (fst g x) snd (⊙∘-pre {f₁} {f₂} g H) = - ! (∙-assoc (! (fst H (fst g (pt Z)))) (ap (fst f₁) (snd g)) (snd f₁)) ◃∙ - ap (λ p → p ∙ snd f₁) (hmtpy-nat-!-sq (fst H) (snd g)) ◃∙ - ∙-assoc (ap (fst f₂) (snd g)) (! (fst H (pt X))) (snd f₁) ◃∙ - ap (λ p → ap (fst f₂) (snd g) ∙ p) (↯ (snd H)) ◃∎ - + ! (∙-assoc (! (fst H (fst g (pt Z)))) (ap (fst f₁) (snd g)) (snd f₁)) ∙ + ap (λ p → p ∙ snd f₁) (hmtpy-nat-!-sq (fst H) (snd g)) ∙ + ∙-assoc (ap (fst f₂) (snd g)) (! (fst H (pt X))) (snd f₁) ∙ + ap (λ p → ap (fst f₂) (snd g) ∙ p) (snd H) + -- concatenation of homotopies of pointed maps module _ {i j} {X : Ptd i} {Y : Ptd j} {f₁ f₂ f₃ : X ⊙→ Y} where @@ -89,9 +89,9 @@ module _ {i j} {X : Ptd i} {Y : Ptd j} {f₁ f₂ f₃ : X ⊙→ Y} where _∙⊙∼_ : f₁ ⊙-comp f₂ → f₂ ⊙-comp f₃ → f₁ ⊙-comp f₃ fst (H₁ ∙⊙∼ H₂) = λ x → fst H₁ x ∙ fst H₂ x snd (H₁ ∙⊙∼ H₂) = - ap (λ p → ! (p ∙ fst H₂ (pt X)) ∙ snd f₁) (tri-exch (↯ (snd H₁))) ◃∙ - ap (λ p → ! ((snd f₁ ∙ ! (snd f₂)) ∙ p) ∙ snd f₁) (tri-exch (↯ (snd H₂))) ◃∙ - !3-∙3 (snd f₁) (snd f₂) (snd f₃) ◃∎ + ap (λ p → ! (p ∙ fst H₂ (pt X)) ∙ snd f₁) (tri-exch (snd H₁)) ∙ + ap (λ p → ! ((snd f₁ ∙ ! (snd f₂)) ∙ p) ∙ snd f₁) (tri-exch (snd H₂)) ∙ + !3-∙3 (snd f₁) (snd f₂) (snd f₃) -- inverse of homotopy of pointed maps @@ -100,16 +100,16 @@ module _ {i j} {X : Ptd i} {Y : Ptd j} where !-⊙∼ : {f₁ f₂ : X ⊙→ Y} (H : f₁ ⊙-comp f₂) → f₂ ⊙-comp f₁ fst (!-⊙∼ (H₀ , H₁)) x = ! (H₀ x) snd (!-⊙∼ {f₁} {f₂} (H₀ , H₁)) = - ap (λ p → p ∙ snd f₂) (!-! (H₀ (pt (X)))) ◃∙ - ap (λ p → H₀ (pt X) ∙ p) (↯ (seq-! H₁)) ◃∙ - ! (∙-assoc (H₀ (pt X)) (! (H₀ (pt X))) (snd f₁)) ◃∙ - ap (λ p → p ∙ snd f₁) (!-inv-r (H₀ (pt X))) ◃∎ + ap (λ p → p ∙ snd f₂) (!-! (H₀ (pt (X)))) ∙ + ap (λ p → H₀ (pt X) ∙ p) (! H₁) ∙ + ! (∙-assoc (H₀ (pt X)) (! (H₀ (pt X))) (snd f₁)) ∙ + ap (λ p → p ∙ snd f₁) (!-inv-r (H₀ (pt X))) -- identity homotopy of pointed maps ⊙∼-id : (f : X ⊙→ Y) → f ⊙-comp f fst (⊙∼-id (f , fₚ)) x = idp - snd (⊙∼-id (f , fₚ)) = idp ◃∎ + snd (⊙∼-id (f , fₚ)) = idp -- homotopies of homotopies of pointed maps @@ -119,7 +119,7 @@ module _ {i j} {X : Ptd i} {Y : Ptd j} where _⊙→∼_ : {f g : X ⊙→ Y} (H₁ H₂ : f ⊙-comp g) → Type (lmax i j) _⊙→∼_ {f = f} H₁ H₂ = Σ (fst H₁ ∼ fst H₂) - (λ K → ap (λ p → ! p ∙ snd f) (K (pt X)) ◃∙ snd H₂ =ₛ snd H₁) + (λ K → ap (λ p → ! p ∙ snd f) (K (pt X)) ◃∙ snd H₂ ◃∎ =ₛ snd H₁ ◃∎) -- pointed sections diff --git a/HoTT-Agda/core/lib/types/Suspension.agda b/HoTT-Agda/core/lib/types/Suspension.agda index 55d33d3..3175466 100644 --- a/HoTT-Agda/core/lib/types/Suspension.agda +++ b/HoTT-Agda/core/lib/types/Suspension.agda @@ -69,29 +69,29 @@ susp-⊙span X = module _ {i j} {A : Type i} {B : Type j} (f g : Susp A → B) (n : f north == g north) (s : f south == g south) - (c : (a : A) → ap f (merid a) =-= n ∙ ap g (merid a) ∙' ! s) where + (c : (a : A) → ap f (merid a) == n ∙ ap g (merid a) ∙' ! s) where SuspMapEq : f ∼ g - SuspMapEq = Susp-elim n s λ a → from-hmpty-nat f g (merid a) (↯ (c a)) + SuspMapEq = Susp-elim n s λ a → from-hmpty-nat f g (merid a) (c a) - SuspMapEq-β : (a : A) → hmpty-nat-∙'-r SuspMapEq (merid a) == ↯ (c a) + SuspMapEq-β : (a : A) → hmpty-nat-∙'-r SuspMapEq (merid a) == c a SuspMapEq-β a = - apd-to-hnat f g SuspMapEq (merid a) (↯ (c a)) - (SuspElim.merid-β n s (λ z → from-hmpty-nat f g (merid z) (↯ (c z))) a) + apd-to-hnat f g SuspMapEq (merid a) (c a) + (SuspElim.merid-β n s (λ z → from-hmpty-nat f g (merid z) (c z)) a) SuspMapEq-!-β : (a : A) → hmpty-nat-∙'-r SuspMapEq (! (merid a)) == - ap-! f (merid a) ∙ ap ! (↯ (c a)) ∙ !-∙-ap-∙'-! g n (merid a) s + ap-! f (merid a) ∙ ap ! (c a) ∙ !-∙-ap-∙'-! g n (merid a) s SuspMapEq-!-β a = apd-to-hnat-! f g SuspMapEq (merid a) (SuspMapEq-β a) SuspMapEq-β-∙ : (a b : A) → hmpty-nat-∙'-r SuspMapEq (merid a ∙ ! (merid b)) == ap-∙ f (merid a) (! (merid b)) ∙ - ap (λ p → p ∙ ap f (! (merid b))) (↯ (c a)) ∙ + ap (λ p → p ∙ ap f (! (merid b))) (c a) ∙ ap (_∙_ (SuspMapEq north ∙ ap g (merid a) ∙' ! (SuspMapEq south))) - (ap-! f (merid b) ∙ ap ! (↯ (c b)) ∙ !-∙-ap-∙'-! g n (merid b) s) ∙ + (ap-! f (merid b) ∙ ap ! (c b) ∙ !-∙-ap-∙'-! g n (merid b) s) ∙ assoc-tri-!-mid (SuspMapEq north) (ap g (merid a)) (SuspMapEq south) (ap g (! (merid b))) (! (SuspMapEq north)) ∙ ap (λ p → SuspMapEq north ∙ p ∙' ! (SuspMapEq north)) @@ -104,9 +104,9 @@ module _ {i j} {A : Type i} {B : Type j} (f g : Susp A → B) == ap-∘-long k g f SuspMapEq (merid a ∙ ! (merid b)) ∙ ! (ap (λ q → ap k (! (SuspMapEq north)) ∙ ap k q ∙' ! (ap k (! (SuspMapEq north)))) - (ap-∙ f (merid a) (! (merid b)) ∙ ap (λ p → p ∙ ap f (! (merid b))) (↯ (c a)) ∙ + (ap-∙ f (merid a) (! (merid b)) ∙ ap (λ p → p ∙ ap f (! (merid b))) (c a) ∙ ap (_∙_ (SuspMapEq north ∙ ap g (merid a) ∙' ! (SuspMapEq south))) - (ap-! f (merid b) ∙ ap ! (↯ (c b)) ∙ !-∙-ap-∙'-! g n (merid b) s) ∙ + (ap-! f (merid b) ∙ ap ! (c b) ∙ !-∙-ap-∙'-! g n (merid b) s) ∙ assoc-tri-!-mid (SuspMapEq north) (ap g (merid a)) (SuspMapEq south) (ap g (! (merid b))) (! (SuspMapEq north)) ∙ ap (λ p → SuspMapEq north ∙ p ∙' ! (SuspMapEq north)) @@ -158,7 +158,7 @@ module _ {i j k} {X : Type i} {Y : Type j} {Z : Type k} (g : Y → Z) (f : X → Susp-fmap-∘-∼ = SuspMapEq (Susp-fmap (g ∘ f)) (Susp-fmap g ∘ Susp-fmap f) idp idp - (Susp-fmap-∘ g f) + (λ a → ↯ (Susp-fmap-∘ g f a)) module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} (g : Y ⊙→ Z) (f : X ⊙→ Y) where diff --git a/HoTT-Agda/core/lib/types/Truncation.agda b/HoTT-Agda/core/lib/types/Truncation.agda new file mode 100644 index 0000000..0256a0c --- /dev/null +++ b/HoTT-Agda/core/lib/types/Truncation.agda @@ -0,0 +1,226 @@ +{-# OPTIONS --without-K --rewriting --overlapping-instances #-} + +open import lib.Basics +open import lib.types.TLevel +open import lib.types.Pi +open import lib.types.Sigma +open import lib.NType2 + +module lib.types.Truncation where + +module _ {i} where + + postulate -- HIT + Trunc : (n : ℕ₋₂) (A : Type i) → Type i + [_] : {n : ℕ₋₂} {A : Type i} → A → Trunc n A + instance Trunc-level : {n : ℕ₋₂} {A : Type i} → has-level n (Trunc n A) + + module TruncElim {n : ℕ₋₂} {A : Type i} {j} {P : Trunc n A → Type j} + {{p : {x : Trunc n A} → has-level n (P x)}} (d : (a : A) → P [ a ]) where + + postulate -- HIT + f : Π (Trunc n A) P + [_]-β : ∀ a → f [ a ] ↦ d a + {-# REWRITE [_]-β #-} + +open TruncElim public renaming (f to Trunc-elim) + +module TruncRec {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} {{p : has-level n B}} + (d : A → B) where + + private + module M = TruncElim {{λ {x} → p}} d + + f : Trunc n A → B + f = M.f + +open TruncRec public renaming (f to Trunc-rec) + +module TruncRecType {i j} {n : ℕ₋₂} {A : Type i} (d : A → n -Type j) where + + open TruncRec {{n -Type-level j}} d public + + flattening-Trunc : Σ (Trunc (S n) A) (fst ∘ f) ≃ Trunc (S n) (Σ A (fst ∘ d)) + flattening-Trunc = equiv to from to-from from-to where + + to-aux : (x : Trunc (S n) A) → (fst (f x) → Trunc (S n) (Σ A (fst ∘ d))) + to-aux = Trunc-elim (λ a b → [ (a , b) ]) + + to : Σ (Trunc (S n) A) (fst ∘ f) → Trunc (S n) (Σ A (fst ∘ d)) + to (x , y) = to-aux x y + + from-aux : Σ A (fst ∘ d) → Σ (Trunc (S n) A) (fst ∘ f) + from-aux (a , b) = ([ a ] , b) + + from : Trunc (S n) (Σ A (fst ∘ d)) → Σ (Trunc (S n) A) (fst ∘ f) + from = Trunc-rec {{Σ-level ⟨⟩ (λ x → raise-level _ (snd (f x)))}} + from-aux + + to-from : (x : Trunc (S n) (Σ A (fst ∘ d))) → to (from x) == x + to-from = Trunc-elim (λ _ → idp) + + from-to-aux : (a : Trunc (S n) A) (b : fst (f a)) → from (to-aux a b) == (a , b) + from-to-aux = Trunc-elim {{Π-level (λ _ → =-preserves-level (Σ-level ⟨⟩ (λ x → raise-level _ (snd (f x)))))}} + (λ a b → idp) + + from-to : (x : Σ (Trunc (S n) A) (fst ∘ f)) → from (to x) == x + from-to (a , b) = from-to-aux a b + + +⊙Trunc : ∀ {i} → ℕ₋₂ → Ptd i → Ptd i +⊙Trunc n ⊙[ A , a ] = ⊙[ Trunc n A , [ a ] ] + +module _ {i} {A : Type i} where + + [_]₀ : A → Trunc 0 A + [_]₀ = [_] {n = 0} + + [_]₁ : A → Trunc 1 A + [_]₁ = [_] {n = 1} + + [_]₂ : A → Trunc 2 A + [_]₂ = [_] {n = 2} + +module _ {i} {n : ℕ₋₂} {A : Type i} where + + private + Trunc= : (a b : Trunc (S n) A) → n -Type i + Trunc= = Trunc-elim (λ a → Trunc-elim ((λ b → (Trunc n (a == b) , Trunc-level)))) + + {- t is for truncated -} + _=ₜ_ : (a b : Trunc (S n) A) → Type i + _=ₜ_ a b = fst (Trunc= a b) + + =ₜ-level : (a b : Trunc (S n) A) → has-level n (a =ₜ b) + =ₜ-level a b = snd (Trunc= a b) + + =ₜ-refl : (a : Trunc (S n) A) → a =ₜ a + =ₜ-refl = Trunc-elim {{λ {x} → raise-level _ (=ₜ-level x x)}} + (λ a → [ idp ]) + + =ₜ-equiv : (a b : Trunc (S n) A) → (a == b) ≃ (a =ₜ b) + =ₜ-equiv a b = to a b , to-is-equiv a b where + + to : (a b : Trunc (S n) A) → (a == b → a =ₜ b) + to a .a idp = =ₜ-refl a + + from-aux : (a b : A) → a == b → [ a ] == [ b ] :> Trunc (S n) A + from-aux _ _ = ap [_] + + from : (a b : Trunc (S n) A) → a =ₜ b → a == b + from = Trunc-elim (λ a → Trunc-elim (λ b → Trunc-rec (from-aux a b))) + + to-from-aux : (a b : A) → (p : a == b) → to _ _ (from-aux a b p) == [ p ] + to-from-aux a .a idp = idp + + to-from : (a b : Trunc (S n) A) (x : a =ₜ b) → to a b (from a b x) == x + to-from = Trunc-elim {{λ {x} → Π-level (λ y → Π-level (λ _ → =-preserves-level (raise-level _ (=ₜ-level x y))))}} + (λ a → Trunc-elim {{λ {x} → Π-level (λ _ → =-preserves-level (raise-level _ (=ₜ-level [ a ] x)))}} + (λ b → Trunc-elim + (to-from-aux a b))) + + from-to-aux : (a : Trunc (S n) A) → from a a (=ₜ-refl a) == idp + from-to-aux = Trunc-elim (λ _ → idp) + + from-to : (a b : Trunc (S n) A) (p : a == b) → from a b (to a b p) == p + from-to a .a idp = from-to-aux a + + adj : (ta tb : Trunc (S n) A) (p : ta == tb) + → ap (to ta tb) (from-to ta tb p) == to-from ta tb (to ta tb p) + adj ta .ta idp = + Trunc-elim {P = λ ta → ap (to ta ta) (from-to ta ta idp) == to-from ta ta (to ta ta idp)} + {{λ {x} → =-preserves-level $ =-preserves-level $ raise-level _ $ =ₜ-level x x}} + (λ _ → idp) + ta + + to-is-equiv : ∀ a b → is-equiv (to a b) + to-is-equiv a b = + record + { g = from a b + ; f-g = to-from a b + ; g-f = from-to a b + ; adj = adj a b + } + + =ₜ-path : (a b : Trunc (S n) A) → (a == b) == (a =ₜ b) + =ₜ-path a b = ua (=ₜ-equiv a b) + +{- Universal property -} + +abstract + Trunc-rec-is-equiv : ∀ {i j} (n : ℕ₋₂) (A : Type i) (B : Type j) + {{p : has-level n B}} → is-equiv (Trunc-rec {{p}} :> ((A → B) → (Trunc n A → B))) + Trunc-rec-is-equiv n A B {{p}} = is-eq _ (λ f → f ∘ [_]) + (λ f → λ= (Trunc-elim (λ a → idp))) (λ f → idp) + + +Trunc-preserves-level : ∀ {i} {A : Type i} {n : ℕ₋₂} (m : ℕ₋₂) + → has-level n A → has-level n (Trunc m A) +Trunc-preserves-level {n = ⟨-2⟩} _ p = has-level-in + ([ contr-center p ] , Trunc-elim (λ a → ap [_] (contr-path p a))) +Trunc-preserves-level ⟨-2⟩ _ = contr-has-level Trunc-level +Trunc-preserves-level {n = (S n)} (S m) c = has-level-in (λ t₁ t₂ → + Trunc-elim + {{λ {s₁} → prop-has-level-S {A = has-level n (s₁ == t₂)} has-level-is-prop}} + (λ a₁ → Trunc-elim + {{λ {s₂} → prop-has-level-S {A = has-level n ([ a₁ ] == s₂)} has-level-is-prop}} + (λ a₂ → equiv-preserves-level + ((=ₜ-equiv [ a₁ ] [ a₂ ])⁻¹) + {{Trunc-preserves-level {n = n} m (has-level-apply c a₁ a₂)}}) + t₂) + t₁) + +{- an n-type is equivalent to its n-truncation -} +unTrunc-equiv : ∀ {i} {n : ℕ₋₂} (A : Type i) + {{_ : has-level n A}} → Trunc n A ≃ A +unTrunc-equiv A {{pA}} = equiv f [_] (λ _ → idp) g-f where + f = Trunc-rec {{pA}} (idf _) + g-f = Trunc-elim {{=-preserves-level Trunc-level}} (λ _ → idp) + +⊙unTrunc-equiv : ∀ {i} {n : ℕ₋₂} (X : Ptd i) + {{_ : has-level n (de⊙ X)}} → ⊙Trunc n X ⊙≃ X +⊙unTrunc-equiv {n = n} X = ≃-to-⊙≃ (unTrunc-equiv (de⊙ X)) idp + +-- Equivalence associated to the universal property +Trunc-extend-equiv : ∀ {i j} (n : ℕ₋₂) (A : Type i) (B : Type j) + {{p : has-level n B}} → (A → B) ≃ (Trunc n A → B) +Trunc-extend-equiv n A B = (Trunc-rec , Trunc-rec-is-equiv n A B) + +{- Various functorial properties -} + +Trunc-fmap : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} → ((A → B) → (Trunc n A → Trunc n B)) +Trunc-fmap f = Trunc-rec ([_] ∘ f) + +⊙Trunc-fmap : ∀ {i j} {n : ℕ₋₂} {X : Ptd i} {Y : Ptd j} → ((X ⊙→ Y) → (⊙Trunc n X ⊙→ ⊙Trunc n Y)) +⊙Trunc-fmap F = Trunc-fmap (fst F) , ap [_] (snd F) + +Trunc-fmap2 : ∀ {i j k} {n : ℕ₋₂} {A : Type i} {B : Type j} {C : Type k} + → ((A → B → C) → (Trunc n A → Trunc n B → Trunc n C)) +Trunc-fmap2 f = Trunc-rec (λ a → Trunc-fmap (f a)) + +Trunc-fpmap : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} {f g : A → B} + → f ∼ g → Trunc-fmap {n = n} f ∼ Trunc-fmap g +Trunc-fpmap h = Trunc-elim (ap [_] ∘ h) + +Trunc-fmap-idf : ∀ {i} {n : ℕ₋₂} {A : Type i} + → ∀ x → Trunc-fmap {n = n} (idf A) x == x +Trunc-fmap-idf = + Trunc-elim (λ _ → idp) + +Trunc-fmap-∘ : ∀ {i j k} {n : ℕ₋₂} {A : Type i} {B : Type j} {C : Type k} + → (g : B → C) → (f : A → B) + → ∀ x → Trunc-fmap {n = n} g (Trunc-fmap f x) == Trunc-fmap (g ∘ f) x +Trunc-fmap-∘ g f = + Trunc-elim (λ _ → idp) + +Trunc-csmap : ∀ {i₀ i₁ j₀ j₁} {n : ℕ₋₂} + {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁} + {f : A₀ → B₀} {g : A₁ → B₁} {hA : A₀ → A₁} {hB : B₀ → B₁} + → CommSquare f g hA hB + → CommSquare (Trunc-fmap {n = n} f) (Trunc-fmap g) (Trunc-fmap hA) (Trunc-fmap hB) +Trunc-csmap (comm-sqr cs) = comm-sqr $ Trunc-elim (ap [_] ∘ cs) + +transport-Trunc : ∀ {i j} {A : Type i} {n : ℕ₋₂} (P : A → Type j) + {x y : A} (p : x == y) (b : P x) + → transport (Trunc n ∘ P) p [ b ] == [ transport P p b ] +transport-Trunc _ idp _ = idp diff --git a/HoTT-Agda/theorems/homotopy/SuspAdjointLoop.agda b/HoTT-Agda/theorems/homotopy/SuspAdjointLoop.agda index 0df4482..9092a17 100644 --- a/HoTT-Agda/theorems/homotopy/SuspAdjointLoop.agda +++ b/HoTT-Agda/theorems/homotopy/SuspAdjointLoop.agda @@ -53,7 +53,7 @@ module _ {i j} (X : Ptd i) (U : Ptd j) where (! (∙-unit-r (! (H₀ x)))) ∙ idp) ∙ ! (Ω-fmap-β (g , ! (H₀ x) ∙ idp) (v ∙ ! v))) ∙ ap (ap f) (!-inv-r v) ∙ idp - =-= + == ap (fst (⊙Ω-fmap (g , ! (H₀ x) ∙ idp))) (!-inv-r v) ∙ snd (⊙Ω-fmap (g , ! (H₀ x) ∙ idp)) ap-comp-into-coher-aux {g = g} H₀ idp = lemma (H₀ (right unit)) @@ -67,9 +67,9 @@ module _ {i j} (X : Ptd i) (U : Ptd j) where ap (λ p → ! (! u ∙ idp) ∙ idp ∙' p) (! (∙-unit-r (! u))) ∙ idp) ∙ ! (Ω-fmap-β (g , ! u ∙ idp) idp)) ∙ idp - =-= + == snd (⊙Ω-fmap (g , ! u ∙ idp)) - lemma idp = idp ◃∎ + lemma idp = idp ap-comp-into-coher : {f g : Susp (de⊙ X) → de⊙ U} (H₀ : f ∼ g) {gₚ : g (left unit) == f (left unit)} (H₁ : ! (H₀ (left unit)) ∙ idp == gₚ) @@ -82,7 +82,7 @@ module _ {i j} (X : Ptd i) (U : Ptd j) where ∙-∙'-= (ap g (glue (pt X) ∙ ! (glue (pt X)))) H₁) ∙ ! (Ω-fmap-β (g , gₚ) (glue (pt X) ∙ ! (glue (pt X))))) ∙ ap (ap f) (!-inv-r (glue (pt X))) ∙ idp - =-= + == ap (Ω-fmap (g , gₚ)) (!-inv-r (glue (pt X))) ∙ snd (⊙Ω-fmap (g , gₚ)) ap-comp-into-coher H₀ idp = ap-comp-into-coher-aux H₀ (glue (pt X)) @@ -93,9 +93,9 @@ module _ {i j} (X : Ptd i) (U : Ptd j) where (! (!-! (fst H (left unit))) ∙ ! (!-∙ (! (fst H (left unit))) idp)) ∙ ap (λ p → (! (! (fst H (left unit)) ∙ idp)) ∙ ap (fst f₂) (glue x ∙ ! (glue (pt X))) ∙' p) (! (∙-unit-r (! (fst H (left unit))))) ∙ - ∙-∙'-= (ap (fst f₂) (glue x ∙ ! (glue (pt X)))) (↯ (snd H))) ∙ + ∙-∙'-= (ap (fst f₂) (glue x ∙ ! (glue (pt X)))) (snd H)) ∙ ! (Ω-fmap-β f₂ (glue x ∙ ! (glue (pt X)))) - snd (ap-comp-into {f₁ = (f , idp)} {f₂} H) = ap-comp-into-coher (fst H) (↯ (snd H)) + snd (ap-comp-into {f₁ = (f , idp)} {f₂} H) = ap-comp-into-coher (fst H) (snd H) {- This definition of ap agrees with the standard ap on the id homotopy, @@ -115,7 +115,7 @@ module _ {i j} (X : Ptd i) (U : Ptd j) where ∙-unit-r (hmpty-nat-∙'-r (λ x₁ → idp) (v ∙ ! v)) ∙ hmpty-nat-∙'-r-idp (v ∙ ! v)) ∙ idp == - ↯ (ap-comp-into-coher-aux (λ x → idp) v) + ap-comp-into-coher-aux (λ x → idp) v lemma idp = idp {- @@ -183,12 +183,12 @@ module _ {i i' j} {X : Ptd i} {Y : Ptd i'} {U : Ptd j} where ap (ap r₀) (ap-! (Susp-fmap h₀) (glue (pt X)))))) (! (ap (λ p → ap r₀ p ∙ ap (r₀ ∘ Susp-fmap h₀) (! (glue (pt X)))) (SuspFmap.merid-β h₀ (pt X)))) (! (ap (λ p → p ∙ ap (r₀ ∘ Susp-fmap h₀) (! (glue (pt X)))) (ap-∘ r₀ (Susp-fmap h₀) (glue (pt X))))) - (! (ap-∙ (r₀ ∘ Susp-fmap h₀) (glue (pt X)) (! (glue (pt X)))))) ◃∙ + (! (ap-∙ (r₀ ∘ Susp-fmap h₀) (glue (pt X)) (! (glue (pt X)))))) ∙ ap (λ p → ! (ap-∙ r₀ (glue (h₀ (pt X))) (! (glue (h₀ (pt X)))) ∙ p ∙ ! (ap (λ p → p ∙ ap (r₀ ∘ Susp-fmap h₀) (! (glue (pt X)))) (ap-∘ r₀ (Susp-fmap h₀) (glue (pt X)))) ∙ ! (ap-∙ (r₀ ∘ Susp-fmap h₀) (glue (pt X)) (! (glue (pt X))))) ∙ - ap (ap r₀) (!-inv-r (glue (h₀ (pt X)))) ∙ idp) (nat-dom-aux-l r₀ h₀) ◃∙ - nat-dom-aux-r r₀ h₀ ((glue (h₀ (pt X)))) ◃∎ + ap (ap r₀) (!-inv-r (glue (h₀ (pt X)))) ∙ idp) (nat-dom-aux-l r₀ h₀) ∙ + nat-dom-aux-r r₀ h₀ ((glue (h₀ (pt X)))) {- the nat-dom proof makes Susp a 2-coherent left adjoint to Loop -} @@ -272,19 +272,19 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W : β-red1-aux2 : {w : Susp (de⊙ W)} (ω₆ : left unit == w) {𝕗 : ap f₁ (! (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) - (Susp-fmap f₂ ∘ Susp-fmap f₃) idp idp (Susp-fmap-∘ f₂ f₃) w)) ∙ + (Susp-fmap f₂ ∘ Susp-fmap f₃) idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x)) w)) ∙ ap f₁ (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃) - idp idp (Susp-fmap-∘ f₂ f₃) w ∙ + idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x)) w ∙ ap (Susp-fmap f₂ ∘ Susp-fmap f₃) (! ω₆)) == ap f₁ (ap (Susp-fmap f₂ ∘ Susp-fmap f₃) (! ω₆))} (𝕣 : 𝕗 == ap-!-∙-ap f₁ (Susp-fmap f₂ ∘ Susp-fmap f₃) (! ω₆) (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃) - idp idp (Susp-fmap-∘ f₂ f₃) w)) → + idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x)) w)) → (! (ap (λ q → q) (ap-∘ (f₁ ∘ Susp-fmap f₂) (Susp-fmap f₃) (! ω₆) ∙ ap (ap (f₁ ∘ Susp-fmap f₂)) (ap-! (Susp-fmap f₃) ω₆))) ∙ idp) ∙ ap-∘-long f₁ (Susp-fmap f₂ ∘ Susp-fmap f₃) (Susp-fmap (f₂ ∘ f₃)) (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃) - idp idp (Susp-fmap-∘ f₂ f₃)) (! ω₆) ∙ + idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x))) (! ω₆) ∙ 𝕗 ∙ ! (ap (ap f₁) (ap (λ q → q) (ap ! (! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) ω₆)) ∙ !-ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₆) ∙ idp)) @@ -304,7 +304,7 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W : ! (ap-∙ (f₁ ∘ Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃ (! ω₆))) ∙ ap-∘-long f₁ (Susp-fmap f₂ ∘ Susp-fmap f₃) (Susp-fmap (f₂ ∘ f₃)) (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃) - idp idp (Susp-fmap-∘ f₂ f₃)) (ω₃ ∙ ! ω₆) ∙ + idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x))) (ω₃ ∙ ! ω₆) ∙ ! (ap (ap f₁) (ap (_∙_ (ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃)) (ap ! (! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) ω₆)) ∙ !-ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₆) ∙ @@ -336,7 +336,7 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W : ! (ap-∙ (f₁ ∘ Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃ (! ω₆))) ∙ ap-∘-long f₁ (Susp-fmap f₂ ∘ Susp-fmap f₃) (Susp-fmap (f₂ ∘ f₃)) (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃) - idp idp (Susp-fmap-∘ f₂ f₃)) (ω₃ ∙ ! ω₆) ∙ + idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x))) (ω₃ ∙ ! ω₆) ∙ ! (ap (ap f₁) (ap (λ p → ap (Susp-fmap f₂ ∘ Susp-fmap f₃) ω₃ ∙ p) (ap ! (! (ap (ap (Susp-fmap f₂)) ω₅) ∙ ! (ap-∘ (Susp-fmap f₂) (Susp-fmap f₃) ω₆)) ∙ @@ -517,7 +517,7 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W : == ((ap-∘-long f₁ (Susp-fmap f₂ ∘ Susp-fmap f₃) (Susp-fmap (f₂ ∘ f₃)) (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃) - idp idp (Susp-fmap-∘ f₂ f₃)) (merid x ∙ ! (merid (pt W))) ∙ + idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x))) (merid x ∙ ! (merid (pt W))) ∙ ! (ap (ap f₁) ( ap-∙ (Susp-fmap (f₂ ∘ f₃)) (merid x) (! (merid (pt W))) ∙ ap (λ p → p ∙ ap (Susp-fmap (f₂ ∘ f₃)) (! (merid (pt W)))) @@ -537,7 +537,7 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W : (merid x ∙ ! (merid (pt W)))))) ∙ idp) ∙ idp Susp-fmap-∘-sq-rw = ap (λ p → (p ∙ idp) ∙ idp) (SuspMapEq-β-∙-ap! (Susp-fmap (f₂ ∘ f₃)) - (Susp-fmap f₂ ∘ Susp-fmap f₃) idp idp (Susp-fmap-∘ f₂ f₃) f₁ x (pt W)) + (Susp-fmap f₂ ∘ Susp-fmap f₃) idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x)) f₁ x (pt W)) -- proof of 2-coherence @@ -546,7 +546,7 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W : (λ p → ap (Susp-fmap f₂ ∘ Susp-fmap f₃) (merid x) ∙ p) ! (ap-∘-long f₁ (Susp-fmap f₂ ∘ Susp-fmap f₃) (Susp-fmap (f₂ ∘ f₃)) (SuspMapEq (Susp-fmap (f₂ ∘ f₃)) (Susp-fmap f₂ ∘ Susp-fmap f₃) - idp idp (Susp-fmap-∘ f₂ f₃)) (merid x ∙ ! (merid (pt W)))) + idp idp (λ x → ↯ (Susp-fmap-∘ f₂ f₃ x))) (merid x ∙ ! (merid (pt W)))) (ap-∙ (Susp-fmap (f₂ ∘ f₃)) (merid x) (! (merid (pt W)))) (SuspFmap.merid-β (f₂ ∘ f₃) x) (! (SuspFmap.merid-β f₂ (f₃ x))) @@ -634,7 +634,7 @@ module _ {i₁ i₂ i₃ i₄} {X : Ptd i₁} {Y : Ptd i₂} {Z : Ptd i₃} {W : ⊙∘-pre h₃ (nat-dom h₂ h₁) ∙⊙∼ nat-dom h₃ (h₁ ⊙∘ ⊙Susp-fmap h₂) ∙⊙∼ ap-comp-into W Y (⊙∘-assoc-comp h₁ (⊙Susp-fmap h₂) (⊙Susp-fmap h₃) ∙⊙∼ - ⊙∘-post h₁ (!-⊙∼ (Susp-fmap-∘-∼ (fst h₂) (fst h₃) , idp ◃∎))) ∙⊙∼ + ⊙∘-post h₁ (!-⊙∼ (Susp-fmap-∘-∼ (fst h₂) (fst h₃) , idp))) ∙⊙∼ !-⊙∼ (nat-dom (h₂ ⊙∘ h₃) h₁) ⊙→∼ ⊙∼-id ((into X Y h₁) ⊙∘ h₂ ⊙∘ h₃) diff --git a/Pullback-stability/README.md b/Pullback-stability/README.md index 8276905..b0ad211 100644 --- a/Pullback-stability/README.md +++ b/Pullback-stability/README.md @@ -9,7 +9,7 @@ Theorem 16 of our preprint). ## Manual Type-Checking -1. Install Agda 2.6.3. +1. Install Agda 2.6.4.3. 2. Install the stripped, modified HoTT-Agda library under `../HoTT-Agda`. 3. Install the library under `../Colimit-code`. 3. Type check the file `Stability.agda`. diff --git a/README.md b/README.md index eda40b0..41c83be 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ ## Overview This Agda code accompanies our paper [Coslice Colimits in Homotopy Type Theory](https://phart3.github.io/colimits-paper.pdf). - (The link points to the preprint.) It has been checked with Agda 2.6.3. + (The link points to the preprint.) It has been checked with Agda 2.6.4.3. ## Organization