From 1f51e2cb91a4a293a63215214549e38e4260e3cb Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Fri, 8 Dec 2023 22:16:05 +0100 Subject: [PATCH] Homotopies between maps out of general sequential colimits --- .../sequential-colimits.lagda.md | 80 ++++++++++++++----- 1 file changed, 61 insertions(+), 19 deletions(-) diff --git a/src/synthetic-homotopy-theory/sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/sequential-colimits.lagda.md index 2be2ea3120..5e93a464f7 100644 --- a/src/synthetic-homotopy-theory/sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/sequential-colimits.lagda.md @@ -47,6 +47,58 @@ In other words, the sequential colimit universally completes the diagram We often abuse notation and write `A∞` for just the codomain of the universal cocone. You may also see the colimit written as `colimₙ Aₙ`. +## Definitions + +### Homotopies between maps out of sequential colimits + +```agda +module _ + { l1 l2 l3 : Level} {A : sequential-diagram l1} {X : UU l2} + ( c : cocone-sequential-diagram A X) + where + + htpy-out-of-sequential-colimit : {Y : UU l3} (f g : X → Y) → UU (l1 ⊔ l3) + htpy-out-of-sequential-colimit f g = + htpy-cocone-sequential-diagram + ( cocone-map-sequential-diagram c f) + ( cocone-map-sequential-diagram c g) + + equiv-htpy-htpy-out-of-sequential-colimit : + universal-property-sequential-colimit c → + {Y : UU l3} (f g : X → Y) → + htpy-out-of-sequential-colimit f g ≃ (f ~ g) + equiv-htpy-htpy-out-of-sequential-colimit up-c f g = + ( inv-equiv + ( equiv-dependent-universal-property-sequential-colimit + ( dependent-universal-property-universal-property-sequential-colimit c + ( up-c)))) ∘e + ( equiv-tot + ( λ K → + equiv-Π-equiv-family + ( λ n → + equiv-Π-equiv-family + ( λ a → + compute-dependent-identification-eq-value-function f g + ( coherence-triangle-cocone-sequential-diagram c n a) + ( K n a) + ( K (succ-ℕ n) (map-sequential-diagram A n a)))))) +``` + +### Components of a homotopy between maps out of sequential colimits + +```agda +module _ + { l1 l2 l3 : Level} {A : sequential-diagram l1} {X : UU l2} + { c : cocone-sequential-diagram A X} + ( up-c : universal-property-sequential-colimit c) {Y : UU l3} {f g : X → Y} + ( H : htpy-out-of-sequential-colimit c f g) + where + + htpy-htpy-out-of-sequential-colimit : f ~ g + htpy-htpy-out-of-sequential-colimit = + map-equiv (equiv-htpy-htpy-out-of-sequential-colimit c up-c f g) H +``` + ## Properties ### All sequential diagrams admit a standard colimit @@ -201,28 +253,16 @@ module _ htpy-out-of-standard-sequential-colimit : UU (l1 ⊔ l2) htpy-out-of-standard-sequential-colimit = - htpy-cocone-sequential-diagram A - ( cocone-map-sequential-diagram A - ( cocone-standard-sequential-colimit A) - ( f)) - ( cocone-map-sequential-diagram A - ( cocone-standard-sequential-colimit A) - ( g)) + htpy-out-of-sequential-colimit (cocone-standard-sequential-colimit A) f g equiv-htpy-htpy-out-of-standard-sequential-colimit : htpy-out-of-standard-sequential-colimit ≃ (f ~ g) equiv-htpy-htpy-out-of-standard-sequential-colimit = - ( inv-equiv equiv-dup-standard-sequential-colimit) ∘e - ( equiv-tot - ( λ K → - equiv-Π-equiv-family - ( λ n → - equiv-Π-equiv-family - ( λ a → - compute-dependent-identification-eq-value-function f g - ( coherence-triangle-cocone-standard-sequential-colimit n a) - ( K n a) - ( K (succ-ℕ n) (map-sequential-diagram A n a)))))) + equiv-htpy-htpy-out-of-sequential-colimit + ( cocone-standard-sequential-colimit A) + ( up-standard-sequential-colimit) + ( f) + ( g) ``` We may then obtain a homotopy of maps from a homotopy of their induced cocones. @@ -236,7 +276,9 @@ module _ htpy-htpy-out-of-standard-sequential-colimit : f ~ g htpy-htpy-out-of-standard-sequential-colimit = - map-equiv (equiv-htpy-htpy-out-of-standard-sequential-colimit A f g) H + htpy-htpy-out-of-sequential-colimit + ( up-standard-sequential-colimit) + ( H) ``` ### A type satisfies `is-sequential-colimit` if and only if it has the (dependent) universal property of sequential colimits