diff --git a/Makefile b/Makefile index 1c7fca38cc..43ebf857d9 100644 --- a/Makefile +++ b/Makefile @@ -14,7 +14,9 @@ else AGDA_MIN_HEAP ?= 4G endif -AGDARTS := +RTS -H$(AGDA_MIN_HEAP) -M6G -RTS +# Temporarily raise maximum heap size; should compile with the previous 6G +# before merging +AGDARTS := +RTS -H$(AGDA_MIN_HEAP) -M14G -RTS AGDAFILES := $(shell find src -name temp -prune -o -type f \( -name "*.lagda.md" -not -name "everything.lagda.md" \) -print) CONTRIBUTORS_FILE := CONTRIBUTORS.toml diff --git a/src/foundation-core/families-of-equivalences.lagda.md b/src/foundation-core/families-of-equivalences.lagda.md index a3578dcaaa..713a875d28 100644 --- a/src/foundation-core/families-of-equivalences.lagda.md +++ b/src/foundation-core/families-of-equivalences.lagda.md @@ -84,6 +84,24 @@ module _ is-equiv-map-fam-equiv x = is-equiv-map-equiv (e x) ``` +### Inverses of families of equivalences + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {P : A → UU l2} {Q : A → UU l3} + (e : fam-equiv P Q) + where + + inv-fam-equiv : fam-equiv Q P + inv-fam-equiv a = inv-equiv (e a) + + map-inv-fam-equiv : (a : A) → Q a → P a + map-inv-fam-equiv = map-fam-equiv inv-fam-equiv + + is-equiv-map-inv-fam-equiv : is-fiberwise-equiv map-inv-fam-equiv + is-equiv-map-inv-fam-equiv = is-equiv-map-fam-equiv inv-fam-equiv +``` + ## Properties ### Families of equivalences are equivalent to fiberwise equivalences diff --git a/src/foundation-core/transport-along-identifications.lagda.md b/src/foundation-core/transport-along-identifications.lagda.md index 49b511e7e0..1dda4c800f 100644 --- a/src/foundation-core/transport-along-identifications.lagda.md +++ b/src/foundation-core/transport-along-identifications.lagda.md @@ -68,6 +68,15 @@ module _ preserves-tr p x ＝ inv (tr-ap id f p x) ∙ ap (λ q → tr B q (f i x)) (ap-id p) compute-preserves-tr refl x = refl + +module _ + {l1 l2 : Level} {I : UU l1} {A : I → UU l2} + where + + compute-preserves-tr-id : + {i j : I} (p : i ＝ j) (x : A i) → + preserves-tr (λ i → id {A = A i}) p x ＝ refl + compute-preserves-tr-id refl x = refl ``` ### Substitution law for transport diff --git a/src/foundation/commuting-squares-of-maps.lagda.md b/src/foundation/commuting-squares-of-maps.lagda.md index 347bb16120..57662665f2 100644 --- a/src/foundation/commuting-squares-of-maps.lagda.md +++ b/src/foundation/commuting-squares-of-maps.lagda.md @@ -13,7 +13,11 @@ open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.commuting-triangles-of-homotopies open import foundation.commuting-triangles-of-maps +open import foundation.dependent-pair-types +open import foundation.embeddings open import foundation.function-extensionality +open import foundation.functoriality-dependent-function-types +open import foundation.homotopies open import foundation.homotopy-algebra open import foundation.postcomposition-functions open import foundation.precomposition-functions @@ -27,7 +31,6 @@ open import foundation-core.commuting-squares-of-homotopies open import foundation-core.commuting-squares-of-identifications open import foundation-core.equivalences open import foundation-core.function-types -open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.whiskering-identifications-concatenation ``` @@ -597,6 +600,58 @@ module _ ( sq-right-top ·r top-left)))) ``` +### Vertical pasting of a square with the right leg an equivalence is an equivalence + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6} + (top : A → X) (top-left : A → B) (top-right : X → Y) (mid : B → Y) + (bottom-left : B → C) (bottom-right : Y → Z) (bottom : C → Z) + (K : coherence-square-maps mid bottom-left bottom-right bottom) + (is-emb-bottom-right : is-emb bottom-right) + where + + is-equiv-pasting-vertical-coherence-square-maps : + is-equiv + ( λ H → + pasting-vertical-coherence-square-maps + ( top) + ( top-left) + ( top-right) + ( mid) + ( bottom-left) + ( bottom-right) + ( bottom) + ( H) + ( K)) + is-equiv-pasting-vertical-coherence-square-maps = + is-equiv-comp _ _ + ( is-equiv-map-Π-is-fiberwise-equiv (λ _ → is-emb-bottom-right _ _)) + ( is-equiv-concat-htpy (K ·r top-left) _) + + equiv-pasting-vertical-coherence-square-maps : + coherence-square-maps top top-left top-right mid ≃ + coherence-square-maps + ( top) + ( bottom-left ∘ top-left) + ( bottom-right ∘ top-right) + ( bottom) + pr1 equiv-pasting-vertical-coherence-square-maps H = + pasting-vertical-coherence-square-maps + ( top) + ( top-left) + ( top-right) + ( mid) + ( bottom-left) + ( bottom-right) + ( bottom) + ( H) + ( K) + pr2 equiv-pasting-vertical-coherence-square-maps = + is-equiv-pasting-vertical-coherence-square-maps +``` + ### Distributivity of pasting squares and transposing by precomposition Given two commuting squares which can be composed horizontally (vertically), we diff --git a/src/foundation/dependent-identifications.lagda.md b/src/foundation/dependent-identifications.lagda.md index 4a1da7c967..7267f431ab 100644 --- a/src/foundation/dependent-identifications.lagda.md +++ b/src/foundation/dependent-identifications.lagda.md @@ -116,14 +116,22 @@ module _ dependent-identification B p x' y' → dependent-identification B q y' z' → dependent-identification B (p ∙ q) x' z' - concat-dependent-identification refl q refl q' = q' + concat-dependent-identification refl q p' q' = ap (tr B q) p' ∙ q' compute-concat-dependent-identification-left-base-refl : { y z : A} (q : y ＝ z) → { x' y' : B y} {z' : B z} (p' : x' ＝ y') → ( q' : dependent-identification B q y' z') → concat-dependent-identification refl q p' q' ＝ ap (tr B q) p' ∙ q' - compute-concat-dependent-identification-left-base-refl q refl q' = refl + compute-concat-dependent-identification-left-base-refl q p' q' = refl + + compute-concat-dependent-identification : + {x y z : A} (p : x ＝ y) (q : y ＝ z) → + {x' : B x} {y' : B y} {z' : B z} → + (p' : dependent-identification B p x' y') → + (q' : dependent-identification B q y' z') → + concat-dependent-identification p q p' q' ＝ tr-concat p q x' ∙ ap (tr B q) p' ∙ q' + compute-concat-dependent-identification refl q p' q' = refl ``` #### Strictly right unital concatenation of dependent identifications diff --git a/src/foundation/families-of-equivalences.lagda.md b/src/foundation/families-of-equivalences.lagda.md index 3cfded46ff..f9b864e830 100644 --- a/src/foundation/families-of-equivalences.lagda.md +++ b/src/foundation/families-of-equivalences.lagda.md @@ -9,10 +9,13 @@ open import foundation-core.families-of-equivalences public
Imports ```agda +open import foundation.equality-dependent-function-types open import foundation.equivalences +open import foundation.univalence open import foundation.universe-levels open import foundation-core.propositions +open import foundation-core.torsorial-type-families ```
@@ -28,6 +31,19 @@ A **family of equivalences** is a family of [equivalences](foundation-core.equivalences.md). Families of equivalences are also called **fiberwise equivalences**. +## Definitions + +### The family of identity equivalences + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + id-fam-equiv : fam-equiv B B + id-fam-equiv a = id-equiv +``` + ## Properties ### Being a fiberwise equivalence is a proposition @@ -43,6 +59,22 @@ module _ is-prop-Π (λ a → is-property-is-equiv (f a)) ``` +### TODO + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + is-torsorial-fam-equiv : is-torsorial (fam-equiv B) + is-torsorial-fam-equiv = + is-torsorial-Eq-Π (λ a → is-torsorial-equiv (B a)) + + is-torsorial-fam-equiv' : is-torsorial (λ C → fam-equiv C B) + is-torsorial-fam-equiv' = + is-torsorial-Eq-Π (λ a → is-torsorial-equiv' (B a)) +``` + ## See also - In diff --git a/src/foundation/fiberwise-equivalence-induction.lagda.md b/src/foundation/fiberwise-equivalence-induction.lagda.md new file mode 100644 index 0000000000..51cc0a5577 --- /dev/null +++ b/src/foundation/fiberwise-equivalence-induction.lagda.md @@ -0,0 +1,119 @@ +# Fiberwise equivalence induction + +```agda +module foundation.fiberwise-equivalence-induction where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.families-of-equivalences +open import foundation.identity-systems +open import foundation.identity-types +-- open import foundation.subuniverses +-- open import foundation.univalence +-- open import foundation.universal-property-identity-systems +open import foundation.universe-levels + +-- open import foundation-core.commuting-triangles-of-maps +-- open import foundation-core.contractible-maps +-- open import foundation-core.function-types +-- open import foundation-core.postcomposition-functions +-- open import foundation-core.sections +-- open import foundation-core.torsorial-type-families +``` + +
+ +## Idea + +## Definitions + +### Evaluation at the family of identity equivalences + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {P : A → UU l2} + (R : (Q : A → UU l2) → fam-equiv P Q → UU l3) + where + + ev-id-fam-equiv : + ((Q : A → UU l2) → (e : fam-equiv P Q) → R Q e) → + R P id-fam-equiv + ev-id-fam-equiv r = r P id-fam-equiv +``` + +### The induction principle of families of equivalences + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (P : A → UU l2) + where + + induction-principle-fam-equiv : UUω + induction-principle-fam-equiv = + is-identity-system (λ (Q : A → UU l2) → fam-equiv P Q) P id-fam-equiv + + induction-principle-fam-equiv' : UUω + induction-principle-fam-equiv' = + is-identity-system (λ (Q : A → UU l2) → fam-equiv Q P) P id-fam-equiv +``` + +## Theorems + +### Induction on families of equivalences + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {P : A → UU l2} + where + + abstract + is-identity-system-fam-equiv : induction-principle-fam-equiv P + is-identity-system-fam-equiv = + is-identity-system-is-torsorial P + ( id-fam-equiv) + ( is-torsorial-fam-equiv) + + is-identity-system-fam-equiv' : induction-principle-fam-equiv' P + is-identity-system-fam-equiv' = + is-identity-system-is-torsorial P + ( id-fam-equiv) + ( is-torsorial-fam-equiv') + +module _ + {l1 l2 l3 : Level} {A : UU l1} {P : A → UU l2} + (R : (Q : A → UU l2) → fam-equiv P Q → UU l3) + (r : R P id-fam-equiv) + where + + abstract + ind-fam-equiv : + {Q : A → UU l2} (e : fam-equiv P Q) → R Q e + ind-fam-equiv {Q = Q} e = + pr1 (is-identity-system-fam-equiv R) r Q e + + compute-ind-fam-equiv : + ind-fam-equiv id-fam-equiv ＝ r + compute-ind-fam-equiv = + pr2 (is-identity-system-fam-equiv R) r + +module _ + {l1 l2 l3 : Level} {A : UU l1} {P : A → UU l2} + (R : (Q : A → UU l2) → fam-equiv Q P → UU l3) + (r : R P id-fam-equiv) + where + + abstract + ind-fam-equiv' : + {Q : A → UU l2} (e : fam-equiv Q P) → R Q e + ind-fam-equiv' {Q = Q} e = + pr1 (is-identity-system-fam-equiv' R) r Q e + + compute-ind-fam-equiv' : + ind-fam-equiv' id-fam-equiv ＝ r + compute-ind-fam-equiv' = + pr2 (is-identity-system-fam-equiv' R) r +``` diff --git a/src/foundation/transposition-identifications-along-equivalences.lagda.md b/src/foundation/transposition-identifications-along-equivalences.lagda.md index ef7e0b1cc7..b7bd10a460 100644 --- a/src/foundation/transposition-identifications-along-equivalences.lagda.md +++ b/src/foundation/transposition-identifications-along-equivalences.lagda.md @@ -127,6 +127,11 @@ module _ {a : A} {b : B} → map-inv-equiv e b ＝ a → b ＝ map-equiv e a map-inv-eq-transpose-equiv-inv {a} {b} = map-inv-equiv (eq-transpose-equiv-inv a b) + + map-eq-transpose-equiv-inv' : + {a : A} {b : B} → b ＝ map-equiv e a → map-inv-equiv e b ＝ a + map-eq-transpose-equiv-inv' {a} {b} p = + ap (map-inv-equiv e) p ∙ is-retraction-map-inv-equiv e a ``` ## Properties @@ -155,6 +160,12 @@ module _ ( equiv-ap e _ _) ( ( right-unit) ∙ ( coherence-map-inv-equiv e _)) + + compute-refl-eq-transpose-equiv-inv' : + {x : A} → + map-eq-transpose-equiv-inv' e refl ＝ is-retraction-map-inv-equiv e x + compute-refl-eq-transpose-equiv-inv' = + refl ``` ### The two definitions of transposing identifications along equivalences are homotopic diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md index f05ba2976d..52b42811e2 100644 --- a/src/synthetic-homotopy-theory.lagda.md +++ b/src/synthetic-homotopy-theory.lagda.md @@ -51,6 +51,7 @@ open import synthetic-homotopy-theory.descent-circle-function-types public open import synthetic-homotopy-theory.descent-circle-subtypes public open import synthetic-homotopy-theory.descent-data-equivalence-types-over-pushouts public open import synthetic-homotopy-theory.descent-data-function-types-over-pushouts public +open import synthetic-homotopy-theory.descent-data-function-types-over-sequential-colimits public open import synthetic-homotopy-theory.descent-data-identity-types-over-pushouts public open import synthetic-homotopy-theory.descent-data-pushouts public open import synthetic-homotopy-theory.descent-data-sequential-colimits public @@ -72,6 +73,7 @@ open import synthetic-homotopy-theory.flattening-lemma-sequential-colimits publi open import synthetic-homotopy-theory.free-loops public open import synthetic-homotopy-theory.functoriality-loop-spaces public open import synthetic-homotopy-theory.functoriality-sequential-colimits public +open import synthetic-homotopy-theory.functoriality-stuff public open import synthetic-homotopy-theory.functoriality-suspensions public open import synthetic-homotopy-theory.groups-of-loops-in-1-types public open import synthetic-homotopy-theory.hatchers-acyclic-type public @@ -120,6 +122,7 @@ open import synthetic-homotopy-theory.smash-products-of-pointed-types public open import synthetic-homotopy-theory.spectra public open import synthetic-homotopy-theory.sphere-prespectrum public open import synthetic-homotopy-theory.spheres public +open import synthetic-homotopy-theory.stuff-over public open import synthetic-homotopy-theory.suspension-prespectra public open import synthetic-homotopy-theory.suspension-structures public open import synthetic-homotopy-theory.suspensions-of-pointed-types public @@ -139,5 +142,6 @@ open import synthetic-homotopy-theory.universal-property-sequential-colimits pub open import synthetic-homotopy-theory.universal-property-suspensions public open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types public open import synthetic-homotopy-theory.wedges-of-pointed-types public +open import synthetic-homotopy-theory.zigzag-construction-identity-type-pushouts public open import synthetic-homotopy-theory.zigzags-sequential-diagrams public ``` diff --git a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md index ca4adb47b0..c9bcd3532d 100644 --- a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md @@ -24,6 +24,7 @@ open import foundation.torsorial-type-families open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation.whiskering-homotopies-composition +open import foundation.whiskering-homotopies-concatenation open import synthetic-homotopy-theory.dependent-sequential-diagrams open import synthetic-homotopy-theory.equifibered-sequential-diagrams @@ -208,6 +209,40 @@ module _ ( coherence-htpy-htpy-cocone-sequential-diagram K n) ``` +### Homotopies of homotopies of cocones under a sequential diagram + +```agda +module _ + {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2} + {c c' : cocone-sequential-diagram A X} + (H H' : htpy-cocone-sequential-diagram c c') + where + + coherence-htpy²-cocone-sequential-diagram : + ((n : ℕ) → + htpy-htpy-cocone-sequential-diagram H n ~ + htpy-htpy-cocone-sequential-diagram H' n) → + UU (l1 ⊔ l2) + coherence-htpy²-cocone-sequential-diagram α = + (n : ℕ) → + coherence-square-homotopies + ( left-whisker-concat-htpy + ( coherence-cocone-sequential-diagram c n) + ( α (succ-ℕ n) ·r map-sequential-diagram A n)) + ( coherence-htpy-htpy-cocone-sequential-diagram H n) + ( coherence-htpy-htpy-cocone-sequential-diagram H' n) + ( right-whisker-concat-htpy + ( α n) + ( coherence-cocone-sequential-diagram c' n)) + + htpy²-cocone-sequential-diagram : UU (l1 ⊔ l2) + htpy²-cocone-sequential-diagram = + Σ ( (n : ℕ) → + htpy-htpy-cocone-sequential-diagram H n ~ + htpy-htpy-cocone-sequential-diagram H' n) + ( coherence-htpy²-cocone-sequential-diagram) +``` + ### Postcomposing cocones under a sequential diagram with a map Given a cocone `c` with vertex `X` under `(A, a)` and a map `f : X → Y`, we may @@ -355,6 +390,60 @@ module _ map-inv-equiv (extensionality-cocone-sequential-diagram c') ``` +### Characterization of identity types of homotopies of cocones under sequential diagrams + +```agda +module _ + {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2} + {c c' : cocone-sequential-diagram A X} + (H : htpy-cocone-sequential-diagram c c') + where + + refl-htpy²-cocone-sequential-diagram : + htpy²-cocone-sequential-diagram H H + pr1 refl-htpy²-cocone-sequential-diagram n = refl-htpy + pr2 refl-htpy²-cocone-sequential-diagram n = right-unit-htpy + + htpy²-eq-cocone-sequential-diagram : + (H' : htpy-cocone-sequential-diagram c c') → + (H ＝ H') → htpy²-cocone-sequential-diagram H H' + htpy²-eq-cocone-sequential-diagram .H refl = + refl-htpy²-cocone-sequential-diagram + + abstract + is-torsorial-htpy²-cocone-sequential-diagram : + is-torsorial (htpy²-cocone-sequential-diagram H) + is-torsorial-htpy²-cocone-sequential-diagram = + is-torsorial-Eq-structure + ( is-torsorial-binary-htpy (htpy-htpy-cocone-sequential-diagram H)) + ( htpy-htpy-cocone-sequential-diagram H , refl-binary-htpy _) + ( is-torsorial-binary-htpy + ( λ n → + coherence-htpy-htpy-cocone-sequential-diagram H n ∙h refl-htpy)) + + is-equiv-htpy²-eq-cocone-sequential-diagram : + (H' : htpy-cocone-sequential-diagram c c') → + is-equiv (htpy²-eq-cocone-sequential-diagram H') + is-equiv-htpy²-eq-cocone-sequential-diagram = + fundamental-theorem-id + ( is-torsorial-htpy²-cocone-sequential-diagram) + ( htpy²-eq-cocone-sequential-diagram) + + extensionality-htpy-eq-cocone-sequential-diagram : + (H' : htpy-cocone-sequential-diagram c c') → + (H ＝ H') ≃ htpy²-cocone-sequential-diagram H H' + pr1 (extensionality-htpy-eq-cocone-sequential-diagram H') = + htpy²-eq-cocone-sequential-diagram H' + pr2 (extensionality-htpy-eq-cocone-sequential-diagram H') = + is-equiv-htpy²-eq-cocone-sequential-diagram H' + + eq-htpy²-cocone-sequential-diagram : + (H' : htpy-cocone-sequential-diagram c c') → + htpy²-cocone-sequential-diagram H H' → H ＝ H' + eq-htpy²-cocone-sequential-diagram H' = + map-inv-equiv (extensionality-htpy-eq-cocone-sequential-diagram H') +``` + ### Postcomposing a cocone under a sequential diagram by identity is the identity ```agda diff --git a/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md index debb9262d7..95280a4e84 100644 --- a/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md @@ -1,6 +1,7 @@ # Dependent cocones under sequential diagrams ```agda +{-# OPTIONS --allow-unsolved-metas #-} module synthetic-homotopy-theory.dependent-cocones-under-sequential-diagrams where ``` @@ -158,6 +159,37 @@ module _ coherence-htpy-htpy-dependent-cocone-sequential-diagram = pr2 H ``` +### Inversion of homotopies of dependent cocones under sequential diagrams + +```agda +module _ + {l1 l2 l3 : Level} {A : sequential-diagram l1} {X : UU l2} + {c : cocone-sequential-diagram A X} (P : X → UU l3) + {d d' : dependent-cocone-sequential-diagram c P} + (H : htpy-dependent-cocone-sequential-diagram P d d') + where + + inv-htpy-dependent-cocone-sequential-diagram : + htpy-dependent-cocone-sequential-diagram P d' d + inv-htpy-dependent-cocone-sequential-diagram = ? +``` + +### Concatenation of homotopies of dependent cocones under sequential diagrams + +```agda +module _ + {l1 l2 l3 : Level} {A : sequential-diagram l1} {X : UU l2} + {c : cocone-sequential-diagram A X} (P : X → UU l3) + {d d' d'' : dependent-cocone-sequential-diagram c P} + (H : htpy-dependent-cocone-sequential-diagram P d d') + (K : htpy-dependent-cocone-sequential-diagram P d' d'') + where + + concat-htpy-dependent-cocone-sequential-diagram : + htpy-dependent-cocone-sequential-diagram P d d'' + concat-htpy-dependent-cocone-sequential-diagram = {!!} +``` + ### Obtaining dependent cocones under sequential diagrams by postcomposing cocones under sequential diagrams with dependent maps Given a cocone `c` with vertex `X`, and a dependent map `h : (x : X) → P x`, we diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md index 449c744b8e..e2607d3474 100644 --- a/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md @@ -196,35 +196,36 @@ module _ ( c : cocone-sequential-diagram A X) where - universal-property-dependent-universal-property-sequential-colimit : - dependent-universal-property-sequential-colimit c → - universal-property-sequential-colimit c - universal-property-dependent-universal-property-sequential-colimit - ( dup-c) - ( Y) = - is-equiv-left-map-triangle - ( cocone-map-sequential-diagram c) - ( map-compute-dependent-cocone-sequential-diagram-constant-family Y) - ( dependent-cocone-map-sequential-diagram c (λ _ → Y)) - ( triangle-compute-dependent-cocone-sequential-diagram-constant-family - ( Y)) - ( dup-c (λ _ → Y)) - ( is-equiv-map-equiv - ( compute-dependent-cocone-sequential-diagram-constant-family Y)) - - dependent-universal-property-universal-property-sequential-colimit : - universal-property-sequential-colimit c → - dependent-universal-property-sequential-colimit c - dependent-universal-property-universal-property-sequential-colimit - ( up-sequential-diagram) = - dependent-universal-property-sequential-colimit-dependent-universal-property-coequalizer - ( c) - ( dependent-universal-property-universal-property-coequalizer - ( double-arrow-sequential-diagram A) - ( cofork-cocone-sequential-diagram c) - ( universal-property-coequalizer-universal-property-sequential-colimit - ( c) - ( up-sequential-diagram))) + abstract + universal-property-dependent-universal-property-sequential-colimit : + dependent-universal-property-sequential-colimit c → + universal-property-sequential-colimit c + universal-property-dependent-universal-property-sequential-colimit + ( dup-c) + ( Y) = + is-equiv-left-map-triangle + ( cocone-map-sequential-diagram c) + ( map-compute-dependent-cocone-sequential-diagram-constant-family Y) + ( dependent-cocone-map-sequential-diagram c (λ _ → Y)) + ( triangle-compute-dependent-cocone-sequential-diagram-constant-family + ( Y)) + ( dup-c (λ _ → Y)) + ( is-equiv-map-equiv + ( compute-dependent-cocone-sequential-diagram-constant-family Y)) + + dependent-universal-property-universal-property-sequential-colimit : + universal-property-sequential-colimit c → + dependent-universal-property-sequential-colimit c + dependent-universal-property-universal-property-sequential-colimit + ( up-sequential-diagram) = + dependent-universal-property-sequential-colimit-dependent-universal-property-coequalizer + ( c) + ( dependent-universal-property-universal-property-coequalizer + ( double-arrow-sequential-diagram A) + ( cofork-cocone-sequential-diagram c) + ( universal-property-coequalizer-universal-property-sequential-colimit + ( c) + ( up-sequential-diagram))) ``` ### The 3-for-2 property of the dependent universal property of sequential colimits diff --git a/src/synthetic-homotopy-theory/descent-data-function-types-over-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/descent-data-function-types-over-sequential-colimits.lagda.md new file mode 100644 index 0000000000..1a615a1cae --- /dev/null +++ b/src/synthetic-homotopy-theory/descent-data-function-types-over-sequential-colimits.lagda.md @@ -0,0 +1,91 @@ +# Descent data for type families of function types over sequential colimits + +```agda +{-# OPTIONS --lossy-unification --allow-unsolved-metas #-} + +module synthetic-homotopy-theory.descent-data-function-types-over-sequential-colimits where +``` + +
Imports + +```agda +-- open import foundation.commuting-squares-of-maps +-- open import foundation.commuting-triangles-of-maps +-- open import foundation.contractible-maps +-- open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.equivalences +-- open import foundation.fibers-of-maps +-- open import foundation.function-extensionality +-- open import foundation.function-types +-- open import foundation.functoriality-dependent-function-types +-- open import foundation.functoriality-dependent-pair-types +-- open import foundation.homotopies +-- open import foundation.homotopy-algebra +open import foundation.postcomposition-functions +-- open import foundation.transport-along-identifications +open import foundation.universal-property-equivalences +open import foundation.universe-levels +-- open import foundation.whiskering-homotopies-composition + +open import synthetic-homotopy-theory.cocones-under-sequential-diagrams +open import synthetic-homotopy-theory.descent-data-sequential-colimits +-- open import synthetic-homotopy-theory.equivalences-descent-data-pushouts +open import synthetic-homotopy-theory.families-descent-data-sequential-colimits +-- open import synthetic-homotopy-theory.morphisms-descent-data-pushouts +-- open import synthetic-homotopy-theory.sections-descent-data-pushouts +open import synthetic-homotopy-theory.sequential-diagrams +-- open import synthetic-homotopy-theory.universal-property-pushouts +``` + +## Idea + +## Definitions + +### TODO + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} {A : sequential-diagram l1} + {X : UU l3} {c : cocone-sequential-diagram A X} + (P : family-with-descent-data-sequential-colimit c l4) + (Q : family-with-descent-data-sequential-colimit c l5) + where + + family-cocone-function-type-sequential-colimit : X → UU (l4 ⊔ l5) + family-cocone-function-type-sequential-colimit x = + family-cocone-family-with-descent-data-sequential-colimit P x → + family-cocone-family-with-descent-data-sequential-colimit Q x + + descent-data-function-type-sequential-colimit : + descent-data-sequential-colimit A (l4 ⊔ l5) + pr1 descent-data-function-type-sequential-colimit n a = + family-family-with-descent-data-sequential-colimit P n a → + family-family-with-descent-data-sequential-colimit Q n a + pr2 descent-data-function-type-sequential-colimit n a = + ( equiv-postcomp _ + ( equiv-family-family-with-descent-data-sequential-colimit Q n a)) ∘e + ( equiv-precomp + ( inv-equiv (equiv-family-family-with-descent-data-sequential-colimit P n a)) + ( _)) +``` + +## Properties + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : sequential-diagram l1} + {X : UU l2} {c : cocone-sequential-diagram A X} + (P : family-with-descent-data-sequential-colimit c l3) + (Q : family-with-descent-data-sequential-colimit c l4) + where + + equiv-hom-descent-data-map-family-cocone-sequential-diagram : + ( (x : X) → + family-cocone-family-with-descent-data-sequential-colimit P x → + family-cocone-family-with-descent-data-sequential-colimit Q x) ≃ + ( hom-descent-data-sequential-colimit + ( descent-data-family-with-descent-data-sequential-colimit P) + ( descent-data-family-with-descent-data-sequential-colimit Q)) + equiv-hom-descent-data-map-family-cocone-sequential-diagram = {!!} +``` diff --git a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md index 020d2dcefb..80fd5e1b19 100644 --- a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md @@ -106,6 +106,13 @@ module _ map-family-descent-data-pushout s = map-equiv (equiv-family-descent-data-pushout s) + inv-map-family-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + right-family-descent-data-pushout (right-map-span-diagram 𝒮 s) → + left-family-descent-data-pushout (left-map-span-diagram 𝒮 s) + inv-map-family-descent-data-pushout s = + map-inv-equiv (equiv-family-descent-data-pushout s) + is-equiv-map-family-descent-data-pushout : (s : spanning-type-span-diagram 𝒮) → is-equiv (map-family-descent-data-pushout s) diff --git a/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md index d498ebe3db..2114f82abb 100644 --- a/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md @@ -180,6 +180,39 @@ module _ id-equiv-descent-data-sequential-colimit = id-equiv-dependent-sequential-diagram ( dependent-sequential-diagram-equifibered-sequential-diagram B) + +module _ + {l1 l2 l3 l4 : Level} {A : sequential-diagram l1} + (B : descent-data-sequential-colimit A l2) + (C : descent-data-sequential-colimit A l3) + (D : descent-data-sequential-colimit A l4) + (f : equiv-descent-data-sequential-colimit C D) + (e : equiv-descent-data-sequential-colimit B C) + where + + comp-equiv-descent-data-sequential-colimit : + equiv-descent-data-sequential-colimit B D + comp-equiv-descent-data-sequential-colimit = + comp-equiv-dependent-sequential-diagram + ( dependent-sequential-diagram-equifibered-sequential-diagram B) + ( dependent-sequential-diagram-equifibered-sequential-diagram C) + ( dependent-sequential-diagram-equifibered-sequential-diagram D) + ( f) + ( e) + +module _ + {l1 l2 l3 : Level} {A : sequential-diagram l1} + (B : descent-data-sequential-colimit A l2) + (C : descent-data-sequential-colimit A l3) + where + + inv-equiv-descent-data-sequential-colimit : + equiv-descent-data-sequential-colimit B C → + equiv-descent-data-sequential-colimit C B + inv-equiv-descent-data-sequential-colimit e = + inv-equiv-dependent-sequential-diagram + ( dependent-sequential-diagram-equifibered-sequential-diagram C) + ( e) ``` ### Descent data induced by families over cocones under sequential diagrams diff --git a/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md index 20b9c33dc7..c36ea4cad1 100644 --- a/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md @@ -10,6 +10,7 @@ module synthetic-homotopy-theory.descent-property-sequential-colimits where open import elementary-number-theory.natural-numbers open import foundation.binary-homotopies +open import foundation.commuting-squares-of-maps open import foundation.commuting-triangles-of-maps open import foundation.dependent-pair-types open import foundation.equality-dependent-pair-types @@ -22,6 +23,7 @@ open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-sequential-diagrams open import synthetic-homotopy-theory.descent-data-sequential-colimits +open import synthetic-homotopy-theory.families-descent-data-sequential-colimits open import synthetic-homotopy-theory.sequential-diagrams open import synthetic-homotopy-theory.universal-property-sequential-colimits ``` @@ -135,3 +137,213 @@ module _ map-inv-equiv ( equiv-descent-data-family-cocone-sequential-diagram) ``` + +```agda +open import synthetic-homotopy-theory.morphisms-sequential-diagrams +open import synthetic-homotopy-theory.morphisms-dependent-sequential-diagrams +open import synthetic-homotopy-theory.descent-data-function-types-over-sequential-colimits +open import foundation.action-on-identifications-functions +open import foundation.transport-along-higher-identifications +open import foundation.transport-along-identifications +open import foundation.function-types +open import foundation.whiskering-homotopies-composition +open import foundation.homotopies +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} + {P : A → UU l3} {Q : B → UU l4} + (f : A → B) (h : (a : A) → P a → Q (f a)) + where + + other-nat-lemma : + {x y : A} (p : x ＝ y) (q : f x ＝ f y) (α : ap f p ＝ q) → + (z : P x) → + tr Q q (h x z) ＝ h y (tr P p z) + other-nat-lemma p q α z = + inv (preserves-tr h p z ∙ (inv (substitution-law-tr Q f p) ∙ tr² Q α _)) +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : sequential-diagram l1} {B : sequential-diagram l2} + {X : UU l3} {c : cocone-sequential-diagram A X} + {Y : UU l4} {c' : cocone-sequential-diagram B Y} + (P : family-with-descent-data-sequential-colimit c l5) + (Q : family-with-descent-data-sequential-colimit c' l6) + (f : hom-sequential-diagram A B) + (f∞ : X → Y) + (C : + (n : ℕ) → + coherence-square-maps + ( map-hom-sequential-diagram B f n) + ( map-cocone-sequential-diagram c n) + ( map-cocone-sequential-diagram c' n) + ( f∞)) + (α : + (n : ℕ) → + ( (f∞ ·l (coherence-cocone-sequential-diagram c n)) ∙h + ( C (succ-ℕ n) ·r map-sequential-diagram A n)) ~ + ( ( C n) ∙h + ( coherence-cocone-sequential-diagram c' n ·r (map-hom-sequential-diagram B f n)) ∙h + ( map-cocone-sequential-diagram c' (succ-ℕ n) ·l naturality-map-hom-sequential-diagram B f n))) + where + + dd-alt-pullback : descent-data-sequential-colimit A l6 + pr1 dd-alt-pullback n a = + family-cocone-family-with-descent-data-sequential-colimit Q + ( map-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)) + pr2 dd-alt-pullback n a = + equiv-tr + ( family-cocone-family-with-descent-data-sequential-colimit Q) + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∘e + equiv-tr + ( family-cocone-family-with-descent-data-sequential-colimit Q) + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)) + + dd-alt-precomp : descent-data-sequential-colimit A l6 + pr1 dd-alt-precomp n a = + family-family-with-descent-data-sequential-colimit Q n + ( map-hom-sequential-diagram B f n a) + pr2 dd-alt-precomp n a = + ( equiv-tr + ( family-family-with-descent-data-sequential-colimit Q (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∘e + ( equiv-family-family-with-descent-data-sequential-colimit Q n + ( map-hom-sequential-diagram B f n a)) + + equiv-dd-foo : + equiv-descent-data-sequential-colimit + ( descent-data-family-cocone-sequential-diagram c + ( family-cocone-family-with-descent-data-sequential-colimit Q ∘ f∞)) + ( dd-alt-pullback) + pr1 equiv-dd-foo n a = + equiv-tr + ( family-cocone-family-with-descent-data-sequential-colimit Q) + ( C n a) + pr2 equiv-dd-foo n a q = + ( ap + ( tr (family-cocone-family-with-descent-data-sequential-colimit Q) (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( inv + ( substitution-law-tr + ( family-cocone-family-with-descent-data-sequential-colimit Q) + ( f∞) + ( coherence-cocone-sequential-diagram c n a)))) ∙ + ( inv + ( tr-concat + ( ap f∞ (coherence-cocone-sequential-diagram c n a)) + ( C (succ-ℕ n) (map-sequential-diagram A n a)) + ( q))) ∙ + ( tr² + ( family-cocone-family-with-descent-data-sequential-colimit Q) + ( α n a) + ( q)) ∙ + ( tr-concat (C n a ∙ pr2 c' n (pr1 f n a)) _ q) ∙ + ap + ( tr (family-cocone-family-with-descent-data-sequential-colimit Q) (ap (pr1 c' (succ-ℕ n)) (pr2 f n a))) + ( tr-concat (C n a) (pr2 c' n (pr1 f n a)) q) + + private + inv-equiv-e : + equiv-descent-data-sequential-colimit + ( descent-data-family-cocone-sequential-diagram c' + ( family-cocone-family-with-descent-data-sequential-colimit Q)) + ( descent-data-family-with-descent-data-sequential-colimit Q) + inv-equiv-e = + inv-equiv-descent-data-sequential-colimit + ( descent-data-family-with-descent-data-sequential-colimit Q) + ( descent-data-family-cocone-sequential-diagram c' + ( family-cocone-family-with-descent-data-sequential-colimit Q)) + ( equiv-descent-data-family-with-descent-data-sequential-colimit Q) + + equiv-equiv-dd-foo' : (n : ℕ) (b : family-sequential-diagram B n) → + ( family-cocone-family-with-descent-data-sequential-colimit Q + ( map-cocone-sequential-diagram c' n b)) ≃ + ( family-family-with-descent-data-sequential-colimit Q n b) + equiv-equiv-dd-foo' = + equiv-equiv-descent-data-sequential-colimit + ( descent-data-family-cocone-sequential-diagram c' + ( family-cocone-family-with-descent-data-sequential-colimit Q)) + ( descent-data-family-with-descent-data-sequential-colimit Q) + ( inv-equiv-e) + + equiv-dd-foo' : + equiv-descent-data-sequential-colimit + ( dd-alt-pullback) + ( dd-alt-precomp) + pr1 equiv-dd-foo' n a = + equiv-equiv-dd-foo' n (map-hom-sequential-diagram B f n a) + pr2 equiv-dd-foo' n a = + pasting-vertical-coherence-square-maps + ( map-equiv (equiv-equiv-dd-foo' n (map-hom-sequential-diagram B f n a))) + ( tr + ( family-cocone-family-with-descent-data-sequential-colimit Q) + ( pr2 c' n (pr1 f n a))) + ( map-family-family-with-descent-data-sequential-colimit Q n (map-hom-sequential-diagram B f n a)) + ( map-equiv + ( equiv-equiv-dd-foo' + ( succ-ℕ n) + ( map-sequential-diagram B n (map-hom-sequential-diagram B f n a)))) + ( tr + ( family-cocone-family-with-descent-data-sequential-colimit Q) + ( ap (map-cocone-sequential-diagram c' (succ-ℕ n)) (pr2 f n a))) + ( tr + ( family-family-with-descent-data-sequential-colimit Q (succ-ℕ n)) + ( pr2 f n a)) + ( map-equiv + ( equiv-equiv-dd-foo' + ( succ-ℕ n) + ( map-hom-sequential-diagram B f (succ-ℕ n) (map-sequential-diagram A n a)))) + ( coh-equiv-descent-data-sequential-colimit + ( descent-data-family-cocone-sequential-diagram c' + ( family-cocone-family-with-descent-data-sequential-colimit Q)) + ( descent-data-family-with-descent-data-sequential-colimit Q) + ( inv-equiv-e) + ( n) + ( map-hom-sequential-diagram B f n a)) + ( ( ( map-equiv + ( equiv-equiv-dd-foo' + ( succ-ℕ n) + ( map-hom-sequential-diagram B f + ( succ-ℕ n) + ( map-sequential-diagram A n a)))) ·l + ( λ z → + substitution-law-tr + ( family-cocone-family-with-descent-data-sequential-colimit Q) + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a) {z})) ∙h + ( inv-htpy + ( other-nat-lemma id + ( λ b → map-equiv (equiv-equiv-dd-foo' (succ-ℕ n) b)) + ( pr2 f n a) + ( pr2 f n a) + ( ap-id (pr2 f n a))))) + + hom-over-map-over : + ( (x : X) → + family-cocone-family-with-descent-data-sequential-colimit P x → + family-cocone-family-with-descent-data-sequential-colimit Q (f∞ x)) ≃ + ( hom-dependent-sequential-diagram-over + ( dependent-sequential-diagram-family-with-descent-data-sequential-colimit P) + ( dependent-sequential-diagram-family-with-descent-data-sequential-colimit Q) + ( f)) + hom-over-map-over = + ( equiv-tot + ( λ g → + equiv-Π-equiv-family + ( λ n → equiv-Π-equiv-family (λ a → equiv-inv-htpy _ _)))) ∘e + ( equiv-hom-descent-data-map-family-cocone-sequential-diagram P + ( family-cocone-family-with-descent-data-sequential-colimit Q ∘ f∞ , + dd-alt-precomp , + inv-equiv-descent-data-sequential-colimit + ( descent-data-family-cocone-sequential-diagram c + ( family-cocone-family-with-descent-data-sequential-colimit Q ∘ f∞)) + ( dd-alt-precomp) + ( comp-equiv-descent-data-sequential-colimit + ( descent-data-family-cocone-sequential-diagram c + ( family-cocone-family-with-descent-data-sequential-colimit Q ∘ f∞)) + ( dd-alt-pullback) + ( dd-alt-precomp) + ( equiv-dd-foo') + ( equiv-dd-foo)))) +``` diff --git a/src/synthetic-homotopy-theory/equivalences-dependent-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/equivalences-dependent-sequential-diagrams.lagda.md index 54b42eb7ca..e1a86f6c42 100644 --- a/src/synthetic-homotopy-theory/equivalences-dependent-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/equivalences-dependent-sequential-diagrams.lagda.md @@ -166,7 +166,7 @@ module _ is-equiv-map-equiv-dependent-sequential-diagram C e ``` -### The identity equivalence of sequential diagrams +### The identity equivalence of dependent sequential diagrams ```agda module _ @@ -179,6 +179,61 @@ module _ pr2 id-equiv-dependent-sequential-diagram n a = refl-htpy ``` +### Composition of equivalences of dependent sequential diagrams + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : sequential-diagram l1} + (B : dependent-sequential-diagram A l2) + (C : dependent-sequential-diagram A l3) + (D : dependent-sequential-diagram A l4) + (f : equiv-dependent-sequential-diagram C D) + (e : equiv-dependent-sequential-diagram B C) + where + + comp-equiv-dependent-sequential-diagram : + equiv-dependent-sequential-diagram B D + pr1 comp-equiv-dependent-sequential-diagram n a = + equiv-equiv-dependent-sequential-diagram D f n a ∘e + equiv-equiv-dependent-sequential-diagram C e n a + pr2 comp-equiv-dependent-sequential-diagram n a = + pasting-horizontal-coherence-square-maps + ( map-equiv-dependent-sequential-diagram C e n a) + ( map-equiv-dependent-sequential-diagram D f n a) + ( map-dependent-sequential-diagram B n a) + ( map-dependent-sequential-diagram C n a) + ( map-dependent-sequential-diagram D n a) + ( map-equiv-dependent-sequential-diagram C e (succ-ℕ n) (map-sequential-diagram A n a)) + ( map-equiv-dependent-sequential-diagram D f (succ-ℕ n) (map-sequential-diagram A n a)) + ( coh-equiv-dependent-sequential-diagram C e n a) + ( coh-equiv-dependent-sequential-diagram D f n a) +``` + +### The inverse of an equivalence of dependent sequential diagrams + +```agda +module _ + {l1 l2 l3 : Level} {A : sequential-diagram l1} + {B : dependent-sequential-diagram A l2} + (C : dependent-sequential-diagram A l3) + where + + inv-equiv-dependent-sequential-diagram : + equiv-dependent-sequential-diagram B C → + equiv-dependent-sequential-diagram C B + pr1 (inv-equiv-dependent-sequential-diagram e) n a = + inv-equiv (equiv-equiv-dependent-sequential-diagram C e n a) + pr2 (inv-equiv-dependent-sequential-diagram e) n a = + horizontal-inv-equiv-coherence-square-maps + ( equiv-equiv-dependent-sequential-diagram C e n a) + ( map-dependent-sequential-diagram B n a) + ( map-dependent-sequential-diagram C n a) + ( equiv-equiv-dependent-sequential-diagram C e + ( succ-ℕ n) + ( map-sequential-diagram A n a)) + ( coh-equiv-dependent-sequential-diagram C e n a) +``` + ## Properties ### Morphisms of dependent sequential diagrams which are equivalences are equivalences of dependent sequential diagrams diff --git a/src/synthetic-homotopy-theory/families-descent-data-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/families-descent-data-sequential-colimits.lagda.md index 4343695a69..560da28e46 100644 --- a/src/synthetic-homotopy-theory/families-descent-data-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/families-descent-data-sequential-colimits.lagda.md @@ -32,7 +32,7 @@ the type of type families over is [equivalent](foundation-core.equivalences.md) to [descent data](synthetic-homotopy-theory.descent-data-sequential-colimits.md). -Sometimes it is useful to consider tripes `(P, B, e)` where `P : X → 𝒰` is a +Sometimes it is useful to consider triples `(P, B, e)` where `P : X → 𝒰` is a type family, `B` is descent data, and `e` is an equivalence between `B` and the descent data induced by `P`. The type of such pairs `(B, e)` is [contractible](foundation-core.contractible-types.md), so the type of these diff --git a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md index 1e014f974d..316040ccfa 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md @@ -21,7 +21,6 @@ open import foundation.whiskering-homotopies-composition open import synthetic-homotopy-theory.cocones-under-sequential-diagrams open import synthetic-homotopy-theory.coforks open import synthetic-homotopy-theory.coforks-cocones-under-sequential-diagrams -open import synthetic-homotopy-theory.dependent-universal-property-sequential-colimits open import synthetic-homotopy-theory.equivalences-coforks-under-equivalences-double-arrows open import synthetic-homotopy-theory.families-descent-data-sequential-colimits open import synthetic-homotopy-theory.flattening-lemma-coequalizers diff --git a/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md index e978bc0554..32812f6747 100644 --- a/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md @@ -125,7 +125,7 @@ This homotopy of cocones provides Aₙ ---------> X | | | | ∨ | - fₙ | Bₙ₊₁ | g + fₙ | Bₙ₊₁ | f∞ | ∧ \ | | / \ | ∨/ ∨∨ @@ -146,87 +146,88 @@ module _ ( f : hom-sequential-diagram A B) where - map-sequential-colimit-hom-sequential-diagram : X → Y - map-sequential-colimit-hom-sequential-diagram = - map-universal-property-sequential-colimit up-c - ( map-cocone-hom-sequential-diagram f c') - - htpy-cocone-map-sequential-colimit-hom-sequential-diagram : - htpy-cocone-sequential-diagram - ( cocone-map-sequential-diagram c - ( map-sequential-colimit-hom-sequential-diagram)) - ( map-cocone-hom-sequential-diagram f c') - htpy-cocone-map-sequential-colimit-hom-sequential-diagram = - htpy-cocone-universal-property-sequential-colimit up-c - ( map-cocone-hom-sequential-diagram f c') - - htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram : - ( n : ℕ) → - coherence-square-maps - ( map-hom-sequential-diagram B f n) - ( map-cocone-sequential-diagram c n) - ( map-cocone-sequential-diagram c' n) - ( map-sequential-colimit-hom-sequential-diagram) - htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram = - htpy-htpy-cocone-sequential-diagram - ( htpy-cocone-map-sequential-colimit-hom-sequential-diagram) + opaque + map-sequential-colimit-hom-sequential-diagram : X → Y + map-sequential-colimit-hom-sequential-diagram = + map-universal-property-sequential-colimit up-c + ( map-cocone-hom-sequential-diagram f c') - coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram : - ( n : ℕ) → - coherence-square-homotopies - ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram n) - ( ( map-sequential-colimit-hom-sequential-diagram) ·l - ( coherence-cocone-sequential-diagram c n)) - ( coherence-cocone-sequential-diagram + htpy-cocone-map-sequential-colimit-hom-sequential-diagram : + htpy-cocone-sequential-diagram + ( cocone-map-sequential-diagram c + ( map-sequential-colimit-hom-sequential-diagram)) + ( map-cocone-hom-sequential-diagram f c') + htpy-cocone-map-sequential-colimit-hom-sequential-diagram = + htpy-cocone-universal-property-sequential-colimit up-c ( map-cocone-hom-sequential-diagram f c') - ( n)) - ( ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram - ( succ-ℕ n)) ·r - ( map-sequential-diagram A n)) - coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram = - coherence-htpy-htpy-cocone-sequential-diagram - htpy-cocone-map-sequential-colimit-hom-sequential-diagram - prism-htpy-cocone-map-sequential-colimit-hom-sequential-diagram : - ( n : ℕ) → - vertical-coherence-prism-maps - ( map-cocone-sequential-diagram c n) - ( map-cocone-sequential-diagram c (succ-ℕ n)) - ( map-sequential-diagram A n) - ( map-cocone-sequential-diagram c' n) - ( map-cocone-sequential-diagram c' (succ-ℕ n)) - ( map-sequential-diagram B n) - ( map-hom-sequential-diagram B f n) - ( map-hom-sequential-diagram B f (succ-ℕ n)) - ( map-sequential-colimit-hom-sequential-diagram) - ( coherence-cocone-sequential-diagram c n) - ( inv-htpy - ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram n)) - ( inv-htpy + htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram : + ( n : ℕ) → + coherence-square-maps + ( map-hom-sequential-diagram B f n) + ( map-cocone-sequential-diagram c n) + ( map-cocone-sequential-diagram c' n) + ( map-sequential-colimit-hom-sequential-diagram) + htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram = + htpy-htpy-cocone-sequential-diagram + ( htpy-cocone-map-sequential-colimit-hom-sequential-diagram) + + coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram : + ( n : ℕ) → + coherence-square-homotopies + ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram n) + ( ( map-sequential-colimit-hom-sequential-diagram) ·l + ( coherence-cocone-sequential-diagram c n)) + ( coherence-cocone-sequential-diagram + ( map-cocone-hom-sequential-diagram f c') + ( n)) + ( ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram + ( succ-ℕ n)) ·r + ( map-sequential-diagram A n)) + coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram = + coherence-htpy-htpy-cocone-sequential-diagram + htpy-cocone-map-sequential-colimit-hom-sequential-diagram + + prism-htpy-cocone-map-sequential-colimit-hom-sequential-diagram : + ( n : ℕ) → + vertical-coherence-prism-maps + ( map-cocone-sequential-diagram c n) + ( map-cocone-sequential-diagram c (succ-ℕ n)) + ( map-sequential-diagram A n) + ( map-cocone-sequential-diagram c' n) + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( map-sequential-diagram B n) + ( map-hom-sequential-diagram B f n) + ( map-hom-sequential-diagram B f (succ-ℕ n)) + ( map-sequential-colimit-hom-sequential-diagram) + ( coherence-cocone-sequential-diagram c n) + ( inv-htpy + ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram n)) + ( inv-htpy + ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram + ( succ-ℕ n))) + ( naturality-map-hom-sequential-diagram B f n) + ( coherence-cocone-sequential-diagram c' n) + prism-htpy-cocone-map-sequential-colimit-hom-sequential-diagram n = + rotate-vertical-coherence-prism-maps + ( map-cocone-sequential-diagram c n) + ( map-cocone-sequential-diagram c (succ-ℕ n)) + ( map-sequential-diagram A n) + ( map-cocone-sequential-diagram c' n) + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( map-sequential-diagram B n) + ( map-hom-sequential-diagram B f n) + ( map-hom-sequential-diagram B f (succ-ℕ n)) + ( map-sequential-colimit-hom-sequential-diagram) + ( coherence-cocone-sequential-diagram c n) + ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram n) ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram - ( succ-ℕ n))) - ( naturality-map-hom-sequential-diagram B f n) - ( coherence-cocone-sequential-diagram c' n) - prism-htpy-cocone-map-sequential-colimit-hom-sequential-diagram n = - rotate-vertical-coherence-prism-maps - ( map-cocone-sequential-diagram c n) - ( map-cocone-sequential-diagram c (succ-ℕ n)) - ( map-sequential-diagram A n) - ( map-cocone-sequential-diagram c' n) - ( map-cocone-sequential-diagram c' (succ-ℕ n)) - ( map-sequential-diagram B n) - ( map-hom-sequential-diagram B f n) - ( map-hom-sequential-diagram B f (succ-ℕ n)) - ( map-sequential-colimit-hom-sequential-diagram) - ( coherence-cocone-sequential-diagram c n) - ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram n) - ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram - ( succ-ℕ n)) - ( naturality-map-hom-sequential-diagram B f n) - ( coherence-cocone-sequential-diagram c' n) - ( inv-htpy - ( coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram - ( n))) + ( succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n) + ( coherence-cocone-sequential-diagram c' n) + ( inv-htpy + ( coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram + ( n))) ``` ### Homotopies between morphisms of sequential diagrams induce homotopies of corresponding maps between sequential colimits diff --git a/src/synthetic-homotopy-theory/functoriality-stuff.lagda.md b/src/synthetic-homotopy-theory/functoriality-stuff.lagda.md new file mode 100644 index 0000000000..d4d462cd77 --- /dev/null +++ b/src/synthetic-homotopy-theory/functoriality-stuff.lagda.md @@ -0,0 +1,2189 @@ +# Functoriality stuff + +```agda +{-# OPTIONS --lossy-unification #-} + +module synthetic-homotopy-theory.functoriality-stuff where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-dependent-functions +open import foundation.action-on-identifications-functions +-- open import foundation.binary-homotopies +open import foundation.commuting-squares-of-identifications +open import foundation.commuting-squares-of-maps +open import foundation.commuting-triangles-of-identifications +open import foundation.commuting-triangles-of-maps +-- open import foundation.dependent-identifications +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equality-dependent-pair-types +open import foundation.equivalences +open import foundation.families-of-equivalences +open import foundation.fiberwise-equivalence-induction +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +-- open import foundation.homotopy-induction +open import foundation.identity-types +open import foundation.implicit-function-types +open import foundation.postcomposition-functions +open import foundation.precomposition-dependent-functions +open import foundation.transport-along-identifications +-- open import foundation.transposition-identifications-along-equivalences +open import foundation.universal-property-equivalences +open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition +-- open import foundation.whiskering-homotopies-concatenation + +open import synthetic-homotopy-theory.cocones-under-sequential-diagrams +open import synthetic-homotopy-theory.dependent-cocones-under-sequential-diagrams +open import synthetic-homotopy-theory.dependent-sequential-diagrams +open import synthetic-homotopy-theory.dependent-universal-property-sequential-colimits +open import synthetic-homotopy-theory.descent-data-sequential-colimits +open import synthetic-homotopy-theory.functoriality-sequential-colimits +open import synthetic-homotopy-theory.morphisms-sequential-diagrams +open import synthetic-homotopy-theory.sequential-diagrams +open import synthetic-homotopy-theory.stuff-over +open import synthetic-homotopy-theory.universal-property-sequential-colimits + +open import foundation.binary-homotopies +open import foundation.commuting-squares-of-homotopies +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopy-induction +open import foundation.structure-identity-principle +open import foundation.torsorial-type-families +open import foundation.transposition-identifications-along-equivalences +``` + +
+ +## Theorem + +```agda +module _ + {l1 l2 : Level} + {A : sequential-diagram l1} + (P : descent-data-sequential-colimit A l2) + where + + section-descent-data-sequential-colimit : UU (l1 ⊔ l2) + section-descent-data-sequential-colimit = + section-dependent-sequential-diagram A + ( dependent-sequential-diagram-descent-data P) + +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) + (P : X → UU l3) + where + + sect-family-sect-dd-sequential-colimit : + section-descent-data-sequential-colimit + ( descent-data-family-cocone-sequential-diagram c P) → + ((x : X) → P x) + sect-family-sect-dd-sequential-colimit s = + map-dependent-universal-property-sequential-colimit + ( dependent-universal-property-universal-property-sequential-colimit _ up-c) + ( s) + +module _ + {l1 l2 l3 : Level} {A : sequential-diagram l1} {X : UU l2} + (c : cocone-sequential-diagram A X) + (P : X → UU l3) + where + + section-descent-data-section-family-cocone-sequential-colimit : + ((x : X) → P x) → + section-descent-data-sequential-colimit + ( descent-data-family-cocone-sequential-diagram c P) + section-descent-data-section-family-cocone-sequential-colimit = + dependent-cocone-map-sequential-diagram c P +``` + +```agda +module _ + {l1 l2 : Level} {A : sequential-diagram l1} + {B : dependent-sequential-diagram A l2} + (s t : section-dependent-sequential-diagram A B) + where + + htpy-section-dependent-sequential-diagram : UU (l1 ⊔ l2) + htpy-section-dependent-sequential-diagram = + Σ ((n : ℕ) → + map-section-dependent-sequential-diagram A B s n ~ + map-section-dependent-sequential-diagram A B t n) + ( λ H → + (n : ℕ) → + coherence-square-homotopies + ( map-dependent-sequential-diagram B n _ ·l H n) + ( naturality-map-section-dependent-sequential-diagram A B s n) + ( naturality-map-section-dependent-sequential-diagram A B t n) + ( H (succ-ℕ n) ·r map-sequential-diagram A n)) + +module _ + {l1 l2 : Level} {A : sequential-diagram l1} + {B : dependent-sequential-diagram A l2} + (s : section-dependent-sequential-diagram A B) + where + + refl-htpy-section-dependent-sequential-diagram : + htpy-section-dependent-sequential-diagram s s + pr1 refl-htpy-section-dependent-sequential-diagram n = + refl-htpy + pr2 refl-htpy-section-dependent-sequential-diagram n = + right-unit-htpy + + htpy-eq-section-dependent-sequential-diagram : + (t : section-dependent-sequential-diagram A B) → + s ＝ t → htpy-section-dependent-sequential-diagram s t + htpy-eq-section-dependent-sequential-diagram .s refl = + refl-htpy-section-dependent-sequential-diagram + + abstract + is-torsorial-htpy-section-dependent-sequential-diagram : + is-torsorial (htpy-section-dependent-sequential-diagram s) + is-torsorial-htpy-section-dependent-sequential-diagram = + is-torsorial-Eq-structure + ( is-torsorial-binary-htpy _) + ( pr1 s , λ n → refl-htpy) + ( is-torsorial-binary-htpy _) + + is-equiv-htpy-eq-section-dependent-sequential-diagram : + (t : section-dependent-sequential-diagram A B) → + is-equiv (htpy-eq-section-dependent-sequential-diagram t) + is-equiv-htpy-eq-section-dependent-sequential-diagram = + fundamental-theorem-id + ( is-torsorial-htpy-section-dependent-sequential-diagram) + ( htpy-eq-section-dependent-sequential-diagram) + + equiv-htpy-eq-section-dependent-sequential-diagram : + (t : section-dependent-sequential-diagram A B) → + (s ＝ t) ≃ + htpy-section-dependent-sequential-diagram s t + equiv-htpy-eq-section-dependent-sequential-diagram t = + ( htpy-eq-section-dependent-sequential-diagram t , + is-equiv-htpy-eq-section-dependent-sequential-diagram t) + + eq-htpy-section-dependent-sequential-diagram : + (t : section-dependent-sequential-diagram A B) → + htpy-section-dependent-sequential-diagram s t → + s ＝ t + eq-htpy-section-dependent-sequential-diagram t = + map-inv-equiv (equiv-htpy-eq-section-dependent-sequential-diagram t) + +module _ + {l1 l2 : Level} {A : sequential-diagram l1} + (B : descent-data-sequential-colimit A l2) + (s t : section-descent-data-sequential-colimit B) + where + + eq-htpy-section-descent-data-sequential-colimit : + htpy-section-dependent-sequential-diagram s t → + s ＝ t + eq-htpy-section-descent-data-sequential-colimit = + eq-htpy-section-dependent-sequential-diagram s t + +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) + (P : X → UU l3) + (let P' = descent-data-family-cocone-sequential-diagram c P) + (s t : section-descent-data-sequential-colimit P') + where + + htpy-colimit-htpy-diagram-section : + htpy-section-dependent-sequential-diagram s t → + sect-family-sect-dd-sequential-colimit up-c P s ~ + sect-family-sect-dd-sequential-colimit up-c P t + htpy-colimit-htpy-diagram-section H = + htpy-eq + ( ap + ( sect-family-sect-dd-sequential-colimit up-c P) + ( eq-htpy-section-dependent-sequential-diagram s t H)) +``` + +```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) + (P : X → UU l3) + where + + htpy-section-out-of-sequential-colimit : (s t : (x : X) → P x) → UU (l1 ⊔ l3) + htpy-section-out-of-sequential-colimit s t = + htpy-section-dependent-sequential-diagram + ( section-descent-data-section-family-cocone-sequential-colimit c P s) + ( section-descent-data-section-family-cocone-sequential-colimit c P t) + + equiv-htpy-section-out-of-sequential-colimit : + (s t : (x : X) → P x) → + htpy-section-out-of-sequential-colimit s t ≃ (s ~ t) + equiv-htpy-section-out-of-sequential-colimit s t = + ( inv-equiv + ( equiv-dependent-universal-property-sequential-colimit + ( dependent-universal-property-universal-property-sequential-colimit c + ( up-c)))) ∘e + ( equiv-tot + ( λ H → + equiv-Π-equiv-family + ( λ n → + equiv-Π-equiv-family + ( λ a → + compute-dependent-identification-eq-value s t + ( coherence-cocone-sequential-diagram c n a) + ( H n a) + ( H (succ-ℕ n) (map-sequential-diagram A n a)))))) + + -- (2.i) + htpy-htpy-section-out-of-sequential-colimit : + (s t : (x : X) → P x) → + htpy-section-out-of-sequential-colimit s t → (s ~ t) + htpy-htpy-section-out-of-sequential-colimit s t = + map-equiv (equiv-htpy-section-out-of-sequential-colimit s t) +``` + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + (s : (a : A) → B a) (t : (a : A) → C a) + (e : (a : A) → B a ≃ C a) + (H : (a : A) → map-equiv (e a) (s a) ＝ t a) + where + + -- the rest of the proof relies on the implementation of + -- map-eq-transpose-equiv', which is probably not the best idea + invert-fiberwise-triangle : (a : A) → s a ＝ map-inv-equiv (e a) (t a) + invert-fiberwise-triangle a = map-eq-transpose-equiv' (e a) (H a) + + invert-fiberwise-triangle' : (a : A) → map-inv-equiv (e a) (t a) ＝ s a + invert-fiberwise-triangle' a = + ap (map-inv-equiv (e a)) (inv (H a)) ∙ + is-retraction-map-inv-equiv (e a) (s a) + + compute-inv-invert-fiberwise-triangle : + (a : A) → + inv (invert-fiberwise-triangle a) ＝ + invert-fiberwise-triangle' a + compute-inv-invert-fiberwise-triangle a = + distributive-inv-concat + ( inv (is-retraction-map-inv-equiv (e a) (s a))) + ( ap (map-inv-equiv (e a)) (H a)) ∙ + ap-binary (_∙_) + ( inv (ap-inv (map-inv-equiv (e a)) (H a))) + ( inv-inv (is-retraction-map-inv-equiv (e a) (s a))) + + compute-inv-invert-fiberwise-triangle' : + (a : A) → + inv (invert-fiberwise-triangle' a) ＝ + invert-fiberwise-triangle a + compute-inv-invert-fiberwise-triangle' a = + distributive-inv-concat + ( ap (map-inv-equiv (e a)) (inv (H a))) + ( is-retraction-map-inv-equiv (e a) (s a)) ∙ + ap + ( inv (is-retraction-map-inv-equiv (e a) (s a)) ∙_) + ( ap inv (ap-inv (map-inv-equiv (e a)) (H a)) ∙ inv-inv _) +``` + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} + {P : A → UU l3} {Q : B → UU l4} {P' : A → UU l5} {Q' : B → UU l6} + (f : A → B) + (s : (a : A) → P a) (t : (b : B) → Q b) + (s' : (a : A) → P' a) (t' : (b : B) → Q' b) + (f' : {a : A} → P a → Q (f a)) + (f'' : {a : A} → P' a → Q' (f a)) + (e : {a : A} → P a ≃ P' a) + (let g = λ {a} → map-equiv (e {a})) + (let inv-g = λ {a} → map-inv-equiv (e {a})) + (j : {b : B} → Q b ≃ Q' b) + (let h = λ {b} → map-equiv (j {b})) + (let inv-h = λ {b} → map-inv-equiv (j {b})) + (T : (a : A) → f' (s a) ＝ t (f a)) + (G : {a : A} (p : P a) → f'' (g p) ＝ h (f' p)) + (let + inv-G = + λ {a} (p : P' a) → + vertical-inv-equiv-coherence-square-maps f' e j f'' G p) + (F : (b : B) → h (t b) ＝ t' b) + (let inv-F = invert-fiberwise-triangle t t' (λ b → j {b}) F) + (let inv-F' = invert-fiberwise-triangle' t t' (λ b → j {b}) F) + (H : (a : A) → g (s a) ＝ s' a) + (let inv-H = invert-fiberwise-triangle s s' (λ a → e {a}) H) + (X : (a : A) → f'' (s' a) ＝ t' (f a)) + (α : (a : A) → G (s a) ∙ (ap h (T a) ∙ F (f a)) ＝ ap f'' (H a) ∙ X a) + where + + opaque + transpose-sq : + (a : A) → + T a ∙ inv-F (f a) ＝ + ap f' (inv-H a) ∙ + ( inv-G (s' a) ∙ + ap inv-h (X a)) + transpose-sq a = + ap + ( T a ∙_) + ( inv (compute-inv-invert-fiberwise-triangle' t t' (λ b → j {b}) F (f a))) ∙ + right-transpose-eq-concat' + ( T a) + ( _) + ( inv-F' (f a)) + ( [g]) + where + [i] : + ap f' (is-retraction-map-inv-equiv e (s a)) ＝ + ( pasting-vertical-coherence-square-maps f' g h f'' inv-g inv-h f' + G inv-G (s a) ∙ + is-retraction-map-inv-equiv j (f' (s a))) + [i] = + inv right-unit ∙ + left-inverse-law-pasting-vertical-coherence-square-maps f' e j f'' G (s a) + [a] : + ap inv-h (G (s a) ∙ (ap h (T a) ∙ F (f a))) ＝ + ap inv-h (ap f'' (H a) ∙ X a) + [a] = ap (ap inv-h) (α a) + [b] : ap inv-h (G (s a)) ∙ + ap inv-h (ap h (T a) ∙ F (f a)) ＝ + ap inv-h (ap f'' (H a) ∙ X a) + [b] = inv (ap-concat inv-h (G (s a)) (ap h (T a) ∙ F (f a))) ∙ [a] + [c] : + ap inv-h (G (s a)) ∙ + ( ap (inv-h ∘ h) (T a) ∙ ap inv-h (F (f a))) ＝ + ap inv-h (ap f'' (H a) ∙ X a) + [c] = + ap + ( ap inv-h (G (s a)) ∙_) + ( ap (_∙ ap inv-h (F (f a))) (ap-comp inv-h h (T a)) ∙ + inv (ap-concat inv-h (ap h (T a)) (F (f a)))) ∙ + [b] + [d] : + pasting-vertical-coherence-square-maps f' g h f'' inv-g inv-h f' G inv-G (s a) ∙ + ( ap (inv-h ∘ h) (T a) ∙ ap inv-h (F (f a))) ＝ + inv-G (g (s a)) ∙ ap inv-h (ap f'' (H a) ∙ X a) + [d] = assoc _ _ _ ∙ ap (inv-G (g (s a)) ∙_) [c] + [f'] : + inv-G (g (s a)) ∙ + ap inv-h (ap f'' (H a)) ＝ + ap f' (ap inv-g (H a)) ∙ + inv-G (s' a) + [f'] = + nat-coherence-square-maps f'' inv-g inv-h f' inv-G (H a) + [e] : + ap f' (is-retraction-map-inv-equiv e (s a)) ＝ + ap f' (ap inv-g (H a)) ∙ + inv-G (s' a) ∙ + ap inv-h (X a) ∙ + ap inv-h (inv (F (f a))) ∙ + inv (ap (inv-h ∘ h) (T a)) ∙ + is-retraction-map-inv-equiv j (f' (s a)) + [e] = + [i] ∙ + ap + ( _∙ is-retraction-map-inv-equiv j (f' (s a))) + ( right-transpose-eq-concat _ _ _ [d] ∙ + ( ( ap + ( _ ∙_) + ( ( distributive-inv-concat + ( ap (inv-h ∘ h) (T a)) + ( ap inv-h (F (f a)))) ∙ + ( ap (_∙ _) (inv (ap-inv inv-h (F (f a))))))) ∙ + ( inv (assoc _ _ _)) ∙ + ( ap + ( λ p → p ∙ _ ∙ _) + ( ap (_ ∙_) (ap-concat inv-h (ap f'' (H a)) (X a)) ∙ + inv (assoc _ _ _) ∙ + ap (_∙ ap inv-h (X a)) [f'])))) + [f] : + inv (ap (inv-h ∘ h) (T a)) ∙ + is-retraction-map-inv-equiv j (f' (s a)) ＝ + is-retraction-map-inv-equiv j (t (f a)) ∙ inv (T a) + [f] = + inv + ( nat-htpy (is-retraction-map-inv-equiv j) (inv (T a)) ∙ + ap (_∙ is-retraction-map-inv-equiv j (f' (s a))) (ap-inv (inv-h ∘ h) (T a))) ∙ + ap + ( is-retraction-map-inv-equiv j (t (f a)) ∙_) + ( ap-id (inv (T a))) + [g] : + T a ＝ + ap f' (inv-H a) ∙ + ( inv-G (s' a) ∙ + ap inv-h (X a)) ∙ + inv-F' (f a) + [g] = + left-transpose-eq-concat _ _ _ + ( inv-right-transpose-eq-concat _ _ _ + ( [e] ∙ + left-whisker-concat-coherence-square-identifications + ( ap f' (ap inv-g (H a)) ∙ inv-G (s' a) ∙ ap inv-h (X a) ∙ ap inv-h (inv (F (f a)))) + ( is-retraction-map-inv-equiv j (t (f a))) + ( inv (ap (inv-h ∘ h) (T a))) + ( inv (T a)) + ( is-retraction-map-inv-equiv j (f' (s a))) + ( [f]))) ∙ + ap + ( _∙ (ap f' (ap inv-g (H a)) ∙ _ ∙ _ ∙ _ ∙ _)) + ( inv (ap-inv f' (is-retraction-map-inv-equiv e (s a)))) ∙ + inv (assoc _ _ _) ∙ + ap + (_∙ is-retraction-map-inv-equiv j (t (f a))) + ( inv (assoc _ _ _)) ∙ + assoc _ _ _ ∙ + ap + ( _∙ inv-F' (f a)) + ( inv (assoc _ _ _) ∙ + ap + ( _∙ ap inv-h (X a)) + ( right-whisker-concat-coherence-triangle-identifications' + ( ap f' (inv-H a)) + ( ap f' (ap inv-g (H a))) + ( ap f' (inv (is-retraction-map-inv-equiv e (s a)))) + ( inv-G (s' a)) + ( inv (ap-concat f' _ _))) ∙ + assoc _ _ _) + +module _ + {l1 l2 l3 l4 l5 l6 l7 l8 : Level} + {P1 : UU l1} {P2 : UU l2} {P3 : UU l3} {P4 : UU l4} + {Q1 : P1 → UU l5} {Q2 : P2 → UU l6} {Q3 : P3 → UU l7} {Q4 : P4 → UU l8} + (g1 : P1 → P3) (f1 : P1 → P2) (f2 : P3 → P4) (g2 : P2 → P4) + (g1' : {p : P1} → Q1 p → Q3 (g1 p)) + (e1' : (p : P1) → Q1 p ≃ Q2 (f1 p)) + (let f1' = λ {p} → map-equiv (e1' p)) + (let inv-f1' = λ {p} → map-inv-equiv (e1' p)) + (e2' : (p : P3) → Q3 p ≃ Q4 (f2 p)) + (let f2' = λ {p} → map-equiv (e2' p)) + (let inv-f2' = λ {p} → map-inv-equiv (e2' p)) + (g2' : {p : P2} → Q2 p → Q4 (g2 p)) + (s1 : (p : P1) → Q1 p) (s2 : (p : P2) → Q2 p) (s3 : (p : P3) → Q3 p) + (s4 : (p : P4) → Q4 p) + (G1 : (p : P1) → g1' (s1 p) ＝ s3 (g1 p)) + (F1 : (p : P1) → f1' (s1 p) ＝ s2 (f1 p)) + (F2 : (p : P3) → f2' (s3 p) ＝ s4 (f2 p)) + (G2 : (p : P2) → g2' (s2 p) ＝ s4 (g2 p)) + (H : coherence-square-maps g1 f1 f2 g2) + (H' : square-over {Q4 = Q4} _ _ _ _ g1' f1' f2' g2' H) + where + + opaque + -- good luck if you ever need to unfold this... + flop-section : + section-square-over {Q4 = Q4} + _ _ _ _ g1' f1' f2' g2' + _ _ _ s4 G1 F1 F2 G2 + H H' → + (p : P1) → + G1 p ∙ invert-fiberwise-triangle s3 (s4 ∘ f2) e2' F2 (g1 p) ＝ + ap g1' (invert-fiberwise-triangle s1 (s2 ∘ f1) e1' F1 p) ∙ + vertical-inv-equiv-coherence-square-maps g1' (e1' p) (e2' (g1 p)) (tr Q4 (H p) ∘ g2') H' (s2 (f1 p)) ∙ + ap (inv-f2' ∘ tr Q4 (H p)) (G2 (f1 p)) ∙ + ap inv-f2' (apd s4 (H p)) + flop-section α p = + [i] p ∙ + left-whisker-concat-coherence-triangle-identifications + ( _) + ( ap inv-f2' (ap (tr Q4 (H p)) (G2 (f1 p)) ∙ apd s4 (H p))) + ( ap inv-f2' (apd s4 (H p))) + ( ap (inv-f2' ∘ tr Q4 (H p)) (G2 (f1 p))) + ( ap-concat inv-f2' _ (apd s4 (H p)) ∙ + ap (_∙ _) (inv (ap-comp inv-f2' (tr Q4 (H p)) (G2 (f1 p))))) + where + [i] : (a : P1) → + G1 a ∙ + invert-fiberwise-triangle s3 (s4 ∘ f2) (λ b → e2' b) F2 (g1 a) + ＝ + ap g1' + (invert-fiberwise-triangle s1 (s2 ∘ f1) (λ a₁ → e1' a₁) F1 a) + ∙ + vertical-inv-equiv-coherence-square-maps g1' (e1' a) (e2' (g1 a)) + (tr Q4 (H a) ∘ g2') H' ((s2 ∘ f1) a) + ∙ + ap (map-inv-equiv (e2' (g1 a))) + (ap (tr Q4 (H a)) (G2 (f1 a)) ∙ apd s4 (H a)) + [i] = + transpose-sq g1 s1 s3 (s2 ∘ f1) (s4 ∘ f2) g1' (λ {a} → tr Q4 (H a) ∘ g2') + ( e1' _) (e2' _) G1 H' F2 F1 + (λ p → ap (tr Q4 (H p)) (G2 (f1 p)) ∙ apd s4 (H p)) + (inv-htpy-assoc-htpy _ _ _ ∙h α ∙h assoc-htpy _ _ _) ∙h + inv-htpy-assoc-htpy _ _ _ +``` + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : B → UU l3} + (f : A → B) (s : (b : B) → C b) + where + + apd-left : + {x y : A} (p : x ＝ y) → + apd (s ∘ f) p ＝ inv (substitution-law-tr C f p) ∙ apd s (ap f p) + apd-left refl = refl + + apd-left' : + {x y : A} (p : x ＝ y) → + substitution-law-tr C f p ∙ apd (s ∘ f) p ＝ apd s (ap f p) + apd-left' refl = refl + +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + (s : (a : A) → B a) (f : {a : A} → B a → C a) + where + + apd-right : + {x y : A} (p : x ＝ y) → + apd (f ∘ s) p ＝ inv (preserves-tr (λ a → f {a}) p (s x)) ∙ ap f (apd s p) + apd-right refl = refl +``` + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + (s : (a : A) → B a) + where + + apd-concat : + {x y z : A} (p : x ＝ y) (q : y ＝ z) → + ap (tr B q) (apd s p) ∙ apd s q ＝ inv (tr-concat p q (s x)) ∙ apd s (p ∙ q) + apd-concat refl q = refl + + apd-concat' : + {x y z : A} (p : x ＝ y) (q : y ＝ z) → + apd s (p ∙ q) ＝ tr-concat p q (s x) ∙ ap (tr B q) (apd s p) ∙ apd s q + apd-concat' refl q = refl +``` + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + (s : (a : A) → B a) + where + + apd-apd : + {x y : A} (p q : x ＝ y) (α : p ＝ q) → + ap (λ r → tr B r (s x)) (inv α) ∙ apd s p ＝ apd s q + apd-apd p q refl = refl + + apd-apd' : + {x y : A} (p q : x ＝ y) (α : p ＝ q) → + apd s p ＝ ap (λ r → tr B r (s x)) α ∙ apd s q + apd-apd' p q refl = refl +``` + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + {f g : (a : A) → B a} (H : f ~ g) + where + + inv-dep-nat-htpy : + {x y : A} (p : x ＝ y) → + apd f p ∙ H y ＝ + ap (tr B p) (H x) ∙ apd g p + inv-dep-nat-htpy {x = x} {y = y} p = + map-inv-compute-dependent-identification-eq-value f g p (H x) (H y) + ( apd H p) +``` + +TODO: this should be parameterized by a fiberwise map, not equivalence + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : sequential-diagram l1} {X : UU l2} + {c : cocone-sequential-diagram A X} + (up-c : universal-property-sequential-colimit c) + {B : sequential-diagram l3} {Y : UU l4} + (c' : cocone-sequential-diagram B Y) + (f : hom-sequential-diagram A B) + (let f∞ = map-sequential-colimit-hom-sequential-diagram up-c c' f) + (let + C = htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c' f) + (P : X → UU l5) + (let P' = descent-data-family-cocone-sequential-diagram c P) + (Q : Y → UU l6) + (let Q' = descent-data-family-cocone-sequential-diagram c' Q) + (e : fam-equiv P (Q ∘ f∞)) + where + + equiv-over-diagram-equiv-over-colimit : + (n : ℕ) (a : family-sequential-diagram A n) → + family-descent-data-sequential-colimit P' n a ≃ + family-descent-data-sequential-colimit Q' n + ( map-hom-sequential-diagram B f n a) + equiv-over-diagram-equiv-over-colimit n a = + equiv-tr Q (C n a) ∘e + e (map-cocone-sequential-diagram c n a) + + map-over-diagram-equiv-over-colimit : + (n : ℕ) (a : family-sequential-diagram A n) → + family-descent-data-sequential-colimit P' n a → + family-descent-data-sequential-colimit Q' n + ( map-hom-sequential-diagram B f n a) + map-over-diagram-equiv-over-colimit n a = + map-equiv (equiv-over-diagram-equiv-over-colimit n a) + + opaque + γ-base' : + (n : ℕ) (a : family-sequential-diagram A n) → + coherence-square-maps + ( tr Q (ap f∞ (coherence-cocone-sequential-diagram c n a))) + ( tr Q (C n a)) + ( tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∘ + ( tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)))) + γ-base' n a q = + inv + ( substitution-law-tr Q + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∙ + inv + ( tr-concat + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)) + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( tr Q (C n a) q)) ∙ + inv + ( tr-concat (C n a) _ q) ∙ + ap + ( λ p → tr Q p q) + ( inv + ( coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c' f n a)) ∙ + tr-concat + ( ap f∞ (coherence-cocone-sequential-diagram c n a)) + ( C (succ-ℕ n) (map-sequential-diagram A n a)) + ( q) + + opaque + γ' : + (n : ℕ) (a : family-sequential-diagram A n) → + coherence-square-maps + ( tr (Q ∘ f∞) (coherence-cocone-sequential-diagram c n a)) + ( tr Q (C n a)) + ( tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∘ + ( tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)))) + γ' n a q = + γ-base' n a q ∙ + ap + ( tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( substitution-law-tr Q f∞ (coherence-cocone-sequential-diagram c n a)) + + opaque + square-over-diagram-square-over-colimit : + (n : ℕ) (a : family-sequential-diagram A n) → + coherence-square-maps + ( tr P (coherence-cocone-sequential-diagram c n a)) + ( map-over-diagram-equiv-over-colimit n a) + ( map-over-diagram-equiv-over-colimit + ( succ-ℕ n) + ( map-sequential-diagram A n a)) + ( ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∘ + ( tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)))) + square-over-diagram-square-over-colimit n a = + pasting-vertical-coherence-square-maps + ( tr P (coherence-cocone-sequential-diagram c n a)) + ( map-fam-equiv e (map-cocone-sequential-diagram c n a)) + ( map-fam-equiv e (map-cocone-sequential-diagram c (succ-ℕ n) (map-sequential-diagram A n a))) + ( tr (Q ∘ f∞) (coherence-cocone-sequential-diagram c n a)) + ( tr Q (C n a)) + ( tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∘ + ( tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)))) + ( inv-htpy + ( preserves-tr + ( map-fam-equiv e) + ( coherence-cocone-sequential-diagram c n a))) + ( γ' n a) + +module _ + {l1 l2 l3 l4 l5 : Level} + {A : sequential-diagram l1} {X : UU l2} + {c : cocone-sequential-diagram A X} + (up-c : universal-property-sequential-colimit c) + {B : sequential-diagram l3} {Y : UU l4} + (c' : cocone-sequential-diagram B Y) + (f : hom-sequential-diagram A B) + (let f∞ = map-sequential-colimit-hom-sequential-diagram up-c c' f) + (Q : Y → UU l5) + where + + opaque + unfolding square-over-diagram-square-over-colimit + + compute-square-over-diagram-id : + (n : ℕ) (a : family-sequential-diagram A n) → + square-over-diagram-square-over-colimit up-c c' f (Q ∘ f∞) Q id-fam-equiv n a ~ + γ' up-c c' f (Q ∘ f∞) Q id-fam-equiv n a + compute-square-over-diagram-id n a q = + ap + ( λ r → + γ' up-c c' f (Q ∘ f∞) Q id-fam-equiv n a q ∙ + ap (tr Q _) (inv r)) + ( compute-preserves-tr-id (coherence-cocone-sequential-diagram c n a) q) ∙ + right-unit +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} + {I : UU l1} {A : I → UU l2} {B : I → UU l3} {C : I → UU l4} + (g : (i : I) → B i → C i) (f : (i : I) → A i → B i) + where + + preserves-tr-comp : + {i j : I} (p : i ＝ j) → + preserves-tr (λ i → g i ∘ f i) p ~ + pasting-horizontal-coherence-square-maps (f i) (g i) (tr A p) (tr B p) (tr C p) (f j) (g j) + ( preserves-tr f p) + ( preserves-tr g p) + preserves-tr-comp refl i = refl + + inv-preserves-tr-comp : + {i j : I} (p : i ＝ j) → + inv-htpy (preserves-tr (λ i → g i ∘ f i) p) ~ + pasting-vertical-coherence-square-maps (tr A p) (f i) (f j) (tr B p) (g i) (g j) (tr C p) + ( inv-htpy (preserves-tr f p)) + ( inv-htpy (preserves-tr g p)) + inv-preserves-tr-comp refl x = refl + +module _ + {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l1} {B : I → UU l2} + (f : (i : I) → A i → B i) + where + + preserves-tr-concat : + {i j : I} (p : i ＝ j) + {k : I} (q : j ＝ k) → + preserves-tr f (p ∙ q) ∙h tr-concat p q ·r f i ~ + f k ·l tr-concat p q ∙h + pasting-vertical-coherence-square-maps (f i) (tr A p) (tr B p) (f j) (tr A q) (tr B q) (f k) + ( preserves-tr f p) + ( preserves-tr f q) + preserves-tr-concat refl q x = refl + + aaa : + {i j : I} (p : i ＝ j) → + pasting-horizontal-coherence-square-maps + ( tr A p) (tr A (inv p)) (f i) (f j) (f i) (tr B p) (tr B (inv p)) + ( inv-htpy (preserves-tr f p)) + ( inv-htpy (preserves-tr f (inv p))) ∙h + f i ·l is-retraction-map-inv-equiv (equiv-tr A p) ~ + is-retraction-map-inv-equiv (equiv-tr B p) ·r f i + aaa refl x = refl + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + (e : A ≃ B) + where + + inv-coherence-map-inv-is-equiv : + (a : A) → + ap (map-equiv e) (inv (is-retraction-map-inv-equiv e a)) ＝ + inv (is-section-map-inv-equiv e (map-equiv e a)) + inv-coherence-map-inv-is-equiv a = + ap-inv (map-equiv e) (is-retraction-map-inv-equiv e a) ∙ + ap inv (inv (coherence-map-inv-equiv e a)) + + left-inv-is-retraction-map-inv-equiv : + (a : A) → + inv (is-section-map-inv-equiv e (map-equiv e a)) ∙ + ap (map-equiv e) (is-retraction-map-inv-equiv e a) ＝ + refl + left-inv-is-retraction-map-inv-equiv a = + ap + ( inv (is-section-map-inv-equiv e (map-equiv e a)) ∙_) + ( inv (coherence-map-inv-equiv e a)) ∙ + left-inv (is-section-map-inv-equiv e (map-equiv e a)) + +opaque + priv-is-section : + {l1 l2 : Level} {A : UU l1} {B : UU l2} + (e : A ≃ B) → map-equiv e ∘ map-inv-equiv e ~ id + priv-is-section = is-section-map-inv-equiv + +module _ + {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : A → UU l2} {C : UU l3} (f : C → A) + {D : C → UU l4} {D' : C → UU l5} + (f' : fam-equiv D D') + (g' : fam-equiv D' (B ∘ f)) + (let + e' : (c : C) → D c → B (f c) + e' c = map-fam-equiv g' c ∘ map-fam-equiv f' c + inv-e' : (c : C) → B (f c) → D c + inv-e' c = map-inv-equiv (g' c ∘e f' c)) + where + open import foundation.dependent-identifications + abstract + + ccc'' : + {x y : C} (p : x ＝ y) + {z : A} (q : z ＝ f y) → + {d : D x} (let b = e' x d) + {b' : B z} (s : tr B (q ∙ ap f (inv p)) b' ＝ b) → + concat-dependent-identification B q (ap f (inv p)) + ( inv (is-section-map-inv-equiv (g' y ∘e f' y) _)) + ( left-whisk-dependent-identification (e' _) (inv p) + ( inv-dependent-identification D p + ( inv + ( ( ap + ( inv-e' _ ∘ tr B q) + ( inv + ( is-retraction-map-inv-equiv (equiv-tr B (q ∙ ap f (inv p))) b') ∙ + ap + ( tr B (inv (q ∙ ap f (inv p)))) + ( s))) ∙ + ( ( ap + ( inv-e' y) + ( ( ap + ( tr B q) + ( ap (λ r → tr B r b) (distributive-inv-concat _ _) ∙ + ( tr-concat _ _ b))) ∙ + ( is-section-map-inv-equiv + ( equiv-tr B q) + ( tr B (inv (ap f (inv p))) b)) ∙ + ap + ( λ r → tr B r b) + ( inv (ap-inv f (inv p)) ∙ ap (ap f) (inv-inv p)) ∙ + substitution-law-tr B f p)) ∙ + ( map-eq-transpose-equiv-inv' + ( g' y ∘e f' y) + ( inv (preserves-tr e' p d)))))))) ＝ + s + ccc'' refl refl {d = d} refl = + ap + ( λ r → + ap id (inv (is-section-map-inv-equiv (g' _ ∘e f' _) (e' _ d))) ∙ + ap (e' _) r) + ( ( inv-inv _) ∙ + ( ap + ( λ r → + ap (inv-e' _) r ∙ is-retraction-map-inv-equiv (g' _ ∘e f' _) _) + ( right-unit ∙ right-unit ∙ coherence-map-inv-equiv id-equiv _))) ∙ + ap + ( _∙ ap (e' _) (is-retraction-map-inv-equiv (g' _ ∘e f' _) d)) + ( ap-id _) ∙ + left-inv-is-retraction-map-inv-equiv (g' _ ∘e f' _) d +``` + +```agda +module _ + {l1 l2 : Level} + {A : UU l1} + {P : A → UU l2} + where + open import foundation.dependent-identifications + + compute-lemma'' : + {x y : A} (p : x ＝ y) → + {x' : P x} {y' z' : P y} + (K : dependent-identification P p x' y') + (H : y' ＝ z') → + inv-dependent-identification P p (K ∙ H) ＝ + ap + ( tr P (inv p)) + ( inv H) ∙ + inv-dependent-identification P p K + compute-lemma'' refl K refl = ap inv right-unit + +module _ + {l1 l2 l5 l6 : Level} + {A : UU l1} {B : UU l2} + {P : A → UU l5} {Q : UU l6} -- {Q : B → UU l6} + where + open import foundation.dependent-identifications + + compute-lemma : + {x y : A} (p : x ＝ y) → + {u v : Q} (H : u ＝ v) → + (f : Q → P y) + {x' : P x} (K : dependent-identification P p x' (f u)) → + inv-dependent-identification P p (K ∙ ap f H) ＝ + ap + ( tr P (inv p) ∘ f) + ( inv H) ∙ + inv-dependent-identification P p K + compute-lemma p H f K = + compute-lemma'' p K (ap f H) ∙ + ap + ( _∙ inv-dependent-identification P p K) + ( ap + ( ap (tr P (inv p))) + ( inv (ap-inv f H)) ∙ + inv (ap-comp (tr P (inv p)) f (inv H))) + + compute-lemma' : + {x y : A} (p : x ＝ y) → + {u v : Q} (H : u ＝ v) → + (f : Q → P y) → + {x' : P x} (K : f v ＝ tr P p x') → + inv-dependent-identification P p (inv (ap f H ∙ K)) ＝ + ap + ( tr P (inv p) ∘ f) + ( H) ∙ + inv-dependent-identification P p (inv K) + compute-lemma' refl refl f K = refl +``` + +```agda + + +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + open import foundation.dependent-identifications + + nat-concat-dependent-identification : + {x y : A} (p : x ＝ y) → + {z : A} (q : y ＝ z) → + (f : B x → B y) → + (H : tr B p ~ f) → + {x' y' : B x} (p' : x' ＝ y') → + concat-dependent-identification B p q (ap (tr B p) p') (ap (tr B q) (H y')) ＝ + concat-dependent-identification B p q (H x') (ap (tr B q) (ap f p')) + nat-concat-dependent-identification refl refl f H refl = inv right-unit + + nat-concat-dependent-identification-id : + {x y : A} (p : x ＝ y) → + {z : A} (q : y ＝ z) → + (f : B y → B y) → + (H : id ~ f) → + {x' : B x} {y' : B y} (p' : dependent-identification B p x' y') → + concat-dependent-identification B p q p' (ap (tr B q) (H y')) ＝ + concat-dependent-identification B p q (H (tr B p x')) (ap (tr B q) (ap f p')) + nat-concat-dependent-identification-id refl q f H refl = inv right-unit + +open import synthetic-homotopy-theory.zigzags-sequential-diagrams +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : sequential-diagram l1} {X : UU l2} + {c : cocone-sequential-diagram A X} + (up-c : universal-property-sequential-colimit c) + {B : sequential-diagram l3} {Y : UU l4} + (c' : cocone-sequential-diagram B Y) + (z : zigzag-sequential-diagram A B) + (let f = hom-diagram-zigzag-sequential-diagram z) + (let f∞ = map-sequential-colimit-hom-sequential-diagram up-c c' f) + (let + C = htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c' f) + (P : X → UU l5) + (let P' = descent-data-family-cocone-sequential-diagram c P) + (Q : Y → UU l6) + (let Q' = descent-data-family-cocone-sequential-diagram c' Q) + (e : fam-equiv P (Q ∘ f∞)) + where + + inv-map-over-diagram-equiv-zigzag' : + (n : ℕ) (a : family-sequential-diagram A n) → + family-descent-data-sequential-colimit Q' n + ( map-zigzag-sequential-diagram z n a) → + family-descent-data-sequential-colimit P' n a + inv-map-over-diagram-equiv-zigzag' n a = + map-inv-equiv + ( equiv-over-diagram-equiv-over-colimit up-c c' f P Q e n a) + + inv-map-over-diagram-equiv-zigzag : + (n : ℕ) (b : family-sequential-diagram B n) → + family-descent-data-sequential-colimit Q' n b → + family-descent-data-sequential-colimit P' (succ-ℕ n) + ( inv-map-zigzag-sequential-diagram z n b) + inv-map-over-diagram-equiv-zigzag n b = + inv-map-over-diagram-equiv-zigzag' (succ-ℕ n) + ( inv-map-zigzag-sequential-diagram z n b) ∘ + tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( lower-triangle-zigzag-sequential-diagram z n b) ∘ + tr Q + ( coherence-cocone-sequential-diagram c' n b) + + opaque + internal-triangle-upper-triangle-over' : + (n : ℕ) (a : family-sequential-diagram A n) → + tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a)) ∘ + tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( inv (naturality-map-hom-diagram-zigzag-sequential-diagram z n a)) ~ + tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( ap + ( map-zigzag-sequential-diagram z (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n a)) + internal-triangle-upper-triangle-over' n a p = + ap + ( tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( lower-triangle-zigzag-sequential-diagram z n + ( map-zigzag-sequential-diagram z n a))) + ( ( ap + ( λ r → tr (family-descent-data-sequential-colimit Q' (succ-ℕ n)) r p) + ( distributive-inv-concat _ _)) ∙ + ( tr-concat _ _ p)) ∙ + is-section-map-inv-equiv + ( equiv-tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a))) + ( _) ∙ + ap + ( λ r → + tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( r) + ( p)) + ( ( inv + ( ap-inv + ( map-zigzag-sequential-diagram z (succ-ℕ n)) + ( inv (upper-triangle-zigzag-sequential-diagram z n a)))) ∙ + ( ap (ap (map-zigzag-sequential-diagram z (succ-ℕ n))) (inv-inv _))) + + inv-upper-triangle-over' : + (n : ℕ) (a : family-sequential-diagram A n) → + tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a)) ∘ + tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( inv (naturality-map-hom-diagram-zigzag-sequential-diagram z n a)) ∘ + map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) (map-sequential-diagram A n a) ~ + map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) (inv-map-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a)) ∘ + tr + ( family-descent-data-sequential-colimit P' (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n a) + inv-upper-triangle-over' n a p = + internal-triangle-upper-triangle-over' n a + ( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) (map-sequential-diagram A n a) p) ∙ + -- left-whisk-dependent-identification + -- ( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) _) + -- ( upper-triangle-zigzag-sequential-diagram z n a) + -- ( refl) + substitution-law-tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( map-zigzag-sequential-diagram z (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n a) ∙ + inv + ( preserves-tr + ( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n a) + ( p)) + + opaque + inv-transport-squares : + (n : ℕ) (a : family-sequential-diagram A n) → + coherence-square-maps + ( tr + ( family-descent-data-sequential-colimit P' (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n a)) + ( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) + ( map-sequential-diagram A n a)) + ( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) + ( inv-map-zigzag-sequential-diagram z n + ( map-zigzag-sequential-diagram z n a))) + ( tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n) ∘ + map-zigzag-sequential-diagram z (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n a)) + inv-transport-squares n a = + inv-htpy + ( preserves-tr + ( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n a)) + + opaque + transpose-squares : + (n : ℕ) (a : family-sequential-diagram A n) → + inv-map-over-diagram-equiv-zigzag' (succ-ℕ n) + ( inv-map-zigzag-sequential-diagram z n + ( map-zigzag-sequential-diagram z n a)) ∘ + tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n) ∘ + map-zigzag-sequential-diagram z (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n a) ∘ + map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) + ( map-sequential-diagram A n a) ~ + tr + ( family-descent-data-sequential-colimit P' (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n a) + transpose-squares n a p = + map-eq-transpose-equiv-inv' + ( equiv-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) _) + ( inv-transport-squares n a p) + + + opaque + upper-triangle-over' : + (n : ℕ) (a : family-sequential-diagram A n) → + inv-map-over-diagram-equiv-zigzag' (succ-ℕ n) _ ∘ + tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a)) ∘ + tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( inv (naturality-map-hom-diagram-zigzag-sequential-diagram z n a)) ∘ + map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) (map-sequential-diagram A n a) ~ + tr + ( family-descent-data-sequential-colimit P' (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n a) + upper-triangle-over' n a p = + ap + ( inv-map-over-diagram-equiv-zigzag' (succ-ℕ n) _) + ( internal-triangle-upper-triangle-over' n a + ( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) (map-sequential-diagram A n a) p) ∙ + substitution-law-tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( map-zigzag-sequential-diagram z (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n a)) ∙ + transpose-squares n a p + + inv-upper-triangle-over : + (n : ℕ) (a : family-sequential-diagram A n) → + coherence-square-maps + ( map-family-descent-data-sequential-colimit P' n a) + ( map-over-diagram-equiv-over-colimit up-c c' f P Q e n a) + ( tr + ( family-descent-data-sequential-colimit P' (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n a)) + ( inv-map-over-diagram-equiv-zigzag n (map-zigzag-sequential-diagram z n a)) + inv-upper-triangle-over n a p = + ap + ( inv-map-over-diagram-equiv-zigzag' (succ-ℕ n) _ ∘ + tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a))) + ( inv + ( is-retraction-map-inv-equiv + ( equiv-tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( naturality-map-hom-diagram-zigzag-sequential-diagram z n a)) + ( _)) ∙ + ap + ( tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( inv + ( naturality-map-hom-diagram-zigzag-sequential-diagram z n a))) + ( square-over-diagram-square-over-colimit up-c c' f P Q e n a p)) ∙ + upper-triangle-over' n a (map-family-descent-data-sequential-colimit P' n a p) + + upper-triangle-over : + (n : ℕ) → + htpy-over + ( family-descent-data-sequential-colimit P' (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n) + ( map-family-descent-data-sequential-colimit P' n _) + ( inv-map-over-diagram-equiv-zigzag n _ ∘ + map-over-diagram-equiv-over-colimit up-c c' f P Q e n _) + upper-triangle-over n {a} p = + inv (inv-upper-triangle-over n a p) + + opaque + lower-triangle-over' : + (n : ℕ) (a : family-sequential-diagram A n) + (q : + family-descent-data-sequential-colimit Q' n + ( map-zigzag-sequential-diagram z n a)) → + q ＝ + map-over-diagram-equiv-over-colimit up-c c' f P Q e n a + ( inv-map-over-diagram-equiv-zigzag' n a q) + lower-triangle-over' n a q = + inv + ( is-section-map-inv-equiv + ( equiv-over-diagram-equiv-over-colimit up-c c' f P Q e n a) + ( q)) + + lower-triangle-over : + (n : ℕ) → + htpy-over + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( lower-triangle-zigzag-sequential-diagram z n) + ( map-family-descent-data-sequential-colimit Q' n _) + ( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) _ ∘ + inv-map-over-diagram-equiv-zigzag n _) + lower-triangle-over n {b} q = + lower-triangle-over' + ( succ-ℕ n) + ( inv-map-zigzag-sequential-diagram z n b) + ( tr + ( family-descent-data-sequential-colimit Q' (succ-ℕ n)) + ( lower-triangle-zigzag-sequential-diagram z n b) + ( map-family-descent-data-sequential-colimit Q' n b q)) + + opaque + unfolding + lower-triangle-over' upper-triangle-over' + internal-triangle-upper-triangle-over' transpose-squares + inv-transport-squares + compute-square-over-zigzag-square-over-colimit : + (n : ℕ) (a : family-sequential-diagram A n) → + pasting-triangles-over + ( map-sequential-diagram A n) + ( map-hom-sequential-diagram B f n) + ( map-hom-sequential-diagram B f (succ-ℕ n)) + ( map-sequential-diagram B n) + ( map-family-descent-data-sequential-colimit P' n _) + ( map-over-diagram-equiv-over-colimit up-c c' f P Q e n _) + ( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) _) + ( map-family-descent-data-sequential-colimit Q' n _) + ( inv-map-zigzag-sequential-diagram z n) + ( inv-map-over-diagram-equiv-zigzag n _) + ( inv-htpy (upper-triangle-zigzag-sequential-diagram z n)) + ( lower-triangle-zigzag-sequential-diagram z n) + ( inv-htpy-over + ( family-descent-data-sequential-colimit P' (succ-ℕ n)) + ( upper-triangle-zigzag-sequential-diagram z n) + _ _ + ( upper-triangle-over n)) + ( lower-triangle-over n) + { a} ~ + square-over-diagram-square-over-colimit up-c c' f P Q e n a + compute-square-over-zigzag-square-over-colimit n a p = + ccc'' + ( map-zigzag-sequential-diagram z (succ-ℕ n)) + ( λ a → e (map-cocone-sequential-diagram c (succ-ℕ n) a)) + ( λ a → equiv-tr Q (C (succ-ℕ n) a)) + ( upper-triangle-zigzag-sequential-diagram z n a) + ( lower-triangle-zigzag-sequential-diagram z n + ( map-zigzag-sequential-diagram z n a)) + ( square-over-diagram-square-over-colimit up-c c' f P Q e n a p) +``` + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {A : sequential-diagram l1} {X : UU l2} + {c : cocone-sequential-diagram A X} + (up-c : universal-property-sequential-colimit c) + {B : sequential-diagram l3} {Y : UU l4} + {c' : cocone-sequential-diagram B Y} + (up-c' : universal-property-sequential-colimit c') + (let + dup-c' = + dependent-universal-property-universal-property-sequential-colimit _ up-c') + (Q : Y → UU l5) + (let Q' = descent-data-family-cocone-sequential-diagram c' Q) + (f : hom-sequential-diagram A B) + (let f∞ = map-sequential-colimit-hom-sequential-diagram up-c c' f) + (let P = Q ∘ f∞) + (let P' = descent-data-family-cocone-sequential-diagram c P) + (let C = htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c' f) + (let f∞n = λ n a → tr Q (C n a)) + (s : section-descent-data-sequential-colimit Q') + (let s∞ = sect-family-sect-dd-sequential-colimit up-c' Q s) + (let + 𝒞 = + htpy-dependent-cocone-dependent-universal-property-sequential-colimit + ( dup-c') + ( s)) + (let C' = htpy-htpy-dependent-cocone-sequential-diagram Q 𝒞) + where + + opaque + unfolding square-over-diagram-square-over-colimit + γ : + (n : ℕ) (a : family-sequential-diagram A n) → + coherence-square-maps + ( tr (Q ∘ f∞) (coherence-cocone-sequential-diagram c n a)) + ( f∞n n a) + ( f∞n (succ-ℕ n) (map-sequential-diagram A n a)) + ( ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∘ + ( tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)))) + γ = γ' up-c c' f P Q id-fam-equiv + + -- compute-γ : + -- (n : ℕ) (a : family-sequential-diagram A n) → + -- square-over-diagram-square-over-colimit up-c c' f (Q ∘ f∞) Q id-fam-equiv n a ~ γ n a + -- compute-γ n a p = + -- ap + -- ( γ n a p ∙_) + -- ( ap + -- ( λ r → ap (tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) (inv r)) + -- ( compute-preserves-tr-id (coherence-cocone-sequential-diagram c n a) p)) ∙ + -- right-unit + + opaque + γ-flip : + (n : ℕ) (a : family-sequential-diagram A n) → + coherence-square-maps + ( ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∘ + ( tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)))) + ( tr Q (inv (C n a))) + ( tr Q (inv (C (succ-ℕ n) (map-sequential-diagram A n a)))) + ( tr (Q ∘ f∞) (coherence-cocone-sequential-diagram c n a)) + γ-flip n a = + vertical-inv-equiv-coherence-square-maps + ( tr (Q ∘ f∞) (coherence-cocone-sequential-diagram c n a)) + ( equiv-tr Q (C n a)) + ( equiv-tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∘ + ( tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)))) + ( γ n a) + + comp-over-diagram : + section-descent-data-sequential-colimit + ( descent-data-family-cocone-sequential-diagram c (Q ∘ f∞)) + pr1 comp-over-diagram n = + tr Q (inv (C n _)) ∘ + map-section-dependent-sequential-diagram _ _ s n ∘ + map-hom-sequential-diagram B f n + pr2 comp-over-diagram n a = + ( γ-flip n a + ( map-section-dependent-sequential-diagram _ _ s n + ( map-hom-sequential-diagram B f n a))) ∙ + ( ap + ( tr Q (inv (C (succ-ℕ n) (map-sequential-diagram A n a)))) + ( ( ap + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( naturality-map-section-dependent-sequential-diagram _ _ s n + ( map-hom-sequential-diagram B f n a))) ∙ + ( apd + ( map-section-dependent-sequential-diagram _ _ s (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)))) + + lemma-1-1 : + htpy-section-dependent-sequential-diagram + ( section-descent-data-section-family-cocone-sequential-colimit c P + ( sect-family-sect-dd-sequential-colimit up-c P comp-over-diagram)) + ( comp-over-diagram) + lemma-1-1 = + htpy-dependent-cocone-dependent-universal-property-sequential-colimit + ( dependent-universal-property-universal-property-sequential-colimit _ up-c) + ( comp-over-diagram) + + -- needs work + lemma-1-2 : + htpy-section-dependent-sequential-diagram + ( section-descent-data-section-family-cocone-sequential-colimit c P + ( s∞ ∘ f∞)) + ( comp-over-diagram) + pr1 lemma-1-2 n = + invert-fiberwise-triangle + ( s∞ ∘ f∞ ∘ map-cocone-sequential-diagram c n) + ( map-section-dependent-sequential-diagram _ _ s n ∘ map-hom-sequential-diagram B f n) + ( λ a → equiv-tr Q (C n a)) + ( λ a → apd s∞ (C n a) ∙ C' n (map-hom-sequential-diagram B f n a)) + pr2 lemma-1-2 n = [i] + where + goal = + (pr2 + (section-descent-data-section-family-cocone-sequential-colimit c P + (s∞ ∘ f∞)) + n + ∙h + invert-fiberwise-triangle + (s∞ ∘ f∞ ∘ pr1 c (succ-ℕ n)) + (pr1 s (succ-ℕ n) ∘ pr1 f (succ-ℕ n)) + (λ a₁ → + equiv-tr Q + (C (succ-ℕ n) a₁)) + (λ a₁ → + apd s∞ (C (succ-ℕ n) a₁) ∙ + C' (succ-ℕ n) (pr1 f (succ-ℕ n) a₁)) + ·r pr2 A n) + ~ + ((λ {v} v₁ → + pr2 (dependent-sequential-diagram-descent-data P') n v v₁) ·l + invert-fiberwise-triangle + (s∞ ∘ f∞ ∘ pr1 c n) + (pr1 s n ∘ pr1 f n) + (λ a₁ → + equiv-tr Q + (C n a₁)) + (λ a₁ → + apd s∞ + (C n a₁) ∙ + C' n (pr1 f n a₁)) + ∙h + (λ a₁ → + γ-flip n a₁ (pr1 s n (pr1 f n a₁)) ∙ + ap + (tr Q + (inv + (C (succ-ℕ n) (pr2 A n a₁)))) + (ap (tr (Q ∘ pr1 c' (succ-ℕ n)) (pr2 f n a₁)) + (pr2 s n (pr1 f n a₁)) + ∙ apd (pr1 s (succ-ℕ n)) (pr2 f n a₁)))) + + opaque + [step-1] : + (a : family-sequential-diagram A n) → + ap + ( tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( substitution-law-tr Q f∞ (coherence-cocone-sequential-diagram c n a)) ∙ + ap + ( tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( apd (s∞ ∘ f∞) (coherence-cocone-sequential-diagram c n a)) ＝ + ap + ( tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( apd s∞ (ap f∞ (coherence-cocone-sequential-diagram c n a))) + [step-1] a = + inv + ( ap-concat + ( tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( substitution-law-tr Q f∞ (coherence-cocone-sequential-diagram c n a)) + ( apd (s∞ ∘ f∞) (coherence-cocone-sequential-diagram c n a))) ∙ + ap + ( ap (tr Q (C (succ-ℕ n) (map-sequential-diagram A n a)))) + ( apd-left' f∞ s∞ (coherence-cocone-sequential-diagram c n a)) + [step-2] : + (a : family-sequential-diagram A n) → + tr-concat + ( ap f∞ (coherence-cocone-sequential-diagram c n a)) + ( C (succ-ℕ n) (map-sequential-diagram A n a)) + ( s∞ (f∞ (map-cocone-sequential-diagram c n a))) ∙ + ap + ( tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( apd s∞ (ap f∞ (coherence-cocone-sequential-diagram c n a))) ∙ + apd s∞ (C (succ-ℕ n) (map-sequential-diagram A n a)) ＝ + apd s∞ + ( ap f∞ (coherence-cocone-sequential-diagram c n a) ∙ + C (succ-ℕ n) (map-sequential-diagram A n a)) + [step-2] a = + inv + ( apd-concat' s∞ + ( ap f∞ (coherence-cocone-sequential-diagram c n a)) + ( C (succ-ℕ n) (map-sequential-diagram A n a))) + [step-3] : + (a : family-sequential-diagram A n) → + ap + ( λ p → tr Q p (s∞ (f∞ (map-cocone-sequential-diagram c n a)))) + ( inv + ( coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c' f n a)) ∙ + apd s∞ + ( ap f∞ (coherence-cocone-sequential-diagram c n a) ∙ + C (succ-ℕ n) (map-sequential-diagram A n a)) ＝ + apd s∞ + ( C n a ∙ + ( ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)) ∙ + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)))) + [step-3] a = + apd-apd s∞ _ _ + ( coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c' f n a) + [step-4] : + (a : family-sequential-diagram A n) → + inv + ( tr-concat (C n a) _ (s∞ (f∞ (map-cocone-sequential-diagram c n a)))) ∙ + apd s∞ + ( C n a ∙ + ( ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)) ∙ + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)))) ＝ + ap + ( tr Q (coherence-cocone-sequential-diagram c' n (map-hom-sequential-diagram B f n a) ∙ ap (map-cocone-sequential-diagram c' (succ-ℕ n)) (naturality-map-hom-sequential-diagram B f n a))) + ( apd s∞ (C n a)) ∙ + apd s∞ (coherence-cocone-sequential-diagram c' n (map-hom-sequential-diagram B f n a) ∙ ap (map-cocone-sequential-diagram c' (succ-ℕ n)) (naturality-map-hom-sequential-diagram B f n a)) + [step-4] a = + inv + ( apd-concat s∞ + ( C n a) + ( _)) + [step-5] : + (a : family-sequential-diagram A n) → + inv + ( tr-concat + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)) + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( tr Q (C n a) (s∞ (f∞ (map-cocone-sequential-diagram c n a))))) ∙ + ap + ( tr Q (coherence-cocone-sequential-diagram c' n (map-hom-sequential-diagram B f n a) ∙ ap (map-cocone-sequential-diagram c' (succ-ℕ n)) (naturality-map-hom-sequential-diagram B f n a))) + ( apd s∞ (C n a)) ＝ + ap + ( tr Q + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∘ + tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + ( apd s∞ (C n a)) ∙ + inv + ( tr-concat + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)) + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( s∞ (map-cocone-sequential-diagram c' n (map-hom-sequential-diagram B f n a)))) + [step-5] a = + nat-htpy + ( inv-htpy + ( tr-concat + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)) + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)))) + ( apd s∞ (C n a)) + [step-6] : + (a : family-sequential-diagram A n) → + inv + ( tr-concat + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)) + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( s∞ (map-cocone-sequential-diagram c' n (map-hom-sequential-diagram B f n a)))) ∙ + apd s∞ + ( ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a)) ∙ + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a))) ＝ + ap + ( tr Q + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a))) + ( apd s∞ + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) ∙ + apd s∞ + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + [step-6] a = inv (apd-concat s∞ _ _) + [step-7] : + (a : family-sequential-diagram A n) → + inv + ( substitution-law-tr Q + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∙ + ap + ( tr Q + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∘ + tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + ( apd s∞ (C n a)) ＝ + ap + ( tr (Q ∘ pr1 c' (succ-ℕ n)) (pr2 f n a) ∘ + tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + ( apd s∞ (C n a)) ∙ + inv + ( substitution-law-tr Q + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + [step-7] a = + nat-htpy + ( inv-htpy + ( λ q → + substitution-law-tr Q + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a) + )) + ( apd s∞ (C n a)) + [step-8] : + (a : family-sequential-diagram A n) → + inv + ( substitution-law-tr Q + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∙ + ap + ( tr Q + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a))) + ( apd s∞ + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) ＝ + ap + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( apd s∞ + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) ∙ + inv + ( substitution-law-tr Q + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + [step-8] a = + nat-htpy + ( inv-htpy + ( λ _ → + substitution-law-tr Q + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a))) + ( apd s∞ + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + [step-9] : + (a : family-sequential-diagram A n) → + inv + ( substitution-law-tr Q + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ∙ + apd s∞ + ( ap + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) ＝ + apd + ( s∞ ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a) + [step-9] a = + inv + ( apd-left + ( map-cocone-sequential-diagram c' (succ-ℕ n)) + ( s∞) + ( naturality-map-hom-sequential-diagram B f n a)) + [step-10] : + (a : family-sequential-diagram A n) → + apd + ( s∞ ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a) ∙ + C' + ( succ-ℕ n) + ( map-hom-sequential-diagram B f + ( succ-ℕ n) + ( map-sequential-diagram A n a)) ＝ + ap + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( C' + ( succ-ℕ n) + ( map-sequential-diagram B n + ( map-hom-sequential-diagram B f n a))) ∙ + apd + ( map-section-dependent-sequential-diagram _ _ s (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a) + [step-10] a = + inv-dep-nat-htpy + ( C' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a) + [step-11] : + (a : family-sequential-diagram A n) → + ap + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( apd s∞ + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) ∙ + ap + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( C' + ( succ-ℕ n) + ( map-sequential-diagram B n + ( map-hom-sequential-diagram B f n a))) ＝ + ap + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( ap + ( tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + ( C' n (map-hom-sequential-diagram B f n a)) ∙ + naturality-map-section-dependent-sequential-diagram _ _ s n + ( map-hom-sequential-diagram B f n a)) + [step-11] a = + inv + ( ap-concat + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( apd s∞ + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + ( C' + ( succ-ℕ n) + ( map-sequential-diagram B n + ( map-hom-sequential-diagram B f n a)))) ∙ + ap + ( ap + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a))) + ( pr2 𝒞 n (map-hom-sequential-diagram B f n a)) + [step-12] : + (a : family-sequential-diagram A n) → + ap + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a) ∘ + tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + ( apd s∞ (C n a)) ∙ + ap + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( ap + ( tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + ( C' n (map-hom-sequential-diagram B f n a)) ∙ + naturality-map-section-dependent-sequential-diagram _ _ s n + ( map-hom-sequential-diagram B f n a)) ＝ + ap + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a) ∘ + tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + ( apd s∞ (C n a) ∙ + C' n (map-hom-sequential-diagram B f n a)) ∙ + ap + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( naturality-map-section-dependent-sequential-diagram _ _ s n + ( map-hom-sequential-diagram B f n a)) + open import foundation.whiskering-identifications-concatenation + [step-12] a = + left-whisker-concat-coherence-triangle-identifications + ( ap _ (apd s∞ (C n a))) + _ _ _ + ( ap-concat + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( ap + ( tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + ( C' n (map-hom-sequential-diagram B f n a))) + ( naturality-map-section-dependent-sequential-diagram _ _ s n + ( map-hom-sequential-diagram B f n a)) ∙ + right-whisker-concat + ( inv + ( ap-comp + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + ( C' n (map-hom-sequential-diagram B f n a)))) + ( _)) ∙ + right-whisker-concat + ( inv + (ap-concat + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a) ∘ + tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + ( apd s∞ (C n a)) + ( C' n (map-hom-sequential-diagram B f n a)))) + ( _) + + opaque + unfolding γ γ' γ-base' γ-flip + + [i] : goal + [i] = + transpose-sq + ( map-sequential-diagram A n) + ( s∞ ∘ f∞ ∘ map-cocone-sequential-diagram c n) + ( s∞ ∘ f∞ ∘ map-cocone-sequential-diagram c (succ-ℕ n)) + ( map-section-dependent-sequential-diagram _ _ s n ∘ map-hom-sequential-diagram B f n) + ( map-section-dependent-sequential-diagram _ _ s (succ-ℕ n) ∘ map-hom-sequential-diagram B f (succ-ℕ n)) + ( λ q → tr (Q ∘ f∞) (coherence-cocone-sequential-diagram c n _) q) + ( ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n _)) ∘ + ( tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n _)))) + ( λ {a} → equiv-tr Q (C n a)) + ( λ {a} → equiv-tr Q (C (succ-ℕ n) a)) + ( λ a → apd (s∞ ∘ f∞) (coherence-cocone-sequential-diagram c n a)) + ( γ n _) + ( λ a → apd s∞ (C (succ-ℕ n) a) ∙ C' (succ-ℕ n) (map-hom-sequential-diagram B f (succ-ℕ n) a)) + ( λ a → apd s∞ (C n a) ∙ C' n (map-hom-sequential-diagram B f n a)) + ( λ a → + ap + ( tr (Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) (naturality-map-hom-sequential-diagram B f n a)) + ( naturality-map-section-dependent-sequential-diagram _ _ s n (map-hom-sequential-diagram B f n a)) ∙ + apd (map-section-dependent-sequential-diagram _ _ s (succ-ℕ n)) (naturality-map-hom-sequential-diagram B f n a)) + ( λ a → + ( left-whisker-concat + ( γ n a (s∞ (f∞ (map-cocone-sequential-diagram c n a)))) + ( inv (assoc _ _ _))) ∙ + ( inv (assoc _ _ _)) ∙ + ( right-whisker-concat + ( ( right-whisker-concat-coherence-triangle-identifications' _ _ _ + ( apd s∞ (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( assoc _ _ _ ∙ + left-whisker-concat + ( γ-base' up-c c' f (Q ∘ f∞) Q id-fam-equiv n a (s∞ (f∞ (map-cocone-sequential-diagram c n a)))) + ( [step-1] a) ∙ + assoc _ _ _)) ∙ + ( assoc _ _ _) ∙ + ( left-whisker-concat + ( _) + ( [step-2] a)) ∙ + ( left-whisker-concat-coherence-triangle-identifications' _ _ _ _ + ( [step-3] a)) ∙ + ( left-whisker-concat-coherence-triangle-identifications' _ _ _ _ + ( [step-4] a)) ∙ + ( left-whisker-concat-coherence-triangle-identifications' _ _ _ _ + ( ( right-whisker-concat-coherence-triangle-identifications' _ _ _ + ( apd s∞ _) + ( [step-5] a)) ∙ + ( ( left-whisker-concat-coherence-triangle-identifications' _ _ _ _ + ( [step-6] a)))) ∙ + ( right-whisker-concat-coherence-square-identifications _ _ _ _ + ( [step-7] a) + ( _)) ∙ + ( left-whisker-concat _ + ( ( right-whisker-concat-coherence-square-identifications _ _ _ _ + ( [step-8] a) + ( _)) ∙ + ( left-whisker-concat _ + ( [step-9] a)))))) + ( C' + ( succ-ℕ n) + ( map-hom-sequential-diagram B f (succ-ℕ n) + ( map-sequential-diagram A n a)))) ∙ + ( assoc _ _ _) ∙ + ( left-whisker-concat-coherence-triangle-identifications + ( ap + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a) ∘ + tr Q + ( coherence-cocone-sequential-diagram c' n + ( map-hom-sequential-diagram B f n a))) + ( apd s∞ (C n a))) + _ _ _ + ( ( left-whisker-concat-coherence-square-identifications _ _ _ _ _ + ( [step-10] a)) ∙ + ( right-whisker-concat + ( [step-11] a) + ( _)))) ∙ + ( right-whisker-concat + ( [step-12] a) + ( apd + ( map-section-dependent-sequential-diagram _ _ s (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a))) ∙ + ( assoc _ _ _)) + + lemma-1 : + s∞ ∘ f∞ ~ sect-family-sect-dd-sequential-colimit up-c P comp-over-diagram + lemma-1 = + htpy-htpy-section-out-of-sequential-colimit up-c P _ _ + ( concat-htpy-dependent-cocone-sequential-diagram P + ( lemma-1-2) + ( inv-htpy-dependent-cocone-sequential-diagram P lemma-1-1)) + + module _ + (t : section-descent-data-sequential-colimit P') + (let t∞ = sect-family-sect-dd-sequential-colimit up-c P t) + (F : + (n : ℕ) (a : family-sequential-diagram A n) → + f∞n n a (map-section-dependent-sequential-diagram _ _ t n a) ＝ + map-section-dependent-sequential-diagram _ _ s n + ( map-hom-sequential-diagram B f n a)) + (cubes : + (n : ℕ) → + section-square-over + ( map-sequential-diagram A n) + ( map-hom-sequential-diagram B f n) + ( map-hom-sequential-diagram B f (succ-ℕ n)) + ( map-sequential-diagram B n) + ( λ {a} → tr (Q ∘ f∞) (coherence-cocone-sequential-diagram c n a)) + ( λ {a} → f∞n n a) + ( λ {a} → f∞n (succ-ℕ n) a) + ( λ {b} → tr Q (coherence-cocone-sequential-diagram c' n b)) + ( map-section-dependent-sequential-diagram _ _ t n) + ( map-section-dependent-sequential-diagram _ _ s n) + ( map-section-dependent-sequential-diagram _ _ t (succ-ℕ n)) + ( map-section-dependent-sequential-diagram _ _ s (succ-ℕ n)) + ( naturality-map-section-dependent-sequential-diagram _ _ t n) + ( F n) + ( F (succ-ℕ n)) + ( naturality-map-section-dependent-sequential-diagram _ _ s n) + ( naturality-map-hom-sequential-diagram B f n) + ( λ {a} → γ n a)) + where + + opaque + unfolding γ-flip + + lemma-2 : htpy-section-dependent-sequential-diagram t comp-over-diagram + pr1 lemma-2 n = + invert-fiberwise-triangle + ( map-section-dependent-sequential-diagram _ _ t n) + ( map-section-dependent-sequential-diagram _ _ s n ∘ map-hom-sequential-diagram B f n) + ( λ a → equiv-tr Q (C n a)) + ( F n) + pr2 lemma-2 n a = + flop-section + ( map-sequential-diagram A n) + ( map-hom-sequential-diagram B f n) + ( map-hom-sequential-diagram B f (succ-ℕ n)) + ( map-sequential-diagram B n) + ( λ {a} → tr (Q ∘ f∞) (coherence-cocone-sequential-diagram c n a)) + ( λ a → equiv-tr Q (C n a)) + ( λ a → equiv-tr Q (C (succ-ℕ n) a)) + ( λ {b} → tr Q (coherence-cocone-sequential-diagram c' n b)) + ( map-section-dependent-sequential-diagram _ _ t n) + ( map-section-dependent-sequential-diagram _ _ s n) + ( map-section-dependent-sequential-diagram _ _ t (succ-ℕ n)) + ( map-section-dependent-sequential-diagram _ _ s (succ-ℕ n)) + ( naturality-map-section-dependent-sequential-diagram _ _ t n) + ( F n) + ( F (succ-ℕ n)) + ( naturality-map-section-dependent-sequential-diagram _ _ s n) + ( naturality-map-hom-sequential-diagram B f n) + ( λ {a} → γ n a) + ( cubes n) + ( a) ∙ + assoc _ _ _ ∙ + ap + ( ap + ( tr P (coherence-cocone-sequential-diagram c n a)) + ( pr1 lemma-2 n a) ∙ + γ-flip n a (map-section-dependent-sequential-diagram _ _ s n (map-hom-sequential-diagram B f n a)) ∙_) + ( ( ap + ( _∙ + ap + ( tr Q (inv (C (succ-ℕ n) (map-sequential-diagram A n a)))) + ( apd + ( map-section-dependent-sequential-diagram _ _ s (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a))) + ( ap-comp + ( tr Q (inv (C (succ-ℕ n) (map-sequential-diagram A n a)))) + ( tr + ( Q ∘ map-cocone-sequential-diagram c' (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n a)) + ( naturality-map-section-dependent-sequential-diagram _ _ s n + ( map-hom-sequential-diagram B f n a)))) ∙ + inv + ( ( ap-concat + ( tr Q (inv (C (succ-ℕ n) (map-sequential-diagram A n a)))) + ( _) + ( _)))) ∙ + assoc _ _ _ + + theorem : t∞ ~ s∞ ∘ f∞ + theorem = + htpy-colimit-htpy-diagram-section up-c P t comp-over-diagram lemma-2 ∙h + inv-htpy lemma-1 +``` + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {A : sequential-diagram l1} {X : UU l2} + {c : cocone-sequential-diagram A X} + (up-c : universal-property-sequential-colimit c) + {B : sequential-diagram l3} {Y : UU l4} + {c' : cocone-sequential-diagram B Y} + (up-c' : universal-property-sequential-colimit c') + (f : hom-sequential-diagram A B) + (let f∞ = map-sequential-colimit-hom-sequential-diagram up-c c' f) + (Q : Y → UU l5) + (let Q' = descent-data-family-cocone-sequential-diagram c (Q ∘ f∞)) + where + + comp-over-diagram' : + -- For now restricted to l5 + (P : X → UU l5) + (let P' = descent-data-family-cocone-sequential-diagram c P) + (e' : fam-equiv P (Q ∘ f∞)) + (s : section-descent-data-sequential-colimit P') + (let s∞ = sect-family-sect-dd-sequential-colimit up-c P s) → + section-descent-data-sequential-colimit Q' + pr1 (comp-over-diagram' P e' s) n a = + map-fam-equiv e' + ( map-cocone-sequential-diagram c n a) + ( map-section-dependent-sequential-diagram _ _ s n a) + pr2 (comp-over-diagram' P e' s) n a = + inv + ( preserves-tr + ( map-fam-equiv e') + ( coherence-cocone-sequential-diagram c n a) + ( map-section-dependent-sequential-diagram _ _ s n a)) ∙ + ap + ( map-fam-equiv e' + ( map-cocone-sequential-diagram c (succ-ℕ n) + ( map-sequential-diagram A n a))) + ( naturality-map-section-dependent-sequential-diagram _ _ s n a) + + compute-comp-over-diagram' : + (s : section-descent-data-sequential-colimit Q') → + htpy-section-dependent-sequential-diagram + ( comp-over-diagram' (Q ∘ f∞) id-fam-equiv s) + ( s) + pr1 (compute-comp-over-diagram' s) n = refl-htpy + pr2 (compute-comp-over-diagram' s) n a = + right-unit ∙ + ap-binary + ( _∙_) + ( ap + ( inv) + ( compute-preserves-tr-id + ( coherence-cocone-sequential-diagram c n a) + ( map-section-dependent-sequential-diagram _ _ s n a))) + ( ap-id (naturality-map-section-dependent-sequential-diagram _ _ s n a)) + + theorem' : + (P : X → UU l5) + (let P' = descent-data-family-cocone-sequential-diagram c P) + (e' : fam-equiv P (Q ∘ f∞)) + (s : section-descent-data-sequential-colimit P') + (let s∞ = sect-family-sect-dd-sequential-colimit up-c P s) → + sect-family-sect-dd-sequential-colimit up-c (Q ∘ f∞) + ( comp-over-diagram' P e' s) ~ + (map-fam-equiv e' _ ∘ s∞) + theorem' P = + ind-fam-equiv' + ( λ P e' → + let P' = descent-data-family-cocone-sequential-diagram c P in + (s : section-descent-data-sequential-colimit P') → + sect-family-sect-dd-sequential-colimit up-c (Q ∘ f∞) + ( comp-over-diagram' P e' s) ~ + map-fam-equiv e' _ ∘ sect-family-sect-dd-sequential-colimit up-c P s) + ( λ s → + htpy-colimit-htpy-diagram-section up-c (Q ∘ f∞) _ _ + ( compute-comp-over-diagram' s)) +``` + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {A : sequential-diagram l1} {X : UU l2} + {c : cocone-sequential-diagram A X} + (up-c : universal-property-sequential-colimit c) + {B : sequential-diagram l3} {Y : UU l4} + {c' : cocone-sequential-diagram B Y} + (up-c' : universal-property-sequential-colimit c') + (f : hom-sequential-diagram A B) + {P : X → UU l5} {Q : Y → UU l5} + (let + P' = descent-data-family-cocone-sequential-diagram c P + Q' = descent-data-family-cocone-sequential-diagram c' Q + f∞ = map-sequential-colimit-hom-sequential-diagram up-c c' f) + (s : section-descent-data-sequential-colimit P') + (t : section-descent-data-sequential-colimit Q') + (let + s∞ = sect-family-sect-dd-sequential-colimit up-c P s + t∞ = sect-family-sect-dd-sequential-colimit up-c' Q t) + (e : fam-equiv P (Q ∘ f∞)) + (let C = htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c' f) + (let + f∞n = + λ n a → + tr Q (C n a) ∘ map-fam-equiv e (map-cocone-sequential-diagram c n a)) + where + + + -- TODO: cleanup + -- - make γ into a proper definition + -- - pasting of squares + -- - find the right lemmas + opaque + unfolding square-over-diagram-square-over-colimit γ γ' γ-base' + square-colimit-cube-diagram : + (F : + (n : ℕ) → + f∞n n _ ∘ map-section-dependent-sequential-diagram _ _ s n ~ + map-section-dependent-sequential-diagram _ _ t n ∘ + map-hom-sequential-diagram B f n) → + ((n : ℕ) → + section-square-over + ( map-sequential-diagram A n) + ( map-hom-sequential-diagram B f n) + ( map-hom-sequential-diagram B f (succ-ℕ n)) + ( map-sequential-diagram B n) + ( λ {a} → map-family-descent-data-sequential-colimit P' n a) + ( λ {a} → f∞n n a) + ( λ {a} → f∞n (succ-ℕ n) a) + ( λ {b} → map-family-descent-data-sequential-colimit Q' n b) + ( map-section-dependent-sequential-diagram _ _ s n) + ( map-section-dependent-sequential-diagram _ _ t n) + ( map-section-dependent-sequential-diagram _ _ s (succ-ℕ n)) + ( map-section-dependent-sequential-diagram _ _ t (succ-ℕ n)) + ( naturality-map-section-dependent-sequential-diagram _ _ s n) + ( F n) + ( F (succ-ℕ n)) + ( naturality-map-section-dependent-sequential-diagram _ _ t n) + ( naturality-map-hom-sequential-diagram B f n) + ( square-over-diagram-square-over-colimit up-c c' f P Q e n _)) → + map-fam-equiv e _ ∘ s∞ ~ t∞ ∘ f∞ + square-colimit-cube-diagram F cubes = + inv-htpy (theorem' up-c up-c' f Q P e s) ∙h + theorem up-c up-c' Q f t _ F + ( λ n a → + assoc _ _ _ ∙ + ap + ( γ up-c up-c' Q f t n a (map-fam-equiv e (map-cocone-sequential-diagram c n a) (map-section-dependent-sequential-diagram _ _ s n a)) ∙_) + ( ( ap + ( _∙ F (succ-ℕ n) (map-sequential-diagram A n a)) + ( ap-concat (tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) + ( inv (preserves-tr (map-fam-equiv e) (coherence-cocone-sequential-diagram c n a) (map-section-dependent-sequential-diagram _ _ s n a))) + ( ap (map-fam-equiv e (map-cocone-sequential-diagram c (succ-ℕ n) (map-sequential-diagram A n a))) (naturality-map-section-dependent-sequential-diagram _ _ s n a)) ∙ + ap + ( ap (tr Q (C (succ-ℕ n) (map-sequential-diagram A n a))) (inv (preserves-tr (map-fam-equiv e) (coherence-cocone-sequential-diagram c n a) (map-section-dependent-sequential-diagram _ _ s n a))) ∙_) + ( inv (ap-comp (tr Q (C (succ-ℕ n) _)) (map-fam-equiv e _) (naturality-map-section-dependent-sequential-diagram _ _ s n a))))) ∙ + ( assoc _ _ _)) ∙ + inv (assoc _ _ _) ∙ + inv (assoc _ _ _) ∙ + cubes n a) +``` diff --git a/src/synthetic-homotopy-theory/morphisms-dependent-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/morphisms-dependent-sequential-diagrams.lagda.md index 129a0c0eca..5ce1fa4428 100644 --- a/src/synthetic-homotopy-theory/morphisms-dependent-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/morphisms-dependent-sequential-diagrams.lagda.md @@ -10,10 +10,13 @@ module synthetic-homotopy-theory.morphisms-dependent-sequential-diagrams where open import elementary-number-theory.natural-numbers open import foundation.commuting-squares-of-maps +open import foundation.dependent-identifications open import foundation.dependent-pair-types +open import foundation.transport-along-identifications open import foundation.universe-levels open import synthetic-homotopy-theory.dependent-sequential-diagrams +open import synthetic-homotopy-theory.morphisms-sequential-diagrams open import synthetic-homotopy-theory.sequential-diagrams ``` @@ -111,3 +114,76 @@ module _ ( map-hom-dependent-sequential-diagram) coh-hom-dependent-sequential-diagram = pr2 h ``` + +### Morphisms of dependent sequential diagrams over morphisms of sequential diagrams + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2} + (P : dependent-sequential-diagram A l3) + (Q : dependent-sequential-diagram B l4) + (h : hom-sequential-diagram A B) + where + + hom-dependent-sequential-diagram-over : UU (l1 ⊔ l3 ⊔ l4) + hom-dependent-sequential-diagram-over = + Σ ( (n : ℕ) (a : family-sequential-diagram A n) → + family-dependent-sequential-diagram P n a → + family-dependent-sequential-diagram Q n + ( map-hom-sequential-diagram B h n a)) + ( λ f → + (n : ℕ) (a : family-sequential-diagram A n) → + (p : family-dependent-sequential-diagram P n a) → + dependent-identification + ( family-dependent-sequential-diagram Q (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B h n a) + ( map-dependent-sequential-diagram Q n + ( map-hom-sequential-diagram B h n a) + ( f n a p)) + ( f (succ-ℕ n) (map-sequential-diagram A n a) (map-dependent-sequential-diagram P n a p))) +``` + +## Properties + +### TODO + +```agda +module _ + {l1 l2 l3 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2} + (h : hom-sequential-diagram A B) + where + + pullback-hom-dependent-sequential-diagram : + dependent-sequential-diagram B l3 → + dependent-sequential-diagram A l3 + pr1 (pullback-hom-dependent-sequential-diagram Q) n a = + family-dependent-sequential-diagram Q n + ( map-hom-sequential-diagram B h n a) + pr2 (pullback-hom-dependent-sequential-diagram Q) n a q = + tr + ( family-dependent-sequential-diagram Q (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B h n a) + ( map-dependent-sequential-diagram Q n + ( map-hom-sequential-diagram B h n a) + ( q)) +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2} + {P : dependent-sequential-diagram A l3} + {Q : dependent-sequential-diagram B l4} + (h : hom-sequential-diagram A B) + where + + open import foundation.homotopies + + hom-dep-seq-diag-over-hom-dep-seq-diag : + hom-dependent-sequential-diagram P + ( pullback-hom-dependent-sequential-diagram h Q) → + hom-dependent-sequential-diagram-over P Q h + pr1 (hom-dep-seq-diag-over-hom-dep-seq-diag h') = + map-hom-dependent-sequential-diagram (pullback-hom-dependent-sequential-diagram h Q) h' + pr2 (hom-dep-seq-diag-over-hom-dep-seq-diag h') n a = + inv-htpy (coh-hom-dependent-sequential-diagram (pullback-hom-dependent-sequential-diagram h Q) h' n a) +``` diff --git a/src/synthetic-homotopy-theory/morphisms-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/morphisms-descent-data-pushouts.lagda.md index 27f747d90f..98d068c27f 100644 --- a/src/synthetic-homotopy-theory/morphisms-descent-data-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/morphisms-descent-data-pushouts.lagda.md @@ -74,7 +74,7 @@ homotopies HB(gs) ·r PS s hB(gs) ∘ PS s ---------------> kB(gs) ∘ PS s | | - hS s | | tS s + hS s | | kS s | | ∨ ∨ QS s ∘ hA(fs) ---------------> QS s ∘ kA(fs) @@ -83,10 +83,10 @@ homotopies [commutes](foundation-core.commuting-squares-of-homotopies.md). This coherence datum may be seen as a filler of the diagram one gets by gluing the squares `hS` -and `tS` along the common vertical maps +and `kS` along the common vertical maps ```text - tA(fs) + kA(fs) ________ / ∨ PA(fs) QA(fs) @@ -94,7 +94,7 @@ and `tS` along the common vertical maps | hA(fs) | | | PS s | | QS s - | tB(gs) | + | kB(gs) | | ________ | ∨ / ∨ ∨ PB(gs) QB(gs). @@ -102,7 +102,7 @@ and `tS` along the common vertical maps hB(gs) ``` -The front and back faces are `hS s` and `tS s`, and the top and bottom faces are +The front and back faces are `hS s` and `kS s`, and the top and bottom faces are `HA(fs)` and `HB(gs)`, respectively. `HS` then expresses that going along the front face and then the top face is homotopic to first going along the bottom face and then the back face. diff --git a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md index a094834153..d4a6a5751d 100644 --- a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md @@ -24,6 +24,7 @@ open import foundation.structure-identity-principle open import foundation.torsorial-type-families open import foundation.universe-levels open import foundation.whiskering-homotopies-composition +open import foundation.whiskering-homotopies-concatenation open import synthetic-homotopy-theory.dependent-sequential-diagrams open import synthetic-homotopy-theory.sequential-diagrams @@ -274,3 +275,54 @@ module _ eq-htpy-sequential-diagram f f' = map-inv-equiv (extensionality-hom-sequential-diagram f f') ``` + +### Composition of morphisms of sequential diagrams is associative + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : sequential-diagram l1} {B : sequential-diagram l2} + {C : sequential-diagram l3} {D : sequential-diagram l4} + (f : hom-sequential-diagram A B) (g : hom-sequential-diagram B C) + (h : hom-sequential-diagram C D) + where + + assoc-comp-hom-sequential-diagram : + htpy-hom-sequential-diagram D + ( comp-hom-sequential-diagram A B D + ( comp-hom-sequential-diagram B C D h g) + ( f)) + ( comp-hom-sequential-diagram A C D h + ( comp-hom-sequential-diagram A B C g f)) + pr1 assoc-comp-hom-sequential-diagram n = refl-htpy + pr2 assoc-comp-hom-sequential-diagram n = + right-unit-htpy ∙h + assoc-htpy + ( naturality-map-hom-sequential-diagram D h n ·r + ( map-hom-sequential-diagram C g n ∘ + map-hom-sequential-diagram B f n)) + ( map-hom-sequential-diagram D h (succ-ℕ n) ·l + naturality-map-hom-sequential-diagram C g n ·r + map-hom-sequential-diagram B f n) + ( ( map-hom-sequential-diagram D h (succ-ℕ n) ∘ + map-hom-sequential-diagram C g (succ-ℕ n)) ·l + naturality-map-hom-sequential-diagram B f n) ∙h + left-whisker-concat-htpy + ( naturality-map-hom-sequential-diagram D h n ·r + ( map-hom-sequential-diagram C g n ∘ map-hom-sequential-diagram B f n)) + ( left-whisker-concat-htpy + ( map-hom-sequential-diagram D h (succ-ℕ n) ·l + naturality-map-hom-sequential-diagram C g n ·r + map-hom-sequential-diagram B f n) + ( inv-preserves-comp-left-whisker-comp + ( map-hom-sequential-diagram D h (succ-ℕ n)) + ( map-hom-sequential-diagram C g (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram B f n)) ∙h + inv-htpy + ( distributive-left-whisker-comp-concat + ( map-hom-sequential-diagram D h (succ-ℕ n)) + ( naturality-map-hom-sequential-diagram C g n ·r + map-hom-sequential-diagram B f n) + ( map-hom-sequential-diagram C g (succ-ℕ n) ·l + naturality-map-hom-sequential-diagram B f n))) +``` diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md index 1b5112681f..7c98487510 100644 --- a/src/synthetic-homotopy-theory/pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pushouts.lagda.md @@ -21,6 +21,7 @@ open import foundation.identity-types open import foundation.propositions open import foundation.retractions open import foundation.sections +open import foundation.span-diagrams open import foundation.transport-along-homotopies open import foundation.transport-along-identifications open import foundation.universe-levels @@ -124,6 +125,37 @@ cocone-pushout : pr1 (cocone-pushout f g) = inl-pushout f g pr1 (pr2 (cocone-pushout f g)) = inr-pushout f g pr2 (pr2 (cocone-pushout f g)) = glue-pushout f g + +module _ + {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) + where + + standard-pushout : UU (l1 ⊔ l2 ⊔ l3) + standard-pushout = + pushout (left-map-span-diagram 𝒮) (right-map-span-diagram 𝒮) + + inl-standard-pushout : domain-span-diagram 𝒮 → standard-pushout + inl-standard-pushout = + inl-pushout (left-map-span-diagram 𝒮) (right-map-span-diagram 𝒮) + + inr-standard-pushout : codomain-span-diagram 𝒮 → standard-pushout + inr-standard-pushout = + inr-pushout (left-map-span-diagram 𝒮) (right-map-span-diagram 𝒮) + + glue-standard-pushout : + coherence-square-maps + ( right-map-span-diagram 𝒮) + ( left-map-span-diagram 𝒮) + ( inr-standard-pushout) + ( inl-standard-pushout) + glue-standard-pushout = + glue-pushout (left-map-span-diagram 𝒮) (right-map-span-diagram 𝒮) + + cocone-pushout-span-diagram : + cocone-span-diagram 𝒮 standard-pushout + pr1 cocone-pushout-span-diagram = inl-standard-pushout + pr1 (pr2 cocone-pushout-span-diagram) = inr-standard-pushout + pr2 (pr2 cocone-pushout-span-diagram) = glue-standard-pushout ``` ### The dependent cogap map diff --git a/src/synthetic-homotopy-theory/sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/sequential-colimits.lagda.md index e0767413bd..4b5b04f385 100644 --- a/src/synthetic-homotopy-theory/sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/sequential-colimits.lagda.md @@ -16,6 +16,7 @@ open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies +open import foundation.identity-types open import foundation.propositions open import foundation.universe-levels @@ -205,6 +206,23 @@ module _ ( x : standard-sequential-colimit A) → P x dependent-cogap-standard-sequential-colimit = map-inv-equiv equiv-dup-standard-sequential-colimit + + compute-incl-dependent-cogap-standard-sequential-colimit : + { P : standard-sequential-colimit A → UU l2} → + ( d : + dependent-cocone-sequential-diagram + ( cocone-standard-sequential-colimit A) + ( P)) → + ( n : ℕ) (a : family-sequential-diagram A n) → + dependent-cogap-standard-sequential-colimit d + ( map-cocone-standard-sequential-colimit n a) ＝ + map-dependent-cocone-sequential-diagram P d n a + compute-incl-dependent-cogap-standard-sequential-colimit d = + pr1 + ( htpy-eq-dependent-cocone-sequential-diagram _ _ d + ( is-section-map-inv-is-equiv + ( dup-standard-sequential-colimit _) + ( d))) ``` ### The small predicate of being a sequential colimit cocone diff --git a/src/synthetic-homotopy-theory/shifts-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/shifts-sequential-diagrams.lagda.md index c7c6e22f6f..be26604bde 100644 --- a/src/synthetic-homotopy-theory/shifts-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/shifts-sequential-diagrams.lagda.md @@ -934,17 +934,20 @@ module _ (up-c : universal-property-sequential-colimit c) where - compute-map-colimit-hom-shift-once-sequential-diagram : - map-sequential-colimit-hom-sequential-diagram - ( up-c) - ( shift-once-cocone-sequential-diagram c) - ( hom-shift-once-sequential-diagram A) ~ - id - compute-map-colimit-hom-shift-once-sequential-diagram = - ( htpy-map-universal-property-htpy-cocone-sequential-diagram - ( up-c) - ( compute-map-cocone-hom-shift-sequential-diagram c)) ∙h - ( compute-map-universal-property-sequential-colimit-id up-c) + opaque + unfolding map-sequential-colimit-hom-sequential-diagram + + compute-map-colimit-hom-shift-once-sequential-diagram : + map-sequential-colimit-hom-sequential-diagram + ( up-c) + ( shift-once-cocone-sequential-diagram c) + ( hom-shift-once-sequential-diagram A) ~ + id + compute-map-colimit-hom-shift-once-sequential-diagram = + ( htpy-map-universal-property-htpy-cocone-sequential-diagram + ( up-c) + ( compute-map-cocone-hom-shift-sequential-diagram c)) ∙h + ( compute-map-universal-property-sequential-colimit-id up-c) module _ {l1 l2 : Level} {A : sequential-diagram l1} diff --git a/src/synthetic-homotopy-theory/stuff-over.lagda.md b/src/synthetic-homotopy-theory/stuff-over.lagda.md new file mode 100644 index 0000000000..e5214a52e0 --- /dev/null +++ b/src/synthetic-homotopy-theory/stuff-over.lagda.md @@ -0,0 +1,1389 @@ +# Stuff over other stuff + +```agda +{-# OPTIONS --lossy-unification #-} +module synthetic-homotopy-theory.stuff-over where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-dependent-functions +open import foundation.action-on-identifications-functions +open import foundation.commuting-cubes-of-maps +open import foundation.commuting-squares-of-homotopies +open import foundation.commuting-squares-of-maps +open import foundation.commuting-triangles-of-maps +open import foundation.dependent-identifications +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.transport-along-identifications +open import foundation.transposition-identifications-along-equivalences +open import foundation.universe-levels +open import foundation.whiskering-higher-homotopies-composition +open import foundation.whiskering-homotopies-composition +open import foundation.whiskering-homotopies-concatenation +``` + +
+ +```agda +open import foundation.dependent-pair-types +open import foundation.equality-dependent-pair-types +open import foundation.functoriality-dependent-pair-types +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} + {A' : A → UU l3} {B' : B → UU l4} + (f : A → B) + (f' : (a : A) → A' a → B' (f a)) + where + + tot-map-over : Σ A A' → Σ B B' + tot-map-over = map-Σ B' f f' + + coh-tot-map-over : coherence-square-maps tot-map-over pr1 pr1 f + coh-tot-map-over = refl-htpy + +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} + {A' : A → UU l3} (B' : B → UU l4) + {f g : A → B} + (H : f ~ g) + (f' : {a : A} → A' a → B' (f a)) + (g' : {a : A} → A' a → B' (g a)) + where + + htpy-over : UU (l1 ⊔ l3 ⊔ l4) + htpy-over = + {a : A} (a' : A' a) → dependent-identification B' (H a) (f' a') (g' a') + +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} + {A' : A → UU l3} (B' : B → UU l4) + {f g : A → B} + (H : f ~ g) + (f' : {a : A} → A' a → B' (f a)) + (g' : {a : A} → A' a → B' (g a)) + where + + inv-htpy-over : htpy-over B' H f' g' → htpy-over B' (inv-htpy H) g' f' + inv-htpy-over H' {a} a' = inv-dependent-identification B' (H a) (H' a') + +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + compute-inv-dependent-identification : + {x y : A} (p : x ＝ y) {x' : B x} {y' : B y} → + (q : dependent-identification B p x' y') → + inv-dependent-identification B p q ＝ map-eq-transpose-equiv-inv' (equiv-tr B p) (inv q) + compute-inv-dependent-identification refl q = inv (right-unit ∙ ap-id (inv q)) + +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {X : UU l3} + {A' : A → UU l4} {B' : B → UU l5} {X' : X → UU l6} + {f g : A → B} + (H : f ~ g) + {f' : {a : A} → A' a → B' (f a)} + {g' : {a : A} → A' a → B' (g a)} + (H' : htpy-over B' H f' g') + (s : X → A) (s' : {x : X} → X' x → A' (s x)) + where + + right-whisk-htpy-over : htpy-over B' (H ·r s) (f' ∘ s') (g' ∘ s') + right-whisk-htpy-over a' = H' (s' a') + +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} + {A' : A → UU l3} {B' : B → UU l4} + where + + left-whisk-dependent-identification : + {s : A → B} (s' : {a : A} → A' a → B' (s a)) + {x y : A} (p : x ＝ y) + {x' : A' x} {y' : A' y} (q : dependent-identification A' p x' y') → + dependent-identification B' (ap s p) (s' x') (s' y') + left-whisk-dependent-identification s' refl q = ap s' q + + compute-left-whisk-dependent-identification : + {s : A → B} (s' : {a : A} → A' a → B' (s a)) + {x y : A} (p : x ＝ y) + {x' : A' x} {y' : A' y} (q : dependent-identification A' p x' y') → + left-whisk-dependent-identification s' p q ＝ + substitution-law-tr B' s p ∙ inv (preserves-tr (λ a → s' {a}) p x') ∙ ap s' q + compute-left-whisk-dependent-identification s' refl q = refl + +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {X : UU l3} + {A' : A → UU l4} {B' : B → UU l5} {X' : X → UU l6} + {f g : A → B} + (H : f ~ g) + {f' : {a : A} → A' a → B' (f a)} + {g' : {a : A} → A' a → B' (g a)} + (H' : htpy-over B' H f' g') + {s : B → X} (s' : {b : B} → B' b → X' (s b)) + where + + LWMOTIF : {a : A} (a' : A' a) (g : A → B) (H : f ~ g) → UU (l5 ⊔ l6) + LWMOTIF {a} a' g H = + {g'a' : B' (g a)} → + (H' : tr B' (H a) (f' a') ＝ g'a') → + tr X' (ap s (H a)) (s' (f' a')) ＝ s' (g'a') + + left-whisk-htpy-over : htpy-over X' (s ·l H) (s' ∘ f') (s' ∘ g') + left-whisk-htpy-over {a} a' = left-whisk-dependent-identification s' (H a) (H' a') + +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} {A' : A → UU l3} {B' : B → UU l4} + {f g h : A → B} + (H : f ~ g) (K : g ~ h) + {f' : {a : A} → A' a → B' (f a)} + {g' : {a : A} → A' a → B' (g a)} + {h' : {a : A} → A' a → B' (h a)} + (H' : htpy-over B' H f' g') (K' : htpy-over B' K g' h') + where + + concat-htpy-over : htpy-over B' (H ∙h K) f' h' + concat-htpy-over {a} a' = + concat-dependent-identification B' (H a) (K a) (H' a') (K' a') + +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} {A' : A → UU l3} {B' : B → UU l4} + (f : A → B) + (f' : {a : A} → A' a → B' (f a)) + (sA : (a : A) → A' a) + (sB : (b : B) → B' b) + where + + section-map-over : UU (l1 ⊔ l4) + section-map-over = (a : A) → f' (sA a) ＝ sB (f a) + +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} + {A' : A → UU l4} {B' : B → UU l5} {C' : C → UU l6} + (g : B → C) (f : A → B) + (g' : {b : B} → B' b → C' (g b)) + (f' : {a : A} → A' a → B' (f a)) + (sA : (a : A) → A' a) (sB : (b : B) → B' b) (sC : (c : C) → C' c) + where + + comp-section-map-over : + section-map-over g g' sB sC → section-map-over f f' sA sB → + section-map-over (g ∘ f) (g' ∘ f') sA sC + comp-section-map-over G F = + g' ·l F ∙h G ·r f + +module _ + {l1 l2 : Level} + {A : UU l1} {B : A → UU l2} + {x y : A} (p : x ＝ y) + {x' : B x} {y' : B y} (q : dependent-identification B p x' y') + (s : (a : A) → B a) + (F : x' ＝ s x) (G : y' ＝ s y) + where + + section-dependent-identification : UU l2 + section-dependent-identification = + q ∙ G ＝ ap (tr B p) F ∙ apd s p + +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} {A' : A → UU l3} {B' : B → UU l4} + {f g : A → B} + (H : f ~ g) + {f' : {a : A} → A' a → B' (f a)} + {g' : {a : A} → A' a → B' (g a)} + (H' : htpy-over B' H f' g') + (sA : (a : A) → A' a) + (sB : (b : B) → B' b) + (F : section-map-over f f' sA sB) + (G : section-map-over g g' sA sB) + where + + section-htpy-over : UU (l1 ⊔ l4) + section-htpy-over = + (a : A) → section-dependent-identification (H a) (H' (sA a)) sB (F a) (G a) + +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + inv-section-identification-over : + {x y : A} (p : x ＝ y) → + {x' : B x} {y' : B y} (q : dependent-identification B p x' y') → + (s : (a : A) → B a) → + (F : x' ＝ s x) (G : y' ＝ s y) → + section-dependent-identification p q s F G → + section-dependent-identification + ( inv p) + ( inv-dependent-identification B p q) + ( s) + ( G) + ( F) + inv-section-identification-over refl refl s F G α = + inv (right-unit ∙ ap-id G ∙ α ∙ right-unit ∙ ap-id F) + +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} {A' : A → UU l3} {B' : B → UU l4} + {f g : A → B} + (H : f ~ g) + {f' : {a : A} → A' a → B' (f a)} + {g' : {a : A} → A' a → B' (g a)} + (H' : htpy-over B' H f' g') + (sA : (a : A) → A' a) + (sB : (b : B) → B' b) + (F : section-map-over f f' sA sB) + (G : section-map-over g g' sA sB) + where + + inv-section-htpy-over : + section-htpy-over H H' sA sB F G → + section-htpy-over + ( inv-htpy H) + ( inv-htpy-over B' H f' g' H') + ( sA) + ( sB) + ( G) + ( F) + inv-section-htpy-over α a = + inv-section-identification-over (H a) (H' (sA a)) sB (F a) (G a) (α a) + +module _ + {l1 l2 l3 l4 l5 l6 l7 l8 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} + {A' : A → UU l5} {B' : B → UU l6} {C' : C → UU l7} {D' : D → UU l8} + {f : A → B} {g : B → C} {h : C → D} + (f' : {a : A} → A' a → B' (f a)) + (g' : {b : B} → B' b → C' (g b)) + (h' : {c : C} → C' c → D' (h c)) + (sA : (a : A) → A' a) + (sB : (b : B) → B' b) + (sC : (c : C) → C' c) + (sD : (d : D) → D' d) + (F : section-map-over f f' sA sB) + (G : section-map-over g g' sB sC) + (H : section-map-over h h' sC sD) + where + + assoc-comp-section-map-over : + section-htpy-over + ( refl-htpy {f = h ∘ g ∘ f}) + ( refl-htpy {f = h' ∘ g' ∘ f'}) + sA sD + ( comp-section-map-over (h ∘ g) f (h' ∘ g') f' sA sB sD + ( comp-section-map-over h g h' g' sB sC sD H G) + ( F)) + ( comp-section-map-over h (g ∘ f) h' (g' ∘ f') sA sC sD H + ( comp-section-map-over g f g' f' sA sB sC G F)) + assoc-comp-section-map-over = + inv-htpy + ( right-unit-htpy ∙h + left-unit-law-left-whisker-comp _ ∙h + inv-htpy-assoc-htpy ((h' ∘ g') ·l F) (h' ·l G ·r f) (H ·r (g ∘ f)) ∙h + right-whisker-concat-htpy + ( ( right-whisker-concat-htpy + ( inv-preserves-comp-left-whisker-comp h' g' F) + ( h' ·l G ·r f)) ∙h + ( inv-htpy + ( distributive-left-whisker-comp-concat h' + ( g' ·l F) + ( G ·r f)))) + ( H ·r g ·r f)) + +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {X : UU l3} + {A' : A → UU l4} {B' : B → UU l5} {X' : X → UU l6} + {f g : A → B} + (H : f ~ g) + {f' : {a : A} → A' a → B' (f a)} + {g' : {a : A} → A' a → B' (g a)} + (H' : htpy-over B' H f' g') + (sA : (a : A) → A' a) + (sB : (b : B) → B' b) + (F : section-map-over f f' sA sB) + (G : section-map-over g g' sA sB) + (α : section-htpy-over H H' sA sB F G) + (s : X → A) + (s' : {x : X} → X' x → A' (s x)) + (sX : (x : X) → X' x) + (S : section-map-over s s' sX sA) + where + open import foundation.commuting-squares-of-identifications + open import foundation.commuting-triangles-of-identifications + + right-whisk-section-htpy-over : + section-htpy-over (H ·r s) + ( right-whisk-htpy-over H H' s s') + sX sB + ( comp-section-map-over f s f' s' sX sA sB F S) + ( comp-section-map-over g s g' s' sX sA sB G S) + right-whisk-section-htpy-over x = + right-whisker-concat-coherence-square-identifications + ( ap (tr B' (H (s x)) ∘ f') (S x)) + ( H' (s' (sX x))) + ( H' (sA (s x))) + ( ap g' (S x)) + ( nat-htpy (H' {s x}) (S x)) + ( G (s x)) ∙ + ap (_∙ (H' (sA (s x)) ∙ G (s x))) (ap-comp (tr B' (H (s x))) f' (S x)) ∙ + ap (ap (tr B' (H (s x))) (ap f' (S x)) ∙_) (α (s x)) ∙ + right-whisker-concat-coherence-triangle-identifications' + ( ap (tr B' (H (s x))) (ap f' (S x) ∙ F (s x))) + ( ap (tr B' (H (s x))) (F (s x))) + ( ap (tr B' (H (s x))) (ap f' (S x))) + ( apd sB (H (s x))) + ( inv (ap-concat (tr B' (H (s x))) (ap f' (S x)) (F (s x)))) + +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {X : UU l2} + {A' : A → UU l3} {X' : X → UU l4} + where + + left-whisk-section-dependent-identification : + {x y : A} (p : x ＝ y) + {x' : A' x} {y' : A' y} (q : dependent-identification A' p x' y') + (sA : (a : A) → A' a) + (F : x' ＝ sA x) (G : y' ＝ sA y) + (α : section-dependent-identification p q sA F G) + {s : A → X} (s' : {a : A} → A' a → X' (s a)) + (sX : (x : X) → X' x) + (S : section-map-over s s' sA sX) → + section-dependent-identification + ( ap s p) + ( left-whisk-dependent-identification s' p q) + sX (ap s' F ∙ S x) (ap s' G ∙ S y) + left-whisk-section-dependent-identification {x} refl refl sA F G α s' sX S = + ap (λ p → ap s' p ∙ S x) (α ∙ right-unit ∙ ap-id F) ∙ + inv (right-unit ∙ ap-id (ap s' F ∙ S x)) + +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {X : UU l3} + {A' : A → UU l4} {B' : B → UU l5} {X' : X → UU l6} + {f g : A → B} + (H : f ~ g) + {f' : {a : A} → A' a → B' (f a)} + {g' : {a : A} → A' a → B' (g a)} + (H' : htpy-over B' H f' g') + (sA : (a : A) → A' a) + (sB : (b : B) → B' b) + (F : section-map-over f f' sA sB) + (G : section-map-over g g' sA sB) + (α : section-htpy-over H H' sA sB F G) + (s : B → X) + (s' : {b : B} → B' b → X' (s b)) + (sX : (x : X) → X' x) + (S : section-map-over s s' sB sX) + where + + left-whisk-section-htpy-over : + section-htpy-over (s ·l H) + ( left-whisk-htpy-over H H' s') + sA sX + ( comp-section-map-over s f s' f' sA sB sX S F) + ( comp-section-map-over s g s' g' sA sB sX S G) + left-whisk-section-htpy-over a = + left-whisk-section-dependent-identification (H a) (H' (sA a)) sB (F a) (G a) (α a) s' sX S + +module _ + {l1 l2 : Level} + {A : UU l1} {B : A → UU l2} + where + + concat-section-dependent-identification : + {x y z : A} (p : x ＝ y) (q : y ＝ z) + {x' : B x} {y' : B y} {z' : B z} + (p' : dependent-identification B p x' y') + (q' : dependent-identification B q y' z') + (s : (a : A) → B a) + (F : x' ＝ s x) (G : y' ＝ s y) (H : z' ＝ s z) + (α : section-dependent-identification p p' s F G) + (β : section-dependent-identification q q' s G H) → + section-dependent-identification (p ∙ q) + ( concat-dependent-identification B p q p' q') + ( s) + ( F) + ( H) + concat-section-dependent-identification refl q refl q' s F G H α β = + β ∙ ap (λ p → ap (tr B q) p ∙ apd s q) (α ∙ right-unit ∙ ap-id F) + +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} {A' : A → UU l3} {B' : B → UU l4} + {f g i : A → B} + (H : f ~ g) (K : g ~ i) + {f' : {a : A} → A' a → B' (f a)} + {g' : {a : A} → A' a → B' (g a)} + {i' : {a : A} → A' a → B' (i a)} + (H' : htpy-over B' H f' g') (K' : htpy-over B' K g' i') + (sA : (a : A) → A' a) + (sB : (b : B) → B' b) + (F : section-map-over f f' sA sB) + (G : section-map-over g g' sA sB) + (I : section-map-over i i' sA sB) + (α : section-htpy-over H H' sA sB F G) + (β : section-htpy-over K K' sA sB G I) + where + + concat-section-htpy-over : + section-htpy-over + ( H ∙h K) + ( concat-htpy-over H K H' K') + ( sA) + ( sB) + ( F) + ( I) + concat-section-htpy-over a = + concat-section-dependent-identification + ( H a) (K a) (H' (sA a)) (K' (sA a)) sB (F a) (G a) (I a) (α a) (β a) + +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {X : UU l3} + {A' : A → UU l4} {B' : B → UU l5} {X' : X → UU l6} + (f : A → B) (g : A → X) (m : B → X) + (f' : {a : A} → A' a → B' (f a)) + (g' : {a : A} → A' a → X' (g a)) + (m' : {b : B} → B' b → X' (m b)) + (sA : (a : A) → A' a) (sB : (b : B) → B' b) (sX : (x : X) → X' x) + (F : (a : A) → f' (sA a) ＝ sB (f a)) + (G : (a : A) → g' (sA a) ＝ sX (g a)) + (M : (b : B) → m' (sB b) ＝ sX (m b)) + where + + section-triangle-over : + (H : coherence-triangle-maps g m f) → + (H' : htpy-over X' H g' (m' ∘ f')) → + UU (l1 ⊔ l6) + section-triangle-over H H' = + (a : A) → + H' (sA a) ∙ ap m' (F a) ∙ (M (f a)) ＝ + ap (tr X' (H a)) (G a) ∙ apd sX (H a) + + unget-section-triangle-over : + (H : coherence-triangle-maps g m f) → + (H' : htpy-over X' H g' (m' ∘ f')) → + section-triangle-over H H' → + section-htpy-over H H' sA sX G + ( comp-section-map-over m f m' f' sA sB sX M F) + unget-section-triangle-over H H' α = + inv-htpy-assoc-htpy (H' ·r sA) (m' ·l F) (M ·r f) ∙h α + + section-triangle-over' : + (H : coherence-triangle-maps' g m f) → + (H' : htpy-over X' H (m' ∘ f') g') → + UU (l1 ⊔ l6) + section-triangle-over' H H' = + (a : A) → + H' (sA a) ∙ G a ＝ + ap (tr X' (H a) ∘ m') (F a) ∙ ap (tr X' (H a)) (M (f a)) ∙ apd sX (H a) + + equiv-get-section-triangle-over' : + (H : coherence-triangle-maps' g m f) → + (H' : htpy-over X' H (m' ∘ f') g') → + section-triangle-over' H H' ≃ + section-htpy-over H H' sA sX + ( comp-section-map-over m f m' f' sA sB sX M F) + ( G) + equiv-get-section-triangle-over' H H' = + equiv-Π-equiv-family + ( λ a → + equiv-concat' + ( H' (sA a) ∙ G a) + ( ap + ( _∙ apd sX (H a)) + ( ( ap + ( _∙ ap (tr X' (H a)) (M (f a))) + ( ap-comp (tr X' (H a)) m' (F a))) ∙ + ( inv (ap-concat (tr X' (H a)) (ap m' (F a)) (M (f a))))))) + + unget-section-triangle-over' : + (H : coherence-triangle-maps' g m f) → + (H' : htpy-over X' H (m' ∘ f') g') → + section-triangle-over' H H' → + section-htpy-over H H' sA sX + ( comp-section-map-over m f m' f' sA sB sX M F) + ( G) + unget-section-triangle-over' H H' = + map-equiv (equiv-get-section-triangle-over' H H') + + get-section-triangle-over' : + (H : coherence-triangle-maps' g m f) → + (H' : htpy-over X' H (m' ∘ f') g') → + section-htpy-over H H' sA sX + ( comp-section-map-over m f m' f' sA sB sX M F) + ( G) → + section-triangle-over' H H' + get-section-triangle-over' H H' = + map-inv-equiv (equiv-get-section-triangle-over' H H') + + -- actually ≐ section-triangle-over 🤔 + -- section-triangle-over-inv : + -- (H : coherence-triangle-maps g m f) → + -- (H' : {a : A} (a' : A' a) → dependent-identification X' (H a) (g' a') (m' (f' a'))) → + -- UU (l1 ⊔ l6) + -- section-triangle-over-inv H H' = + -- (a : A) → + -- H' (sA a) ∙ ap m' (F a) ∙ (M (f a)) ＝ + -- ap (tr X' (H a)) (G a) ∙ apd sX (H a) + +module _ + {l1 l2 l3 l4 l5 l6 l7 l8 : Level} + {P1 : UU l1} {P2 : UU l2} {P3 : UU l3} {P4 : UU l4} + {Q1 : P1 → UU l5} {Q2 : P2 → UU l6} {Q3 : P3 → UU l7} {Q4 : P4 → UU l8} + (g1 : P1 → P3) (f1 : P1 → P2) (f2 : P3 → P4) (g2 : P2 → P4) + (g1' : {p : P1} → Q1 p → Q3 (g1 p)) + (f1' : {p : P1} → Q1 p → Q2 (f1 p)) + (f2' : {p : P3} → Q3 p → Q4 (f2 p)) + (g2' : {p : P2} → Q2 p → Q4 (g2 p)) + where + + square-over : coherence-square-maps g1 f1 f2 g2 → UU (l1 ⊔ l5 ⊔ l8) + square-over H = htpy-over Q4 H (g2' ∘ f1') (f2' ∘ g1') + + module _ + (s1 : (p : P1) → Q1 p) (s2 : (p : P2) → Q2 p) (s3 : (p : P3) → Q3 p) + (s4 : (p : P4) → Q4 p) + (G1 : (p : P1) → g1' (s1 p) ＝ s3 (g1 p)) + (F1 : (p : P1) → f1' (s1 p) ＝ s2 (f1 p)) + (F2 : (p : P3) → f2' (s3 p) ＝ s4 (f2 p)) + (G2 : (p : P2) → g2' (s2 p) ＝ s4 (g2 p)) + (H : coherence-square-maps g1 f1 f2 g2) + (H' : square-over H) + where + + section-square-over : UU (l1 ⊔ l8) + section-square-over = + (p : P1) → + H' (s1 p) ∙ ap f2' (G1 p) ∙ (F2 (g1 p)) ＝ + ( ap (tr Q4 (H p) ∘ g2') (F1 p) ∙ + ap (tr Q4 (H p)) (G2 (f1 p)) ∙ + apd s4 (H p)) + + get-section-square-over : + section-htpy-over H H' s1 s4 + ( comp-section-map-over g2 f1 g2' f1' s1 s2 s4 G2 F1) + ( comp-section-map-over f2 g1 f2' g1' s1 s3 s4 F2 G1) → + section-square-over + get-section-square-over α = + assoc-htpy (H' ·r s1) (f2' ·l G1) (F2 ·r g1) ∙h + α ∙h + ( λ p → + ap + ( _∙ apd s4 (H p)) + ( ap-concat (tr Q4 (H p)) (ap g2' (F1 p)) (G2 (f1 p)) ∙ + ap (_∙ _) (inv (ap-comp _ g2' (F1 p))))) + + module _ + (m : P2 → P3) + (m' : {p : P2} → Q2 p → Q3 (m p)) + (B1 : coherence-triangle-maps' g1 m f1) + (B2 : coherence-triangle-maps g2 f2 m) + (T1 : htpy-over Q3 B1 (m' ∘ f1') g1') + (T2 : htpy-over Q4 B2 g2' (f2' ∘ m')) + where + + pasting-triangles-over : + htpy-over Q4 + ( horizontal-pasting-up-diagonal-coherence-triangle-maps g1 f1 f2 g2 B1 B2) + ( g2' ∘ f1') + ( f2' ∘ g1') + pasting-triangles-over = + concat-htpy-over + ( B2 ·r f1) + ( f2 ·l B1) + ( right-whisk-htpy-over B2 T2 f1 f1') + ( left-whisk-htpy-over B1 T1 f2') + + module _ + (m : P2 → P3) + (m' : {p : P2} → Q2 p → Q3 (m p)) + (s1 : (p : P1) → Q1 p) (s2 : (p : P2) → Q2 p) (s3 : (p : P3) → Q3 p) + (s4 : (p : P4) → Q4 p) + (G1 : (p : P1) → g1' (s1 p) ＝ s3 (g1 p)) + (F1 : (p : P1) → f1' (s1 p) ＝ s2 (f1 p)) + (F2 : (p : P3) → f2' (s3 p) ＝ s4 (f2 p)) + (G2 : (p : P2) → g2' (s2 p) ＝ s4 (g2 p)) + (M : (p : P2) → m' (s2 p) ＝ s3 (m p)) + (B1 : coherence-triangle-maps' g1 m f1) + (B2 : coherence-triangle-maps g2 f2 m) + (T1 : htpy-over Q3 B1 (m' ∘ f1') g1') + (T2 : htpy-over Q4 B2 g2' (f2' ∘ m')) + where + + pasting-sections-triangles-over : + section-triangle-over' f1 g1 m f1' g1' m' s1 s2 s3 F1 G1 M B1 T1 → + section-triangle-over m g2 f2 m' g2' f2' s2 s3 s4 M G2 F2 B2 T2 → + section-square-over s1 s2 s3 s4 G1 F1 F2 G2 + ( horizontal-pasting-up-diagonal-coherence-triangle-maps g1 f1 f2 g2 B1 B2) + ( pasting-triangles-over m m' B1 B2 T1 T2) + pasting-sections-triangles-over S1 S2 = + get-section-square-over s1 s2 s3 s4 G1 F1 F2 G2 + ( horizontal-pasting-up-diagonal-coherence-triangle-maps g1 f1 f2 g2 B1 B2) + ( pasting-triangles-over m m' B1 B2 T1 T2) + ( concat-section-htpy-over (B2 ·r f1) (f2 ·l B1) + ( right-whisk-htpy-over B2 T2 f1 f1') + ( left-whisk-htpy-over B1 T1 f2') + s1 s4 + ( comp-section-map-over g2 f1 g2' f1' s1 s2 s4 G2 F1) + ( comp-section-map-over (f2 ∘ m) f1 (f2' ∘ m') f1' s1 s2 s4 + ( comp-section-map-over f2 m f2' m' s2 s3 s4 F2 M) + ( F1)) + ( comp-section-map-over f2 g1 f2' g1' s1 s3 s4 F2 G1) + ( [ii]) + ( concat-section-htpy-over refl-htpy (f2 ·l B1) refl-htpy + ( left-whisk-htpy-over B1 T1 f2') + s1 s4 _ _ _ + ( assoc-comp-section-map-over f1' m' f2' s1 s2 s3 s4 F1 M F2) + ( [iv]))) + where + [i] = + unget-section-triangle-over m g2 f2 m' g2' f2' s2 s3 s4 M G2 F2 B2 T2 S2 + [ii] = right-whisk-section-htpy-over B2 T2 s2 s4 _ _ [i] f1 f1' s1 F1 + [iii] = + unget-section-triangle-over' f1 g1 m f1' g1' m' s1 s2 s3 F1 G1 M B1 T1 S1 + [iv] = left-whisk-section-htpy-over B1 T1 s1 s3 _ _ [iii] f2 f2' s4 F2 +``` + +```agda +-- open import foundation.sections +-- open import foundation.transport-along-homotopies +-- module _ +-- {l1 l2 : Level} +-- {A : UU l1} (B : A → UU l2) +-- where + +-- sect-section : +-- section (pr1 {B = B}) → +-- ((a : A) → B a) +-- sect-section (s , H) a = tr B (H a) (pr2 (s a)) + +-- section-sect : +-- ((a : A) → B a) → +-- section (pr1 {B = B}) +-- section-sect = section-dependent-function + +-- module _ +-- {l1 l2 l3 l4 : Level} +-- {A : UU l1} {B : UU l2} {A' : UU l3} {B' : UU l4} +-- (f : A → B) (f' : A' → B') +-- where + +-- htpy-hom-map : +-- (hA : A' → A) (hB : B' → B) → +-- coherence-square-maps f' hA hB f → +-- (hA' : A' → A) (hB' : B' → B) → +-- coherence-square-maps f' hA' hB' f → +-- hA ~ hA' → hB ~ hB' → +-- UU (l2 ⊔ l3) +-- htpy-hom-map hA hB H hA' hB' H' σA σB = H ∙h (σB ·r f') ~ (f ·l σA) ∙h H' + +-- module _ +-- {l1 l2 l3 l4 l5 l6 : Level} +-- {A : UU l1} {B : UU l2} {C : UU l3} +-- {X : UU l4} {Y : UU l5} {Z : UU l6} +-- (f : A → B) (g : B → C) +-- (f' : X → Y) (g' : Y → Z) +-- (hA hA' : X → A) (hB hB' : Y → B) (hC hC' : Z → C) +-- (σA : hA ~ hA') (σB : hB ~ hB') (σC : hC ~ hC') +-- (NL : coherence-square-maps f' hA hB f) +-- (FL : coherence-square-maps f' hA' hB' f) +-- (α : htpy-hom-map f f' hA hB NL hA' hB' FL σA σB) +-- (NR : coherence-square-maps g' hB hC g) +-- (FR : coherence-square-maps g' hB' hC' g) +-- (β : htpy-hom-map g g' hB hC NR hB' hC' FR σB σC) +-- where +-- open import foundation.commuting-squares-of-homotopies + +-- comp-htpy-hom-map : +-- htpy-hom-map (g ∘ f) (g' ∘ f') +-- hA hC +-- ( pasting-horizontal-coherence-square-maps f' g' hA hB hC f g NL NR) +-- hA' hC' +-- ( pasting-horizontal-coherence-square-maps f' g' hA' hB' hC' f g FL FR) +-- σA σC +-- comp-htpy-hom-map = +-- left-whisker-concat-coherence-square-homotopies (g ·l NL) +-- ( g ·l σB ·r f') (NR ·r f') (FR ·r f') (σC ·r (g' ∘ f')) +-- ( β ·r f') ∙h +-- right-whisker-concat-htpy +-- ( inv-htpy +-- ( distributive-left-whisker-comp-concat g NL (σB ·r f')) ∙h +-- left-whisker-comp² g α ∙h +-- distributive-left-whisker-comp-concat g (f ·l σA) FL ∙h +-- right-whisker-concat-htpy +-- ( preserves-comp-left-whisker-comp g f σA) +-- ( g ·l FL)) +-- ( FR ·r f') ∙h +-- assoc-htpy ((g ∘ f) ·l σA) (g ·l FL) (FR ·r f') + +-- module _ +-- {l1 l2 l3 l4 : Level} +-- {A : UU l1} {B : UU l2} {A' : UU l3} {B' : UU l4} +-- (f : A → B) (f' : A' → B') +-- (hA : A' → A) (hB : B' → B) +-- (H : coherence-square-maps f' hA hB f) +-- where + +-- section-displayed-map-over : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) +-- section-displayed-map-over = +-- Σ ( section hA) +-- ( λ sA → +-- Σ ( section hB) +-- ( λ sB → +-- Σ ( coherence-square-maps +-- f (map-section hA sA) (map-section hB sB) f') +-- ( λ K → +-- htpy-hom-map f f +-- ( hA ∘ map-section hA sA) +-- ( hB ∘ map-section hB sB) +-- ( pasting-vertical-coherence-square-maps f +-- ( map-section hA sA) (map-section hB sB) f' hA hB f K H) +-- id id refl-htpy +-- ( is-section-map-section hA sA) +-- ( is-section-map-section hB sB)))) + +-- module _ +-- {l1 l2 l3 l4 : Level} +-- {A : UU l1} {P : A → UU l2} +-- {B : UU l3} {Q : B → UU l4} +-- (f : A → B) +-- (f' : {a : A} → P a → Q (f a)) +-- where + +-- sect-map-over-section-map-over : +-- (s : +-- section-displayed-map-over f +-- (tot-map-over f (λ a → f' {a})) +-- pr1 pr1 refl-htpy) → +-- section-map-over f +-- ( f') +-- ( sect-section P (pr1 s)) +-- ( sect-section Q (pr1 (pr2 s))) +-- sect-map-over-section-map-over (sA , sB , H , α) a = +-- ( preserves-tr (λ a → f' {a}) (σA a) (sA2 a)) ∙ +-- ( inv (substitution-law-tr Q f (σA a))) ∙ +-- ( ap (λ p → tr Q p (f' (sA2 a))) (inv (α a ∙ right-unit))) ∙ +-- ( tr-concat (H1 a) (σB (f a)) (f' (sA2 a))) ∙ +-- ( ap +-- ( tr Q (σB (f a))) +-- ( substitution-law-tr Q pr1 (H a) ∙ apd pr2 (H a))) +-- where +-- sA1 : A → A +-- sA1 = pr1 ∘ map-section pr1 sA +-- σA : sA1 ~ id +-- σA = is-section-map-section pr1 sA +-- sA2 : (a : A) → P (sA1 a) +-- sA2 = pr2 ∘ map-section pr1 sA +-- sB1 : B → B +-- sB1 = pr1 ∘ map-section pr1 sB +-- σB : sB1 ~ id +-- σB = is-section-map-section pr1 sB +-- H1 : f ∘ sA1 ~ sB1 ∘ f +-- H1 = pr1 ·l H +-- ``` + +-- ```agda +-- module _ +-- {l1 l2 : Level} +-- {A : UU l1} {B : A → UU l2} +-- (s : (a : A) → B a) +-- where + +-- ap-map-section-family-lemma : +-- {a a' : A} (p : a ＝ a') → +-- ap (map-section-family s) p ＝ eq-pair-Σ p (apd s p) +-- ap-map-section-family-lemma refl = refl +-- module _ +-- {l1 l2 l3 : Level} +-- {A : UU l1} {B : UU l2} {Q : B → UU l3} +-- (s : (b : B) → Q b) +-- {f g : A → B} (H : f ~ g) +-- where + +-- left-whisker-dependent-function-lemma : +-- (a : A) → +-- (map-section-family s ·l H) a ＝ eq-pair-Σ (H a) (apd s (H a)) +-- left-whisker-dependent-function-lemma a = ap-map-section-family-lemma s (H a) +-- module _ +-- {l1 l2 : Level} {A : UU l1} {B : A → UU l2} +-- where +-- concat-vertical-eq-pair : +-- {x y : A} (p : x ＝ y) {x' : B x} {y' z' : B y} → +-- (q : dependent-identification B p x' y') → (r : y' ＝ z') → +-- eq-pair-Σ p (q ∙ r) ＝ eq-pair-Σ p q ∙ eq-pair-eq-fiber r +-- concat-vertical-eq-pair {x} refl q r = ap-concat (pair x) q r +-- module _ +-- {l1 l2 l3 l4 : Level} +-- {A : UU l1} {B : UU l2} +-- {A' : A → UU l3} {B' : B → UU l4} +-- {f : A → B} (f' : (a : A) → A' a → B' (f a)) +-- where + +-- ap-map-Σ-eq-fiber : +-- {a : A} (x y : A' a) (p : x ＝ y) → +-- ap (map-Σ B' f f') (eq-pair-eq-fiber p) ＝ eq-pair-eq-fiber (ap (f' a) p) +-- ap-map-Σ-eq-fiber x .x refl = refl + +-- -- ap-map-Σ-eq-fiber' : +-- -- {a : A} (x y : A' a) (p : x ＝ y) → +-- -- ap (map-Σ B' f f') (eq-pair-eq-fiber p) ＝ eq-pair-eq-fiber (ap (f' a) p) +-- -- ap-map-Σ-eq-fiber' {a} x y p = +-- -- compute-ap-eq-pair-Σ (map-Σ B' f f') refl p ∙ +-- -- ap-comp (pair (f a)) (f' a) p +-- module _ +-- {l1 l2 l3 l4 l5 l6 : Level} +-- {A : UU l1} {B : UU l2} {C : UU l3} +-- {A' : A → UU l4} {B' : B → UU l5} {C' : C → UU l6} +-- {f : A → B} {g : B → C} +-- (f' : (a : A) → A' a → B' (f a)) +-- (g' : (b : B) → B' b → C' (g b)) +-- (sA : (a : A) → A' a) (sB : (b : B) → B' b) (sC : (c : C) → C' c) +-- (F : (a : A) → f' a (sA a) ＝ sB (f a)) (G : (b : B) → g' b (sB b) ＝ sC (g b)) +-- where + +-- pasting-horizontal-comp : +-- pasting-horizontal-coherence-square-maps f g +-- ( map-section-family sA) (map-section-family sB) (map-section-family sC) +-- ( tot-map-over f f') (tot-map-over g g') +-- ( eq-pair-eq-fiber ∘ F) +-- ( eq-pair-eq-fiber ∘ G) ~ +-- eq-pair-eq-fiber ∘ +-- ((g' _) ·l F ∙h G ·r f) +-- pasting-horizontal-comp a = +-- ap +-- ( _∙ eq-pair-eq-fiber (G (f a))) +-- ( inv (ap-comp (tot-map-over g g') (pair (f a)) (F a)) ∙ +-- ap-comp (pair (g (f a))) (g' (f a)) (F a)) ∙ +-- inv (ap-concat (pair (g (f a))) (ap (g' (f a)) (F a)) (G (f a))) + +-- module _ +-- {l1 l2 l3 l4 : Level} +-- {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} +-- {f g : A → B} {f' g' : X → Y} +-- (top : f' ~ g') (bottom : f ~ g) +-- {hA : X → A} {hB : Y → B} +-- (N : f ∘ hA ~ hB ∘ f') (F : g ∘ hA ~ hB ∘ g') +-- where + +-- hom-htpy : UU (l2 ⊔ l3) +-- hom-htpy = N ∙h (hB ·l top) ~ (bottom ·r hA) ∙h F + +-- -- module _ +-- -- where + +-- -- alt-map-coherence-square-homotopies + +-- module _ +-- {l1 l2 l3 l4 l5 l6 : Level} +-- {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {V : UU l5} {W : UU l6} +-- {f g : A → B} {f' g' : X → Y} {f'' g'' : V → W} +-- (mid : f' ~ g') (bottom : f ~ g) (top : f'' ~ g'') +-- {hA : X → A} {hB : Y → B} {hA' : V → X} {hB' : W → Y} +-- (bottom-N : f ∘ hA ~ hB ∘ f') (bottom-F : g ∘ hA ~ hB ∘ g') +-- (top-N : f' ∘ hA' ~ hB' ∘ f'') (top-F : g' ∘ hA' ~ hB' ∘ g'') +-- where + +-- pasting-vertical-hom-htpy : +-- hom-htpy mid bottom {hB = hB} bottom-N bottom-F → +-- hom-htpy top mid {hB = hB'} top-N top-F → +-- hom-htpy top bottom {hB = hB ∘ hB'} +-- ( pasting-vertical-coherence-square-maps f'' hA' hB' f' hA hB f +-- top-N bottom-N) +-- ( pasting-vertical-coherence-square-maps g'' hA' hB' g' hA hB g +-- top-F bottom-F) +-- pasting-vertical-hom-htpy α β = +-- left-whisker-concat-coherence-square-homotopies +-- ( bottom-N ·r hA') +-- ( hB ·l mid ·r hA') +-- ( hB ·l top-N) +-- ( hB ·l top-F) +-- ( (hB ∘ hB') ·l top) +-- ( left-whisker-concat-htpy (hB ·l top-N) +-- ( inv-htpy (preserves-comp-left-whisker-comp hB hB' top)) ∙h +-- map-coherence-square-homotopies hB (mid ·r hA') top-N top-F (hB' ·l top) +-- ( β)) ∙h +-- right-whisker-concat-htpy (α ·r hA') (hB ·l top-F) ∙h +-- assoc-htpy (bottom ·r (hA ∘ hA')) (bottom-F ·r hA') (hB ·l top-F) + +-- module _ +-- {l1 l2 : Level} +-- {A : UU l1} {B : UU l2} +-- {f g : A → B} (H : f ~ g) +-- where + +-- id-hom-htpy : hom-htpy H H {hA = id} {hB = id} refl-htpy refl-htpy +-- id-hom-htpy = left-unit-law-left-whisker-comp H ∙h inv-htpy-right-unit-htpy + +-- module _ +-- {l1 l2 l3 l4 : Level} +-- {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} +-- (f g : A → B) (f' g' : X → Y) +-- (bottom : f ~ g) (top : f' ~ g') +-- (hA : X → A) (hB : Y → B) +-- (N : f ∘ hA ~ hB ∘ f') (F : g ∘ hA ~ hB ∘ g') +-- (α : hom-htpy top bottom N F) +-- (hA' : X → A) (hB' : Y → B) +-- (N' : f ∘ hA' ~ hB' ∘ f') (F' : g ∘ hA' ~ hB' ∘ g') +-- (β : hom-htpy top bottom N' F') +-- (σA : hA ~ hA') (σB : hB ~ hB') +-- (γN : htpy-hom-map f f' hA hB N hA' hB' N' σA σB) +-- (γF : htpy-hom-map g g' hA hB F hA' hB' F' σA σB) +-- where + +-- nudged-α nudged-β : +-- (N ∙h (hB ·l top)) ∙h (σB ·r g') ~ +-- (f ·l σA) ∙h ((bottom ·r hA') ∙h F') +-- nudged-α = +-- right-whisker-concat-htpy α (σB ·r g') ∙h +-- assoc-htpy (bottom ·r hA) F (σB ·r g') ∙h +-- left-whisker-concat-htpy (bottom ·r hA) γF ∙h +-- right-whisker-concat-coherence-square-homotopies +-- ( f ·l σA) +-- ( bottom ·r hA) +-- ( bottom ·r hA') +-- ( g ·l σA) +-- ( λ x → nat-htpy bottom (σA x)) +-- ( F') +-- nudged-β = +-- left-whisker-concat-coherence-square-homotopies N +-- ( σB ·r f') +-- ( hB ·l top) +-- ( hB' ·l top) +-- ( σB ·r g') +-- ( λ x → inv (nat-htpy σB (top x))) ∙h +-- right-whisker-concat-htpy γN (hB' ·l top) ∙h +-- assoc-htpy (f ·l σA) N' (hB' ·l top) ∙h +-- left-whisker-concat-htpy (f ·l σA) β + +-- htpy-hom-htpy : UU (l2 ⊔ l3) +-- htpy-hom-htpy = nudged-α ~ nudged-β + +-- module _ +-- {l1 l2 l3 l4 : Level} +-- {A : UU l1} {B : UU l2} {A' : UU l3} {B' : UU l4} +-- {f' g' : A' → B'} (top : f' ~ g') +-- {f g : A → B} (bottom : f ~ g) +-- (hA : A' → A) (hB : B' → B) +-- (N : coherence-square-maps f' hA hB f) +-- (F : coherence-square-maps g' hA hB g) +-- (α : hom-htpy top bottom {hB = hB} N F) +-- where + +-- coh-section-hom-htpy : +-- (sA : section hA) (sB : section hB) +-- (sN : coherence-square-maps f (map-section hA sA) (map-section hB sB) f') +-- (sF : coherence-square-maps g (map-section hA sA) (map-section hB sB) g') +-- (β : hom-htpy bottom top {hB = map-section hB sB} sN sF) +-- (γN : +-- htpy-hom-map f f +-- ( hA ∘ map-section hA sA) (hB ∘ map-section hB sB) +-- ( pasting-vertical-coherence-square-maps f +-- ( map-section hA sA) (map-section hB sB) +-- f' hA hB f sN N) +-- id id refl-htpy +-- ( is-section-map-section hA sA) +-- ( is-section-map-section hB sB)) +-- (γF : +-- htpy-hom-map g g +-- ( hA ∘ pr1 sA) (hB ∘ pr1 sB) +-- ( pasting-vertical-coherence-square-maps g (pr1 sA) (pr1 sB) g' hA +-- hB g sF F) +-- id id refl-htpy (pr2 sA) (pr2 sB)) → +-- UU (l1 ⊔ l2) +-- coh-section-hom-htpy sA sB sN sF β = +-- htpy-hom-htpy f g f g bottom bottom +-- ( hA ∘ map-section hA sA) +-- ( hB ∘ map-section hB sB) +-- ( pasting-vertical-coherence-square-maps f map-sA map-sB f' hA hB f sN N) +-- ( pasting-vertical-coherence-square-maps g map-sA map-sB g' hA hB g sF F) +-- ( pasting-vertical-hom-htpy top bottom bottom N F sN sF α β) +-- id id refl-htpy refl-htpy (id-hom-htpy bottom) +-- ( is-section-map-section hA sA) +-- ( is-section-map-section hB sB) +-- where +-- map-sA : A → A' +-- map-sA = map-section hA sA +-- map-sB : B → B' +-- map-sB = map-section hB sB + +-- module _ +-- {l1 l2 : Level} {A : UU l1} {B : A → UU l2} +-- where + +-- compute-concat-dependent-identification-right-base-refl : +-- { x y : A} (p : x ＝ y) → +-- { x' : B x} {y' z' : B y} (p' : dependent-identification B p x' y') → +-- ( q' : y' ＝ z') → +-- concat-dependent-identification B p refl p' q' ＝ ap (λ r → tr B r x') right-unit ∙ p' ∙ q' +-- compute-concat-dependent-identification-right-base-refl refl p' q' = ap (_∙ q') (ap-id p') + +-- interchange-concat-eq-pair-Σ-left : +-- {y z : A} (q : y ＝ z) {x' y' : B y} {z' : B z} → +-- (p' : x' ＝ y') +-- (q' : dependent-identification B q y' z') → +-- eq-pair-eq-fiber p' ∙ eq-pair-Σ q q' ＝ +-- eq-pair-Σ q (ap (tr B q) p' ∙ q') +-- interchange-concat-eq-pair-Σ-left q refl q' = refl + +-- interchange-concat-eq-pair-Σ-right : +-- {x y : A} (p : x ＝ y) {x' : B x} {y' z' : B y} → +-- (p' : dependent-identification B p x' y') → +-- (q' : y' ＝ z') → +-- eq-pair-Σ p p' ∙ eq-pair-eq-fiber q' ＝ +-- eq-pair-Σ p (p' ∙ q') +-- interchange-concat-eq-pair-Σ-right p p' refl = +-- right-unit ∙ ap (eq-pair-Σ p) (inv right-unit) + +-- module _ +-- {l1 l2 l3 l4 : Level} +-- {A : UU l1} {B : UU l2} {P : A → UU l3} {Q : B → UU l4} +-- {f g : A → B} (H : f ~ g) +-- {f' : (a : A) → P a → Q (f a)} {g' : (a : A) → P a → Q (g a)} +-- (H' : htpy-over Q H (f' _) (g' _)) +-- (sA : (a : A) → P a) +-- (sB : (b : B) → Q b) +-- (F : section-map-over f (f' _) sA sB) +-- (G : section-map-over g (g' _) sA sB) +-- (α : section-htpy-over H H' sA sB F G) +-- where +-- open import foundation.embeddings + +-- _ : coh-section-hom-htpy +-- ( λ p → eq-pair-Σ (H (pr1 p)) (H' (pr2 p))) +-- ( H) +-- pr1 pr1 refl-htpy refl-htpy +-- ( λ p → ap-pr1-eq-pair-Σ (H (pr1 p)) (H' (pr2 p)) ∙ inv right-unit) +-- ( section-dependent-function sA) +-- ( section-dependent-function sB) +-- ( eq-pair-eq-fiber ∘ F) +-- ( eq-pair-eq-fiber ∘ G) +-- -- The point is that this will be `ap pr1`'d, so the α in the fiber is +-- -- projected away. This definition should probably be defined in a nicer way +-- -- to make the proof less opaque. +-- ( λ a → +-- ap (eq-pair-eq-fiber (F a) ∙_) (ap-map-section-family-lemma sB (H a)) ∙ +-- interchange-concat-eq-pair-Σ-left (H a) (F a) (apd sB (H a)) ∙ +-- ap (eq-pair-Σ (H a)) (inv (α a)) ∙ +-- inv (interchange-concat-eq-pair-Σ-right (H a) (H' (sA a)) (G a))) +-- ( λ a → right-unit ∙ ap-pr1-eq-pair-eq-fiber (F a)) +-- ( λ a → right-unit ∙ ap-pr1-eq-pair-eq-fiber (G a)) +-- _ = {!!} + +-- -- module _ +-- -- {l1 l2 l3 l4 l1' l2' l3' l4' : Level} +-- -- {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} +-- -- (f : A → B) (g : A → C) (h : B → D) (k : C → D) +-- -- {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'} +-- -- (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D') +-- -- (top : h' ∘ f' ~ k' ∘ g') +-- -- (bottom : h ∘ f ~ k ∘ g) +-- -- (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D) +-- -- (back-left : (f ∘ hA) ~ (hB ∘ f')) +-- -- (back-right : (g ∘ hA) ~ (hC ∘ g')) +-- -- (front-left : (h ∘ hB) ~ (hD ∘ h')) +-- -- (front-right : (k ∘ hC) ~ (hD ∘ k')) +-- -- (α : +-- -- coherence-cube-maps f g h k f' g' h' k' hA hB hC hD +-- -- top back-left back-right front-left front-right bottom) +-- -- (hA' : A' → A) (hB' : B' → B) (hC' : C' → C) (hD' : D' → D) +-- -- (back-left' : (f ∘ hA') ~ (hB' ∘ f')) +-- -- (back-right' : (g ∘ hA') ~ (hC' ∘ g')) +-- -- (front-left' : (h ∘ hB') ~ (hD' ∘ h')) +-- -- (front-right' : (k ∘ hC') ~ (hD' ∘ k')) +-- -- (β : +-- -- coherence-cube-maps f g h k f' g' h' k' hA' hB' hC' hD' +-- -- top back-left' back-right' front-left' front-right' bottom) +-- -- (σA : hA ~ hA') (σB : hB ~ hB') (σC : hC ~ hC') (σD : hD ~ hD') +-- -- (back-left-H : htpy-hom-map f f' hA hB back-left hA' hB' back-left' σA σB) +-- -- (back-right-H : htpy-hom-map g g' hA hC back-right hA' hC' back-right' σA σC) +-- -- (front-left-H : htpy-hom-map h h' hB hD front-left hB' hD' front-left' σB σD) +-- -- (front-right-H : htpy-hom-map k k' hC hD front-right hC' hD' front-right' σC σD) +-- -- where +-- -- open import foundation.commuting-squares-of-homotopies + +-- -- htpy-hom-square : +-- -- UU (l4 ⊔ l1') +-- -- htpy-hom-square = +-- -- htpy-hom-htpy (h ∘ f) (k ∘ g) (h' ∘ f') (k' ∘ g') bottom top hA hD +-- -- ( pasting-horizontal-coherence-square-maps f' h' hA hB hD f h back-left front-left) +-- -- ( pasting-horizontal-coherence-square-maps g' k' hA hC hD g k back-right front-right) +-- -- ( α) +-- -- hA' hD' +-- -- ( pasting-horizontal-coherence-square-maps f' h' hA' hB' hD' f h back-left' front-left') +-- -- ( pasting-horizontal-coherence-square-maps g' k' hA' hC' hD' g k back-right' front-right') +-- -- ( β) +-- -- σA σD +-- -- ( comp-htpy-hom-map f h f' h' hA hA' hB hB' hD hD' σA σB σD +-- -- back-left back-left' back-left-H +-- -- front-left front-left' front-left-H) +-- -- ( comp-htpy-hom-map g k g' k' hA hA' hC hC' hD hD' σA σC σD +-- -- back-right back-right' back-right-H +-- -- front-right front-right' front-right-H) + +-- -- module _ +-- -- {l1 l2 l3 l4 : Level} +-- -- {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} +-- -- (f : A → B) (g : A → C) (h : B → D) (k : C → D) +-- -- (H : coherence-square-maps g f k h) +-- -- where + +-- -- id-cube : +-- -- coherence-cube-maps f g h k f g h k id id id id +-- -- H refl-htpy refl-htpy refl-htpy refl-htpy H +-- -- id-cube = left-unit-law-left-whisker-comp H ∙h inv-htpy-right-unit-htpy + +-- -- module _ +-- -- {l1 l2 l3 l4 l1' l2' l3' l4' : Level} +-- -- {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} +-- -- (f : A → B) (g : A → C) (h : B → D) (k : C → D) +-- -- {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'} +-- -- (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D') +-- -- (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D) +-- -- (top : (h' ∘ f') ~ (k' ∘ g')) +-- -- (back-left : (f ∘ hA) ~ (hB ∘ f')) +-- -- (back-right : (g ∘ hA) ~ (hC ∘ g')) +-- -- (front-left : (h ∘ hB) ~ (hD ∘ h')) +-- -- (front-right : (k ∘ hC) ~ (hD ∘ k')) +-- -- (bottom : (h ∘ f) ~ (k ∘ g)) +-- -- (α : +-- -- coherence-cube-maps f g h k f' g' h' k' hA hB hC hD +-- -- top back-left back-right front-left front-right bottom) +-- -- where + +-- -- section-displayed-cube-over : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l1' ⊔ l2' ⊔ l3' ⊔ l4') +-- -- section-displayed-cube-over = +-- -- Σ ( section-displayed-map-over f f' hA hB back-left) +-- -- ( λ sF → +-- -- Σ ( section-displayed-map-over k k' hC hD front-right) +-- -- ( λ sK → +-- -- Σ ( coherence-square-maps g +-- -- ( map-section hA (pr1 sF)) +-- -- ( map-section hC (pr1 sK)) +-- -- ( g')) +-- -- ( λ G → +-- -- Σ ( htpy-hom-map g g +-- -- ( hA ∘ map-section hA (pr1 sF)) +-- -- ( hC ∘ map-section hC (pr1 sK)) +-- -- ( pasting-vertical-coherence-square-maps g +-- -- ( map-section hA (pr1 sF)) +-- -- ( map-section hC (pr1 sK)) +-- -- g' hA hC g +-- -- G back-right) +-- -- id id refl-htpy +-- -- ( is-section-map-section hA (pr1 sF)) +-- -- ( is-section-map-section hC (pr1 sK))) +-- -- ( λ sG → +-- -- Σ ( coherence-square-maps h +-- -- ( map-section hB (pr1 (pr2 sF))) +-- -- ( map-section hD (pr1 (pr2 sK))) +-- -- ( h')) +-- -- ( λ H → +-- -- Σ ( htpy-hom-map h h +-- -- ( hB ∘ map-section hB (pr1 (pr2 sF))) +-- -- ( hD ∘ map-section hD (pr1 (pr2 sK))) +-- -- ( pasting-vertical-coherence-square-maps h +-- -- ( map-section hB (pr1 (pr2 sF))) +-- -- ( map-section hD (pr1 (pr2 sK))) +-- -- h' hB hD h +-- -- H front-left) +-- -- id id refl-htpy +-- -- ( is-section-map-section hB (pr1 (pr2 sF))) +-- -- ( is-section-map-section hD (pr1 (pr2 sK)))) +-- -- ( λ sH → +-- -- Σ ( coherence-cube-maps f' g' h' k' f g h k +-- -- ( map-section hA (pr1 sF)) +-- -- ( map-section hB (pr1 (pr2 sF))) +-- -- ( map-section hC (pr1 sK)) +-- -- ( map-section hD (pr1 (pr2 sK))) +-- -- ( bottom) +-- -- ( pr1 (pr2 (pr2 sF))) +-- -- ( G) +-- -- ( H) +-- -- ( pr1 (pr2 (pr2 sK))) +-- -- ( top)) +-- -- ( λ β → +-- -- htpy-hom-square f g h k f g h k bottom bottom +-- -- ( hA ∘ map-section hA (pr1 sF)) +-- -- ( hB ∘ map-section hB (pr1 (pr2 sF))) +-- -- ( hC ∘ map-section hC (pr1 sK)) +-- -- ( hD ∘ map-section hD (pr1 (pr2 sK))) +-- -- ( pasting-vertical-coherence-square-maps f +-- -- ( map-section hA (pr1 sF)) +-- -- ( map-section hB (pr1 (pr2 sF))) +-- -- f' hA hB f +-- -- ( pr1 (pr2 (pr2 sF))) +-- -- ( back-left)) +-- -- ( pasting-vertical-coherence-square-maps g +-- -- ( map-section hA (pr1 sF)) +-- -- ( map-section hC (pr1 sK)) +-- -- g' hA hC g +-- -- ( G) +-- -- ( back-right)) +-- -- ( pasting-vertical-coherence-square-maps h +-- -- ( map-section hB (pr1 (pr2 sF))) +-- -- ( map-section hD (pr1 (pr2 sK))) +-- -- h' hB hD h +-- -- ( H) +-- -- ( front-left)) +-- -- ( pasting-vertical-coherence-square-maps k +-- -- ( map-section hC (pr1 sK)) +-- -- ( map-section hD (pr1 (pr2 sK))) +-- -- k' hC hD k +-- -- ( pr1 (pr2 (pr2 sK))) +-- -- ( front-right)) +-- -- ( pasting-vertical-coherence-cube-maps f g h k +-- -- f' g' h' k' f g h k +-- -- hA hB hC hD +-- -- ( map-section hA (pr1 sF)) +-- -- ( map-section hB (pr1 (pr2 sF))) +-- -- ( map-section hC (pr1 sK)) +-- -- ( map-section hD (pr1 (pr2 sK))) +-- -- ( top) +-- -- back-left back-right front-left front-right bottom +-- -- ( bottom) +-- -- ( pr1 (pr2 (pr2 sF))) +-- -- ( G) +-- -- ( H) +-- -- ( pr1 (pr2 (pr2 sK))) +-- -- ( α) +-- -- ( β)) +-- -- id id id id +-- -- refl-htpy refl-htpy refl-htpy refl-htpy +-- -- ( id-cube f g h k bottom) +-- -- ( is-section-map-section hA (pr1 sF)) +-- -- ( is-section-map-section hB (pr1 (pr2 sF))) +-- -- ( is-section-map-section hC (pr1 sK)) +-- -- ( is-section-map-section hD (pr1 (pr2 sK))) +-- -- ( pr2 (pr2 (pr2 sF))) +-- -- ( sG) +-- -- ( sH) +-- -- ( pr2 (pr2 (pr2 sK)))))))))) + +-- -- module _ +-- -- {l1 l2 l3 l4 l5 l6 l7 l8 : Level} +-- -- {P1 : UU l1} {P2 : UU l2} {P3 : UU l3} {P4 : UU l4} +-- -- {Q1 : P1 → UU l5} {Q2 : P2 → UU l6} {Q3 : P3 → UU l7} {Q4 : P4 → UU l8} +-- -- (g1 : P1 → P3) (f1 : P1 → P2) (f2 : P3 → P4) (g2 : P2 → P4) +-- -- (g1' : (p : P1) → Q1 p → Q3 (g1 p)) +-- -- (f1' : (p : P1) → Q1 p → Q2 (f1 p)) +-- -- (f2' : (p : P3) → Q3 p → Q4 (f2 p)) +-- -- (g2' : (p : P2) → Q2 p → Q4 (g2 p)) +-- -- (bottom : g2 ∘ f1 ~ f2 ∘ g1) +-- -- (top : square-over g1 f1 f2 g2 (g1' _) (f1' _) (f2' _) (g2' _) bottom) +-- -- where + +-- -- tot-square-over : +-- -- coherence-square-maps +-- -- ( tot-map-over g1 g1') +-- -- ( tot-map-over f1 f1') +-- -- ( tot-map-over {B' = Q4} f2 f2') +-- -- ( tot-map-over g2 g2') +-- -- tot-square-over = +-- -- coherence-square-maps-Σ Q4 g1' f1' f2' g2' (λ p → top {p}) + +-- -- coh-tot-square-over : +-- -- coherence-cube-maps f1 g1 g2 f2 +-- -- ( map-Σ Q2 f1 f1') +-- -- ( map-Σ Q3 g1 g1') +-- -- ( map-Σ Q4 g2 g2') +-- -- ( map-Σ Q4 f2 f2') +-- -- pr1 pr1 pr1 pr1 +-- -- ( tot-square-over) +-- -- refl-htpy refl-htpy refl-htpy refl-htpy +-- -- ( bottom) +-- -- coh-tot-square-over (p , q) = +-- -- ap-pr1-eq-pair-Σ (bottom p) (top q) ∙ inv right-unit + +-- -- module _ +-- -- (s1 : (p : P1) → Q1 p) (s2 : (p : P2) → Q2 p) +-- -- (s3 : (p : P3) → Q3 p) (s4 : (p : P4) → Q4 p) +-- -- (G1 : (p : P1) → g1' p (s1 p) ＝ s3 (g1 p)) +-- -- (F1 : (p : P1) → f1' p (s1 p) ＝ s2 (f1 p)) +-- -- (F2 : (p : P3) → f2' p (s3 p) ＝ s4 (f2 p)) +-- -- (G2 : (p : P2) → g2' p (s2 p) ＝ s4 (g2 p)) +-- -- where +-- -- open import foundation.action-on-identifications-binary-functions + +-- -- lemma : +-- -- pasting-vertical-coherence-square-maps g1 +-- -- ( map-section-family s1) (map-section-family s3) +-- -- ( tot-map-over g1 g1') (tot-map-over f1 f1') +-- -- ( tot-map-over {B' = Q4} f2 f2') (tot-map-over g2 g2') +-- -- ( eq-pair-eq-fiber ∘ G1) +-- -- ( coherence-square-maps-Σ Q4 g1' f1' f2' g2' (λ p → top {p})) ~ +-- -- ( λ p → eq-pair-Σ (bottom p) (top (s1 p) ∙ ap (f2' (g1 p)) (G1 p))) +-- -- lemma = λ p → ap +-- -- ( eq-pair-Σ (bottom p) (top (s1 p)) ∙_) +-- -- ( [i] p) ∙ +-- -- ( inv (concat-vertical-eq-pair (bottom p) (top (s1 p)) (ap (f2' (g1 p)) (G1 p)))) +-- -- where +-- -- [i] = +-- -- λ (p : P1) → +-- -- inv (ap-comp (map-Σ Q4 f2 f2') (pair (g1 p)) (G1 p)) ∙ +-- -- ap-comp (pair (f2 (g1 p))) (f2' (g1 p)) (G1 p) + +-- -- section-cube-over-sect-square-over : +-- -- section-square-over g1 f1 f2 g2 +-- -- ( g1' _) (f1' _) (f2' _) (g2' _) +-- -- s1 s2 s3 s4 +-- -- G1 F1 F2 G2 +-- -- bottom top → +-- -- section-displayed-cube-over f1 g1 g2 f2 +-- -- ( tot-map-over f1 f1') +-- -- ( tot-map-over g1 g1') +-- -- ( tot-map-over g2 g2') +-- -- ( tot-map-over f2 f2') +-- -- pr1 pr1 pr1 pr1 +-- -- ( coherence-square-maps-Σ Q4 g1' f1' f2' g2' (λ p → top {p})) +-- -- refl-htpy refl-htpy refl-htpy refl-htpy +-- -- ( bottom) +-- -- ( coh-tot-square-over) +-- -- pr1 (section-cube-over-sect-square-over α) = +-- -- ( section-dependent-function s1) , +-- -- ( section-dependent-function s2) , +-- -- ( eq-pair-eq-fiber ∘ F1) , +-- -- ( λ p → right-unit ∙ ap-pr1-eq-pair-Σ refl (F1 p)) +-- -- pr1 (pr2 (section-cube-over-sect-square-over α)) = +-- -- ( section-dependent-function s3) , +-- -- ( section-dependent-function s4) , +-- -- ( eq-pair-eq-fiber ∘ F2) , +-- -- ( λ p → right-unit ∙ ap-pr1-eq-pair-Σ refl (F2 p)) +-- -- pr2 (pr2 (section-cube-over-sect-square-over α)) = +-- -- ( eq-pair-eq-fiber ∘ G1) , +-- -- ( λ p → right-unit ∙ ap-pr1-eq-pair-Σ refl (G1 p)) , +-- -- ( eq-pair-eq-fiber ∘ G2) , +-- -- ( λ p → right-unit ∙ ap-pr1-eq-pair-Σ refl (G2 p)) , +-- -- ( λ p → +-- -- ap-binary +-- -- ( _∙_) +-- -- ( pasting-horizontal-comp f1' g2' s1 s2 s4 F1 G2 p) +-- -- ( ap-map-section-family-lemma s4 (bottom p)) ∙ +-- -- {!!} ∙ +-- -- ap (eq-pair-Σ (bottom p)) (inv (α p) ∙ assoc (top (s1 p)) (ap (f2' (g1 p)) (G1 p)) (F2 (g1 p))) ∙ +-- -- concat-vertical-eq-pair +-- -- ( bottom p) +-- -- ( top (s1 p)) +-- -- ( ap (f2' (g1 p)) (G1 p) ∙ F2 (g1 p)) ∙ +-- -- ap-binary +-- -- ( _∙_) +-- -- ( refl {x = eq-pair-Σ (bottom p) (top (s1 p))}) +-- -- ( inv (pasting-horizontal-comp g1' f2' s1 s3 s4 G1 F2 p))) , +-- -- {!!} +-- -- ``` diff --git a/src/synthetic-homotopy-theory/zigzag-construction-identity-type-pushouts.lagda.md b/src/synthetic-homotopy-theory/zigzag-construction-identity-type-pushouts.lagda.md new file mode 100644 index 0000000000..80ac2fa11e --- /dev/null +++ b/src/synthetic-homotopy-theory/zigzag-construction-identity-type-pushouts.lagda.md @@ -0,0 +1,1235 @@ +# The zigzag construction of identity types of pushouts + +```agda +{-# OPTIONS --lossy-unification #-} + +module synthetic-homotopy-theory.zigzag-construction-identity-type-pushouts where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-dependent-functions +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.commuting-squares-of-homotopies +open import foundation.commuting-squares-of-maps +open import foundation.dependent-identifications +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.empty-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.homotopy-algebra +open import foundation.identity-types +open import foundation.raising-universe-levels +open import foundation.span-diagrams +open import foundation.transport-along-identifications +open import foundation.transposition-identifications-along-equivalences +open import foundation.unit-type +open import foundation.universe-levels +open import foundation.whiskering-higher-homotopies-composition +open import foundation.whiskering-homotopies-composition + +open import synthetic-homotopy-theory.cocones-under-spans +open import synthetic-homotopy-theory.dependent-cocones-under-sequential-diagrams +open import synthetic-homotopy-theory.dependent-cocones-under-spans +open import synthetic-homotopy-theory.dependent-universal-property-sequential-colimits +open import synthetic-homotopy-theory.descent-data-pushouts +open import synthetic-homotopy-theory.families-descent-data-pushouts +open import synthetic-homotopy-theory.flattening-lemma-pushouts +open import synthetic-homotopy-theory.functoriality-sequential-colimits +open import synthetic-homotopy-theory.functoriality-stuff +open import synthetic-homotopy-theory.identity-systems-descent-data-pushouts +open import synthetic-homotopy-theory.pushouts +open import synthetic-homotopy-theory.sections-descent-data-pushouts +open import synthetic-homotopy-theory.sequential-colimits +open import synthetic-homotopy-theory.sequential-diagrams +open import synthetic-homotopy-theory.shifts-sequential-diagrams +open import synthetic-homotopy-theory.stuff-over +open import synthetic-homotopy-theory.universal-property-pushouts +open import synthetic-homotopy-theory.zigzags-sequential-diagrams +``` + +
+ +## Idea + +The identity types of pushouts may be characterized as certain sequential +colimits of pushouts. + +## Definitions + +```agda +module _ + {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) + where + + type-stage-zigzag-construction-id-pushout : ℕ → UU (lsuc (l1 ⊔ l2 ⊔ l3)) + type-stage-zigzag-construction-id-pushout n = + Σ ( codomain-span-diagram 𝒮 → UU (l1 ⊔ l2 ⊔ l3)) + ( λ Path-to-b → + Σ ( domain-span-diagram 𝒮 → UU (l1 ⊔ l2 ⊔ l3)) + ( λ Path-to-a → + ( Σ ( (s : spanning-type-span-diagram 𝒮) → + Path-to-b (right-map-span-diagram 𝒮 s) → + Path-to-a (left-map-span-diagram 𝒮 s)) + ( λ _ → + rec-ℕ + ( raise-unit (lsuc (l1 ⊔ l2 ⊔ l3))) + ( λ _ _ → + ( codomain-span-diagram 𝒮 → + span-diagram + ( l1 ⊔ l2 ⊔ l3) + ( l1 ⊔ l2 ⊔ l3) + ( l1 ⊔ l2 ⊔ l3)) × + ( domain-span-diagram 𝒮 → + span-diagram + ( l1 ⊔ l2 ⊔ l3) + ( l1 ⊔ l2 ⊔ l3) + ( l1 ⊔ l2 ⊔ l3))) + ( n))))) + +module _ + {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) + (a₀ : domain-span-diagram 𝒮) + where + + stage-zigzag-construction-id-pushout : + (n : ℕ) → type-stage-zigzag-construction-id-pushout 𝒮 n + stage-zigzag-construction-id-pushout zero-ℕ = + Path-to-b , + Path-to-a , + ( λ s → raise-ex-falso _) , + raise-star + where + Path-to-b : codomain-span-diagram 𝒮 → UU (l1 ⊔ l2 ⊔ l3) + Path-to-b _ = raise-empty _ + Path-to-a : domain-span-diagram 𝒮 → UU (l1 ⊔ l2 ⊔ l3) + Path-to-a a = raise (l2 ⊔ l3) (a₀ ＝ a) + stage-zigzag-construction-id-pushout (succ-ℕ n) = + Path-to-b , + Path-to-a , + ( λ s p → inr-pushout _ _ (s , refl , p)) , + span-diagram-B , + span-diagram-A + where + span-diagram-B : + codomain-span-diagram 𝒮 → + span-diagram (l1 ⊔ l2 ⊔ l3) (l1 ⊔ l2 ⊔ l3) (l1 ⊔ l2 ⊔ l3) + span-diagram-B b = + make-span-diagram + ( pr2 ∘ pr2) + ( tot + ( λ s → + tot + ( λ r (p : pr1 (stage-zigzag-construction-id-pushout n) b) → + pr1 + ( pr2 (pr2 (stage-zigzag-construction-id-pushout n))) + ( s) + ( tr (pr1 (stage-zigzag-construction-id-pushout n)) r p)))) + Path-to-b : codomain-span-diagram 𝒮 → UU (l1 ⊔ l2 ⊔ l3) + Path-to-b b = standard-pushout (span-diagram-B b) + span-diagram-A : + domain-span-diagram 𝒮 → + span-diagram (l1 ⊔ l2 ⊔ l3) (l1 ⊔ l2 ⊔ l3) (l1 ⊔ l2 ⊔ l3) + span-diagram-A a = + make-span-diagram + ( pr2 ∘ pr2) + ( tot + ( λ s → + tot + ( λ r (p : pr1 (pr2 (stage-zigzag-construction-id-pushout n)) a) → + inr-standard-pushout + ( span-diagram-B (right-map-span-diagram 𝒮 s)) + ( ( s) , + ( refl) , + ( tr + ( pr1 (pr2 (stage-zigzag-construction-id-pushout n))) + ( r) + ( p)))))) + Path-to-a : domain-span-diagram 𝒮 → UU (l1 ⊔ l2 ⊔ l3) + Path-to-a a = standard-pushout (span-diagram-A a) + + span-diagram-path-to-b : + codomain-span-diagram 𝒮 → ℕ → + span-diagram + ( l1 ⊔ l2 ⊔ l3) + ( l1 ⊔ l2 ⊔ l3) + ( l1 ⊔ l2 ⊔ l3) + span-diagram-path-to-b b n = + pr1 (pr2 (pr2 (pr2 (stage-zigzag-construction-id-pushout (succ-ℕ n))))) b + + span-diagram-path-to-a : + domain-span-diagram 𝒮 → ℕ → + span-diagram + ( l1 ⊔ l2 ⊔ l3) + ( l1 ⊔ l2 ⊔ l3) + ( l1 ⊔ l2 ⊔ l3) + span-diagram-path-to-a a n = + pr2 (pr2 (pr2 (pr2 (stage-zigzag-construction-id-pushout (succ-ℕ n))))) a + + Path-to-b : codomain-span-diagram 𝒮 → ℕ → UU (l1 ⊔ l2 ⊔ l3) + Path-to-b b n = pr1 (stage-zigzag-construction-id-pushout n) b + + Path-to-a : domain-span-diagram 𝒮 → ℕ → UU (l1 ⊔ l2 ⊔ l3) + Path-to-a a n = pr1 (pr2 (stage-zigzag-construction-id-pushout n)) a + + inl-Path-to-b : + (b : codomain-span-diagram 𝒮) (n : ℕ) → Path-to-b b n → Path-to-b b (succ-ℕ n) + inl-Path-to-b b n = + inl-standard-pushout + ( span-diagram-path-to-b b n) + + inl-Path-to-a : + (a : domain-span-diagram 𝒮) (n : ℕ) → Path-to-a a n → Path-to-a a (succ-ℕ n) + inl-Path-to-a a n = + inl-standard-pushout + ( span-diagram-path-to-a a n) + + concat-inv-s : + (s : spanning-type-span-diagram 𝒮) → + (n : ℕ) → + Path-to-b (right-map-span-diagram 𝒮 s) n → + Path-to-a (left-map-span-diagram 𝒮 s) n + concat-inv-s s n = pr1 (pr2 (pr2 (stage-zigzag-construction-id-pushout n))) s + + concat-s : + (s : spanning-type-span-diagram 𝒮) → + (n : ℕ) → + Path-to-a (left-map-span-diagram 𝒮 s) n → + Path-to-b (right-map-span-diagram 𝒮 s) (succ-ℕ n) + concat-s s n p = + inr-standard-pushout + ( span-diagram-path-to-b (right-map-span-diagram 𝒮 s) n) + ( s , refl , p) + + right-sequential-diagram-zigzag-id-pushout : + codomain-span-diagram 𝒮 → + sequential-diagram (l1 ⊔ l2 ⊔ l3) + pr1 (right-sequential-diagram-zigzag-id-pushout b) = Path-to-b b + pr2 (right-sequential-diagram-zigzag-id-pushout b) = inl-Path-to-b b + + left-sequential-diagram-zigzag-id-pushout : + domain-span-diagram 𝒮 → + sequential-diagram (l1 ⊔ l2 ⊔ l3) + pr1 (left-sequential-diagram-zigzag-id-pushout a) = Path-to-a a + pr2 (left-sequential-diagram-zigzag-id-pushout a) = inl-Path-to-a a + + zigzag-sequential-diagram-zigzag-id-pushout : + (s : spanning-type-span-diagram 𝒮) → + zigzag-sequential-diagram + ( left-sequential-diagram-zigzag-id-pushout + ( left-map-span-diagram 𝒮 s)) + ( shift-once-sequential-diagram + ( right-sequential-diagram-zigzag-id-pushout + ( right-map-span-diagram 𝒮 s))) + pr1 (zigzag-sequential-diagram-zigzag-id-pushout s) = + concat-s s + pr1 (pr2 (zigzag-sequential-diagram-zigzag-id-pushout s)) n = + concat-inv-s s (succ-ℕ n) + pr1 (pr2 (pr2 (zigzag-sequential-diagram-zigzag-id-pushout s))) n p = + glue-standard-pushout + ( span-diagram-path-to-a (left-map-span-diagram 𝒮 s) n) + ( s , refl , p) + pr2 (pr2 (pr2 (zigzag-sequential-diagram-zigzag-id-pushout s))) n p = + glue-standard-pushout + ( span-diagram-path-to-b (right-map-span-diagram 𝒮 s) (succ-ℕ n)) + ( s , refl , p) + + left-id-pushout : domain-span-diagram 𝒮 → UU (l1 ⊔ l2 ⊔ l3) + left-id-pushout a = + standard-sequential-colimit (left-sequential-diagram-zigzag-id-pushout a) + + refl-id-pushout : left-id-pushout a₀ + refl-id-pushout = + map-cocone-standard-sequential-colimit 0 (map-raise refl) + + right-id-pushout : codomain-span-diagram 𝒮 → UU (l1 ⊔ l2 ⊔ l3) + right-id-pushout b = + standard-sequential-colimit (right-sequential-diagram-zigzag-id-pushout b) + + equiv-id-pushout : + (s : spanning-type-span-diagram 𝒮) → + left-id-pushout (left-map-span-diagram 𝒮 s) ≃ + right-id-pushout (right-map-span-diagram 𝒮 s) + equiv-id-pushout s = + equiv-colimit-zigzag-sequential-diagram _ _ + ( up-standard-sequential-colimit) + ( up-shift-cocone-sequential-diagram 1 up-standard-sequential-colimit) + ( zigzag-sequential-diagram-zigzag-id-pushout s) + + -- concat-inv-s-inf : + -- (s : spanning-type-span-diagram 𝒮) → + -- right-id-pushout (right-map-span-diagram 𝒮 s) → + -- left-id-pushout (left-map-span-diagram 𝒮 s) + -- concat-inv-s-inf s = + -- map-inv-equiv (equiv-id-pushout s) + + concat-s-inf : + (s : spanning-type-span-diagram 𝒮) → + left-id-pushout (left-map-span-diagram 𝒮 s) → + right-id-pushout (right-map-span-diagram 𝒮 s) + concat-s-inf s = + map-equiv (equiv-id-pushout s) + + descent-data-zigzag-id-pushout : descent-data-pushout 𝒮 (l1 ⊔ l2 ⊔ l3) + pr1 descent-data-zigzag-id-pushout = left-id-pushout + pr1 (pr2 descent-data-zigzag-id-pushout) = right-id-pushout + pr2 (pr2 descent-data-zigzag-id-pushout) = equiv-id-pushout +``` + +## Theorem + +### TODO + +```agda +apd-lemma : + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + (f : (a : A) → B a) (g : (a : A) → B a → C a) {x y : A} (p : x ＝ y) → + apd (λ a → g a (f a)) p ＝ inv (preserves-tr g p (f x)) ∙ ap (g y) (apd f p) +apd-lemma f g refl = refl + +lem : + {l : Level} {X : UU l} {x y z u v : X} → + (p : y ＝ x) (q : y ＝ z) (r : z ＝ u) (s : x ＝ v) (t : u ＝ v) → + (inv p ∙ (q ∙ r) ＝ s ∙ inv t) → q ∙ r ∙ t ＝ p ∙ s +lem refl q r refl refl x = right-unit ∙ x + +module _ + {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} + {X : UU l4} {c : cocone-span-diagram 𝒮 X} + (up-c : universal-property-pushout _ _ c) + (a₀ : domain-span-diagram 𝒮) + where + + module _ + {l5 : Level} + (R : descent-data-pushout + ( span-diagram-flattening-descent-data-pushout + ( descent-data-zigzag-id-pushout 𝒮 a₀)) + ( l5)) + (r₀ : left-family-descent-data-pushout R (a₀ , refl-id-pushout 𝒮 a₀)) + where + + private + CB : + (s : spanning-type-span-diagram 𝒮) → + (n : ℕ) → + (p : Path-to-a 𝒮 a₀ (left-map-span-diagram 𝒮 s) n) → + concat-s-inf 𝒮 a₀ s + ( map-cocone-standard-sequential-colimit n p) ＝ + map-cocone-standard-sequential-colimit (succ-ℕ n) + ( concat-s 𝒮 a₀ s n p) + CB s = + htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram + ( up-standard-sequential-colimit) + ( shift-once-cocone-sequential-diagram + ( cocone-standard-sequential-colimit + ( right-sequential-diagram-zigzag-id-pushout 𝒮 a₀ (right-map-span-diagram 𝒮 s)))) + ( hom-diagram-zigzag-sequential-diagram + ( zigzag-sequential-diagram-zigzag-id-pushout 𝒮 a₀ s)) + + Ψ : + (s : spanning-type-span-diagram 𝒮) → + (n : ℕ) → + (p : Path-to-a 𝒮 a₀ (left-map-span-diagram 𝒮 s) n) → + left-family-descent-data-pushout R + ( left-map-span-diagram 𝒮 s , map-cocone-standard-sequential-colimit n p) → + right-family-descent-data-pushout R + ( right-map-span-diagram 𝒮 s , map-cocone-standard-sequential-colimit (succ-ℕ n) (concat-s 𝒮 a₀ s n p)) + Ψ s = + map-over-diagram-equiv-over-colimit + ( up-standard-sequential-colimit) + ( shift-once-cocone-sequential-diagram + ( cocone-standard-sequential-colimit _)) + ( hom-diagram-zigzag-sequential-diagram + ( zigzag-sequential-diagram-zigzag-id-pushout 𝒮 a₀ s)) + ( ev-pair + ( left-family-descent-data-pushout R) + ( left-map-span-diagram 𝒮 s)) + ( ev-pair + ( right-family-descent-data-pushout R) + ( right-map-span-diagram 𝒮 s)) + ( ev-pair + ( equiv-family-descent-data-pushout R) + ( s)) + -- ( tr + -- ( ev-pair (right-family-descent-data-pushout R) (right-map-span-diagram 𝒮 s)) + -- ( CB s n p)) ∘ + -- ( map-family-descent-data-pushout R + -- ( s , map-cocone-standard-sequential-colimit n p)) + + opaque + -- The definitions currently matter for α and β + -- Φ : + -- (s : spanning-type-span-diagram 𝒮) → + -- (n : ℕ) → + -- (p : Path-to-b 𝒮 a₀ (right-map-span-diagram 𝒮 s) (succ-ℕ n)) → + -- right-family-descent-data-pushout R + -- ( right-map-span-diagram 𝒮 s , map-cocone-standard-sequential-colimit (succ-ℕ n) p) → + -- right-family-descent-data-pushout R + -- ( right-map-span-diagram 𝒮 s , + -- concat-s-inf 𝒮 a₀ s (map-cocone-standard-sequential-colimit (succ-ℕ n) (concat-inv-s 𝒮 a₀ s (succ-ℕ n) p))) + -- Φ s n p = + -- ( tr + -- ( ev-pair (right-family-descent-data-pushout R) (right-map-span-diagram 𝒮 s)) + -- ( inv (CB s (succ-ℕ n) (concat-inv-s 𝒮 a₀ s (succ-ℕ n) p)))) ∘ + -- ( tr + -- ( λ p → + -- right-family-descent-data-pushout R + -- ( right-map-span-diagram 𝒮 s , map-cocone-standard-sequential-colimit (succ-ℕ (succ-ℕ n)) p)) + -- ( glue-pushout _ _ (s , refl , p))) ∘ + -- ( tr + -- ( ev-pair (right-family-descent-data-pushout R) (right-map-span-diagram 𝒮 s)) + -- ( coherence-cocone-standard-sequential-colimit (succ-ℕ n) p)) + + Φ' : + (s : spanning-type-span-diagram 𝒮) → + (n : ℕ) → + (p : Path-to-b 𝒮 a₀ (right-map-span-diagram 𝒮 s) (succ-ℕ n)) → + right-family-descent-data-pushout R + ( right-map-span-diagram 𝒮 s , map-cocone-standard-sequential-colimit (succ-ℕ n) p) → + left-family-descent-data-pushout R + ( left-map-span-diagram 𝒮 s , map-cocone-standard-sequential-colimit (succ-ℕ n) (concat-inv-s 𝒮 a₀ s (succ-ℕ n) p)) + Φ' s = + inv-map-over-diagram-equiv-zigzag + ( up-standard-sequential-colimit) + ( shift-once-cocone-sequential-diagram + ( cocone-standard-sequential-colimit _)) + ( zigzag-sequential-diagram-zigzag-id-pushout 𝒮 a₀ s) + ( ev-pair + ( left-family-descent-data-pushout R) + ( left-map-span-diagram 𝒮 s)) + ( ev-pair + ( right-family-descent-data-pushout R) + ( right-map-span-diagram 𝒮 s)) + ( ev-pair + ( equiv-family-descent-data-pushout R) + ( s)) + + -- coh-dep-cocone-a : + -- (s : spanning-type-span-diagram 𝒮) (n : ℕ) → + -- (p : Path-to-a 𝒮 a₀ (left-map-span-diagram 𝒮 s) n) → + -- coherence-square-maps + -- ( ( tr + -- ( λ p → + -- left-family-descent-data-pushout R + -- ( left-map-span-diagram 𝒮 s , + -- map-cocone-standard-sequential-colimit (succ-ℕ n) p)) + -- ( glue-pushout _ _ (s , refl , p))) ∘ + -- ( tr + -- ( ev-pair + -- ( left-family-descent-data-pushout R) + -- ( left-map-span-diagram 𝒮 s)) + -- ( coherence-cocone-standard-sequential-colimit n p))) + -- ( map-family-descent-data-pushout R + -- ( s , map-cocone-standard-sequential-colimit n p)) + -- ( map-family-descent-data-pushout R + -- ( s , + -- map-cocone-standard-sequential-colimit (succ-ℕ n) + -- ( concat-inv-s 𝒮 a₀ s (succ-ℕ n) ( concat-s 𝒮 a₀ s n p)))) + -- ( ( tr + -- ( ev-pair + -- ( right-family-descent-data-pushout R) + -- ( right-map-span-diagram 𝒮 s)) + -- ( inv (CB s (succ-ℕ n) (concat-inv-s 𝒮 a₀ s (succ-ℕ n) (concat-s 𝒮 a₀ s n p))))) ∘ + -- ( tr + -- ( λ p → + -- right-family-descent-data-pushout R + -- ( right-map-span-diagram 𝒮 s , + -- map-cocone-standard-sequential-colimit (succ-ℕ (succ-ℕ n)) p)) + -- ( glue-pushout _ _ (s , refl , concat-s 𝒮 a₀ s n p))) ∘ + -- ( tr + -- ( ev-pair + -- ( right-family-descent-data-pushout R) + -- ( right-map-span-diagram 𝒮 s)) + -- ( coherence-cocone-standard-sequential-colimit (succ-ℕ n) (concat-s 𝒮 a₀ s n p))) ∘ + -- ( tr + -- ( ev-pair + -- ( right-family-descent-data-pushout R) + -- ( right-map-span-diagram 𝒮 s)) + -- ( CB s n p))) + -- coh-dep-cocone-a s n p = + -- ( ( inv-htpy + -- ( ( tr-concat _ _) ∙h + -- ( ( tr _ _) ·l + -- ( ( tr-concat _ _) ∙h + -- ( horizontal-concat-htpy + -- ( λ _ → substitution-law-tr _ _ _) + -- ( tr-concat _ _)))))) ·r + -- ( map-family-descent-data-pushout R + -- ( s , map-cocone-standard-sequential-colimit n p))) ∙h + -- ( ( λ q → + -- ap + -- ( λ r → + -- tr + -- ( ev-pair + -- ( right-family-descent-data-pushout R) + -- ( right-map-span-diagram 𝒮 s)) + -- ( r) + -- ( map-family-descent-data-pushout R + -- ( s , map-cocone-standard-sequential-colimit n p) + -- ( q))) + -- ( inv ([i] p))) ∙h + -- ( λ q → + -- substitution-law-tr + -- ( ev-pair + -- ( right-family-descent-data-pushout R) + -- ( right-map-span-diagram 𝒮 s)) + -- ( concat-s-inf 𝒮 a₀ s) + -- ( coherence-cocone-standard-sequential-colimit n p ∙ + -- ap + -- ( map-cocone-standard-sequential-colimit (succ-ℕ n)) + -- ( glue-standard-pushout _ _))) ∙h + -- ( inv-htpy + -- ( preserves-tr + -- ( ev-pair + -- ( map-family-descent-data-pushout R) + -- ( s)) + -- ( coherence-cocone-standard-sequential-colimit n p ∙ + -- ap (map-cocone-standard-sequential-colimit (succ-ℕ n)) (glue-standard-pushout _ _))))) ∙h + -- ( ( map-family-descent-data-pushout R + -- ( s , + -- map-cocone-standard-sequential-colimit + -- ( succ-ℕ n) + -- ( concat-inv-s 𝒮 a₀ s + -- ( succ-ℕ n) + -- ( concat-s 𝒮 a₀ s n p)))) ·l + -- ( ( tr-concat _ _) ∙h + -- ( λ q → substitution-law-tr _ _ _))) + -- where + -- [i] : + -- ( ( concat-s-inf 𝒮 a₀ s) ·l + -- ( ( coherence-cocone-standard-sequential-colimit n) ∙h + -- ( ( map-cocone-standard-sequential-colimit + -- { A = + -- left-sequential-diagram-zigzag-id-pushout 𝒮 a₀ + -- ( left-map-span-diagram 𝒮 s)} + -- ( succ-ℕ n)) ·l + -- ( λ p → glue-pushout _ _ (s , refl , p))))) ~ + -- ( ( CB s n) ∙h + -- ( ( coherence-cocone-standard-sequential-colimit (succ-ℕ n)) ·r + -- ( concat-s 𝒮 a₀ s n)) ∙h + -- ( ( map-cocone-standard-sequential-colimit + -- { A = + -- right-sequential-diagram-zigzag-id-pushout 𝒮 a₀ + -- ( right-map-span-diagram 𝒮 s)} + -- ( succ-ℕ (succ-ℕ n))) ·l + -- ( λ p → glue-pushout _ _ ( s , refl , concat-s 𝒮 a₀ s n p))) ∙h + -- ( ( inv-htpy (CB s (succ-ℕ n))) ·r + -- ( concat-inv-s 𝒮 a₀ s (succ-ℕ n) ∘ concat-s 𝒮 a₀ s n))) + -- [i] = + -- ( distributive-left-whisker-comp-concat _ _ _) ∙h + -- ( right-transpose-htpy-concat _ _ _ + -- ( ( left-whisker-concat-coherence-square-homotopies _ _ _ _ _ + -- ( λ p → + -- inv + -- ( nat-coherence-square-maps _ _ _ _ + -- ( CB s (succ-ℕ n)) + -- ( glue-pushout _ _ (s , refl , p))))) ∙h + -- ( map-inv-equiv + -- ( equiv-right-transpose-htpy-concat _ _ _) + -- ( ( coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram + -- ( up-standard-sequential-colimit) + -- ( shift-once-cocone-sequential-diagram + -- ( cocone-standard-sequential-colimit + -- ( right-sequential-diagram-zigzag-id-pushout 𝒮 a₀ + -- ( right-map-span-diagram 𝒮 s)))) + -- ( hom-diagram-zigzag-sequential-diagram + -- ( zigzag-sequential-diagram-zigzag-id-pushout 𝒮 a₀ s)) + -- ( n)) ∙h + -- ( ap-concat-htpy + -- ( CB s n) + -- ( ( ap-concat-htpy _ + -- ( ( distributive-left-whisker-comp-concat + -- ( map-cocone-standard-sequential-colimit + -- { A = + -- right-sequential-diagram-zigzag-id-pushout 𝒮 a₀ + -- ( right-map-span-diagram 𝒮 s)} + -- ( succ-ℕ (succ-ℕ n))) + -- ( _) + -- ( _)) ∙h + -- ( ap-concat-htpy _ + -- ( ( left-whisker-comp² _ + -- ( left-whisker-inv-htpy _ _)) ∙h + -- ( left-whisker-inv-htpy _ _))))) ∙h + -- ( inv-htpy-assoc-htpy _ _ _))) ∙h + -- ( inv-htpy-assoc-htpy _ _ _))))) ∙h + -- ( ap-concat-htpy' _ + -- ( inv-htpy-assoc-htpy _ _ _)) + + α : + (s : spanning-type-span-diagram 𝒮) → + (n : ℕ) → + (p : Path-to-a 𝒮 a₀ (left-map-span-diagram 𝒮 s) n) → + coherence-square-maps + ( Ψ s n p) + ( tr + ( ev-pair + ( left-family-descent-data-pushout R) + ( left-map-span-diagram 𝒮 s)) + ( coherence-cocone-standard-sequential-colimit n p)) + ( Φ' s n (concat-s 𝒮 a₀ s n p)) + ( tr + ( λ p → + left-family-descent-data-pushout R + ( left-map-span-diagram 𝒮 s , + map-cocone-standard-sequential-colimit (succ-ℕ n) p)) + ( glue-pushout _ _ (s , refl , p))) + α s n p = + upper-triangle-over + ( up-standard-sequential-colimit) + ( shift-once-cocone-sequential-diagram + ( cocone-standard-sequential-colimit _)) + ( zigzag-sequential-diagram-zigzag-id-pushout 𝒮 a₀ s) + ( ev-pair + ( left-family-descent-data-pushout R) + ( left-map-span-diagram 𝒮 s)) + ( ev-pair + ( right-family-descent-data-pushout R) + ( right-map-span-diagram 𝒮 s)) + ( ev-pair + ( equiv-family-descent-data-pushout R) + ( s)) + ( n) + { p} + -- map-eq-transpose-equiv + -- ( equiv-family-descent-data-pushout R + -- ( s , + -- map-cocone-standard-sequential-colimit + -- ( succ-ℕ n) + -- ( concat-inv-s 𝒮 a₀ s + -- ( succ-ℕ n) + -- ( concat-s 𝒮 a₀ s n p)))) + -- ( inv (coh-dep-cocone-a s n p q)) + + β : + (s : spanning-type-span-diagram 𝒮) → + (n : ℕ) → + (p : Path-to-b 𝒮 a₀ (right-map-span-diagram 𝒮 s) (succ-ℕ n)) → + coherence-square-maps + ( Φ' s n p) + ( tr + ( ev-pair + ( right-family-descent-data-pushout R) + ( right-map-span-diagram 𝒮 s)) + ( coherence-cocone-standard-sequential-colimit (succ-ℕ n) p)) + ( Ψ s (succ-ℕ n) (concat-inv-s 𝒮 a₀ s (succ-ℕ n) p)) + ( tr + ( λ p → + right-family-descent-data-pushout R + ( right-map-span-diagram 𝒮 s , + map-cocone-standard-sequential-colimit (succ-ℕ (succ-ℕ n)) p)) + ( glue-pushout _ _ (s , refl , p))) + β s n p = + lower-triangle-over + ( up-standard-sequential-colimit) + ( shift-once-cocone-sequential-diagram + ( cocone-standard-sequential-colimit _)) + ( zigzag-sequential-diagram-zigzag-id-pushout 𝒮 a₀ s) + ( ev-pair + ( left-family-descent-data-pushout R) + ( left-map-span-diagram 𝒮 s)) + ( ev-pair + ( right-family-descent-data-pushout R) + ( right-map-span-diagram 𝒮 s)) + ( ev-pair + ( equiv-family-descent-data-pushout R) + ( s)) + ( n) + { p} + + -- Note for refactoring: after contracting away the last component and the + -- vertical map, the definition of prism2 will fail to typecheck, since + -- currently the coherence computes to ∙ refl, which needs to be taken + -- into account; contracting away this data would simplify the later + -- homotopy algebra. + stages-cocones' : + (n : ℕ) → + Σ ( (b : codomain-span-diagram 𝒮) → + dependent-cocone-span-diagram + ( cocone-pushout-span-diagram + ( span-diagram-path-to-b 𝒮 a₀ b n)) + ( λ p → + right-family-descent-data-pushout R + ( b , map-cocone-standard-sequential-colimit (succ-ℕ n) p))) + ( λ dep-cocone-b → + Σ ( (a : domain-span-diagram 𝒮) → + dependent-cocone-span-diagram + ( cocone-pushout-span-diagram + ( span-diagram-path-to-a 𝒮 a₀ a n)) + ( λ p → + left-family-descent-data-pushout R + ( a , map-cocone-standard-sequential-colimit (succ-ℕ n) p))) + ( λ dep-cocone-a → + (s : spanning-type-span-diagram 𝒮) → + (p : Path-to-b 𝒮 a₀ (right-map-span-diagram 𝒮 s) (succ-ℕ n)) → + vertical-map-dependent-cocone _ _ _ _ + ( dep-cocone-a (left-map-span-diagram 𝒮 s)) + ( s , refl , p) ＝ + Φ' s n p (dependent-cogap _ _ (dep-cocone-b (right-map-span-diagram 𝒮 s)) p))) + stages-cocones' zero-ℕ = + dep-cocone-b , + dep-cocone-a , + λ s p → refl + where + dep-cocone-b : + (b : codomain-span-diagram 𝒮) → + dependent-cocone-span-diagram + ( cocone-pushout-span-diagram (span-diagram-path-to-b 𝒮 a₀ b 0)) + ( λ p → + right-family-descent-data-pushout R + ( b , map-cocone-standard-sequential-colimit 1 p)) + pr1 (dep-cocone-b b) (map-raise ()) + pr1 (pr2 (dep-cocone-b ._)) (s , refl , map-raise refl) = + tr + ( ev-pair + ( right-family-descent-data-pushout R) + ( right-map-span-diagram 𝒮 s)) + ( CB s 0 (map-raise refl)) + ( map-family-descent-data-pushout R + ( s , map-cocone-standard-sequential-colimit 0 (map-raise refl)) + ( r₀)) + pr2 (pr2 (dep-cocone-b ._)) (s , refl , map-raise ()) + dep-cocone-a : + (a : domain-span-diagram 𝒮) → + dependent-cocone-span-diagram + ( cocone-pushout-span-diagram (span-diagram-path-to-a 𝒮 a₀ a 0)) + ( λ p → + left-family-descent-data-pushout R + ( a , map-cocone-standard-sequential-colimit 1 p)) + pr1 (dep-cocone-a .a₀) (map-raise refl) = + tr + ( ev-pair (left-family-descent-data-pushout R) a₀) + ( coherence-cocone-standard-sequential-colimit 0 (map-raise refl)) + ( r₀) + pr1 (pr2 (dep-cocone-a a)) (s , refl , p) = + Φ' s 0 p (dependent-cogap _ _ (dep-cocone-b (right-map-span-diagram 𝒮 s)) p) + pr2 (pr2 (dep-cocone-a .a₀)) (s , refl , map-raise refl) = + ( α s 0 (map-raise refl) r₀) ∙ + ( ap + ( Φ' s 0 _) + ( inv + ( compute-inr-dependent-cogap _ _ + ( dep-cocone-b (right-map-span-diagram 𝒮 s)) + ( s , refl , map-raise refl)))) + stages-cocones' (succ-ℕ n) = + dep-cocone-b , + dep-cocone-a , + λ s p → refl + where + dep-cocone-b : + (b : codomain-span-diagram 𝒮) → + dependent-cocone-span-diagram + ( cocone-pushout-span-diagram (span-diagram-path-to-b 𝒮 a₀ b (succ-ℕ n))) + ( λ p → + right-family-descent-data-pushout R + ( b , map-cocone-standard-sequential-colimit (succ-ℕ (succ-ℕ n)) p)) + pr1 (dep-cocone-b b) p = + tr + ( ev-pair (right-family-descent-data-pushout R) b) + ( coherence-cocone-standard-sequential-colimit (succ-ℕ n) p) + ( dependent-cogap _ _ (pr1 (stages-cocones' n) b) p) + pr1 (pr2 (dep-cocone-b b)) (s , refl , p) = + tr + ( ev-pair + ( right-family-descent-data-pushout R) + ( right-map-span-diagram 𝒮 s)) + ( CB s (succ-ℕ n) p) + ( map-family-descent-data-pushout R + ( s , map-cocone-standard-sequential-colimit (succ-ℕ n) p) + ( dependent-cogap _ _ (pr1 (pr2 (stages-cocones' n)) (left-map-span-diagram 𝒮 s)) p)) + pr2 (pr2 (dep-cocone-b b)) (s , refl , p) = + ( β s n p _) ∙ + ( ap + ( Ψ s (succ-ℕ n) _) + ( inv + ( ( compute-inr-dependent-cogap _ _ + ( pr1 (pr2 (stages-cocones' n)) (left-map-span-diagram 𝒮 s)) + ( s , refl , p)) ∙ + ( pr2 (pr2 (stages-cocones' n)) s p)))) + dep-cocone-a : + (a : domain-span-diagram 𝒮) → + dependent-cocone-span-diagram + ( cocone-pushout-span-diagram (span-diagram-path-to-a 𝒮 a₀ a (succ-ℕ n))) + ( λ p → + left-family-descent-data-pushout R + ( a , map-cocone-standard-sequential-colimit (succ-ℕ (succ-ℕ n)) p)) + pr1 (dep-cocone-a a) p = + tr + ( ev-pair (left-family-descent-data-pushout R) a) + ( coherence-cocone-standard-sequential-colimit (succ-ℕ n) p) + ( dependent-cogap _ _ (pr1 (pr2 (stages-cocones' n)) a) p) + pr1 (pr2 (dep-cocone-a a)) (s , refl , p) = + Φ' s (succ-ℕ n) p (dependent-cogap _ _ (dep-cocone-b (right-map-span-diagram 𝒮 s)) p) + pr2 (pr2 (dep-cocone-a a)) (s , refl , p) = + ( α s (succ-ℕ n) p _) ∙ + ( ap + ( Φ' s (succ-ℕ n) _) + ( inv + ( compute-inr-dependent-cogap _ _ + ( dep-cocone-b (right-map-span-diagram 𝒮 s)) + ( s , refl , p)))) + + tB : + (b : codomain-span-diagram 𝒮) (n : ℕ) (p : Path-to-b 𝒮 a₀ b n) → + right-family-descent-data-pushout R + ( b , map-cocone-standard-sequential-colimit n p) + tB b zero-ℕ (map-raise ()) + tB b (succ-ℕ n) = dependent-cogap _ _ (pr1 (stages-cocones' n) b) + + KB : + (b : codomain-span-diagram 𝒮) (n : ℕ) (p : Path-to-b 𝒮 a₀ b n) → + dependent-identification + ( ev-pair (right-family-descent-data-pushout R) b) + ( coherence-cocone-standard-sequential-colimit n p) + ( tB b n p) + ( tB b (succ-ℕ n) (inl-Path-to-b 𝒮 a₀ b n p)) + KB b zero-ℕ (map-raise ()) + KB b (succ-ℕ n) p = + inv + ( compute-inl-dependent-cogap _ _ + ( pr1 (stages-cocones' (succ-ℕ n)) b) + ( p)) + + tA : + (a : domain-span-diagram 𝒮) (n : ℕ) (p : Path-to-a 𝒮 a₀ a n) → + left-family-descent-data-pushout R + ( a , map-cocone-standard-sequential-colimit n p) + tA .a₀ zero-ℕ (map-raise refl) = r₀ + tA a (succ-ℕ n) = dependent-cogap _ _ (pr1 (pr2 (stages-cocones' n)) a) + + KA : + (a : domain-span-diagram 𝒮) (n : ℕ) (p : Path-to-a 𝒮 a₀ a n) → + dependent-identification + ( ev-pair (left-family-descent-data-pushout R) a) + ( coherence-cocone-standard-sequential-colimit n p) + ( tA a n p) + ( tA a (succ-ℕ n) (inl-Path-to-a 𝒮 a₀ a n p)) + KA a zero-ℕ (map-raise refl) = + inv + ( compute-inl-dependent-cogap _ _ + ( pr1 (pr2 (stages-cocones' 0)) a) + ( map-raise refl)) + KA a (succ-ℕ n) p = + inv + ( compute-inl-dependent-cogap _ _ + ( pr1 (pr2 (stages-cocones' (succ-ℕ n))) a) + ( p)) + + tS-in-diagram : + (s : spanning-type-span-diagram 𝒮) (n : ℕ) → + (p : Path-to-a 𝒮 a₀ (left-map-span-diagram 𝒮 s) n) → + ( tr (ev-pair (right-family-descent-data-pushout R) (right-map-span-diagram 𝒮 s)) + ( CB s n p) + ( map-family-descent-data-pushout R _ (tA (left-map-span-diagram 𝒮 s) n p))) ＝ + ( tB (right-map-span-diagram 𝒮 s) (succ-ℕ n) (concat-s 𝒮 a₀ s n p)) + tS-in-diagram s zero-ℕ (map-raise refl) = + inv (compute-inr-dependent-cogap _ _ _ _) + tS-in-diagram s (succ-ℕ n) p = inv (compute-inr-dependent-cogap _ _ _ _) + + module vertices + (s : spanning-type-span-diagram 𝒮) + where + PAn : (n : ℕ) → UU (l1 ⊔ l2 ⊔ l3) + PAn = Path-to-a 𝒮 a₀ (left-map-span-diagram 𝒮 s) + QAn : {n : ℕ} → PAn n → UU l5 + QAn {n} p = + left-family-descent-data-pushout R (left-map-span-diagram 𝒮 s , map-cocone-standard-sequential-colimit n p) + PBn : (n : ℕ) → UU (l1 ⊔ l2 ⊔ l3) + PBn = Path-to-b 𝒮 a₀ (right-map-span-diagram 𝒮 s) ∘ succ-ℕ + QBn : {n : ℕ} → PBn n → UU l5 + QBn {n} p = + right-family-descent-data-pushout R (right-map-span-diagram 𝒮 s , map-cocone-standard-sequential-colimit (succ-ℕ n) p) + fn : {n : ℕ} → PAn n → PBn n + fn = concat-s 𝒮 a₀ s _ + gn : {n : ℕ} → PAn n → PAn (succ-ℕ n) + gn = inl-Path-to-a 𝒮 a₀ (left-map-span-diagram 𝒮 s) _ + hn : {n : ℕ} → PBn n → PBn (succ-ℕ n) + hn = inl-Path-to-b 𝒮 a₀ (right-map-span-diagram 𝒮 s) _ + mn : {n : ℕ} → PBn n → PAn (succ-ℕ n) + mn {n} = concat-inv-s 𝒮 a₀ s (succ-ℕ n) + sAn : {n : ℕ} (p : PAn n) → QAn p + sAn = tA (left-map-span-diagram 𝒮 s) _ + sBn : {n : ℕ} (p : PBn n) → QBn p + sBn = tB (right-map-span-diagram 𝒮 s) _ + f'n : {n : ℕ} {p : PAn n} → QAn p → QBn (fn p) + f'n {n} {p} = Ψ s n p + g'n : {n : ℕ} {p : PAn n} → QAn p → QAn (gn p) + g'n {n} {p} = + tr + ( ev-pair + ( left-family-descent-data-pushout R) + ( left-map-span-diagram 𝒮 s)) + ( coherence-cocone-standard-sequential-colimit n p) + h'n : {n : ℕ} {p : PBn n} → QBn p → QBn (hn p) + h'n {n} {p} = + tr + ( ev-pair + ( right-family-descent-data-pushout R) + ( right-map-span-diagram 𝒮 s)) + ( coherence-cocone-standard-sequential-colimit (succ-ℕ n) p) + m'n : {n : ℕ} {p : PBn n} → QBn p → QAn (mn p) + m'n = Φ' s _ _ + + module sides + (s : spanning-type-span-diagram 𝒮) (n : ℕ) + where + open vertices s + left : + {p : PAn n} → f'n (sAn p) ＝ sBn (fn p) + left = tS-in-diagram s n _ + right : + {p : PAn (succ-ℕ n)} → + f'n (sAn p) ＝ sBn (fn p) + right = tS-in-diagram s (succ-ℕ n) _ + bottom : + {p : PAn n} → hn (fn p) ＝ fn (gn p) + bottom = + naturality-map-hom-diagram-zigzag-sequential-diagram + ( zigzag-sequential-diagram-zigzag-id-pushout 𝒮 a₀ s) + ( n) + ( _) + bottom1 : + {p : PAn n} → gn p ＝ mn (fn p) + bottom1 = glue-pushout _ _ _ + bottom2 : + {p : PBn n} → hn p ＝ fn (mn p) + bottom2 = glue-pushout _ _ _ + far : + {p : PAn n} → g'n (sAn p) ＝ sAn (gn p) + far = KA (left-map-span-diagram 𝒮 s) n _ + near : + {p : PBn n} → h'n (sBn p) ＝ sBn (hn p) + near = KB (right-map-span-diagram 𝒮 s) (succ-ℕ n) _ + mid : + {p : PBn n} → m'n (sBn p) ＝ sAn (mn p) + mid = mid' _ _ + where + mid' : (n : ℕ) (p : PBn n) → m'n (sBn p) ＝ sAn (mn p) + mid' zero-ℕ p = inv (compute-inr-dependent-cogap _ _ _ _) + mid' (succ-ℕ n) p = inv (compute-inr-dependent-cogap _ _ _ _) + top1 : + {p : PAn n} (q : QAn p) → + tr QAn bottom1 (g'n q) ＝ m'n (f'n q) + top1 = α s n _ + top2 : + {p : PBn n} (q : QBn p) → + tr QBn bottom2 (h'n {n = n} q) ＝ f'n {n = succ-ℕ n} (m'n q) + top2 = β s n _ + top : + {p : PAn n} (q : QAn p) → + tr QBn bottom (h'n (f'n q)) ＝ f'n (g'n q) + top = + pasting-triangles-over gn fn fn hn g'n f'n f'n h'n mn m'n + ( inv-htpy (λ p → bottom1 {p})) + ( λ p → bottom2 {p}) + ( inv-htpy-over QAn (λ _ → bottom1) g'n (m'n ∘ f'n) top1) + ( top2) + + module CUBE + (s : spanning-type-span-diagram 𝒮) (n : ℕ) + where + open vertices s + open sides s n + + CUBE : UU (l1 ⊔ l2 ⊔ l3 ⊔ l5) + CUBE = + section-square-over gn fn fn hn g'n f'n f'n h'n sAn sBn sAn sBn + ( λ p → far {p}) + ( λ p → left {p}) + ( λ p → right {p}) + ( λ p → near {p}) + ( λ p → bottom {p}) + ( top) + + PRISM1 : UU (l1 ⊔ l2 ⊔ l3 ⊔ l5) + PRISM1 = + section-triangle-over fn gn mn f'n g'n m'n sAn sBn sAn + ( λ p → left {p}) + ( λ p → far {p}) + ( λ p → mid {p}) + ( λ p → bottom1 {p}) + ( top1) + + PRISM2 : UU (l1 ⊔ l2 ⊔ l3 ⊔ l5) + PRISM2 = + section-triangle-over mn hn fn m'n h'n f'n sBn sAn sBn + ( λ p → mid {p}) + ( λ p → near {p}) + ( λ p → right {p}) + ( λ p → bottom2 {p}) + ( top2) + + module cube + (s : spanning-type-span-diagram 𝒮) + where abstract + open vertices s + open sides s + open CUBE s + + -- THE COMMENTED CODE WORKS, DON'T DELETE IT! + -- It just takes too long to typecheck it in its current state + prism1 : (n : ℕ) → PRISM1 n + -- prism1 = {!!} + prism1 zero-ℕ (map-raise refl) = + lem _ _ _ _ _ + ( ( ap + ( _∙ (top1 0 (sAn _) ∙ ap m'n (left 0))) + ( ( inv (ap-inv (tr QAn (bottom1 0)) (far 0))) ∙ + ( ap² (tr QAn (bottom1 0)) (inv-inv _)))) ∙ + -- ( [i]) ∙ + ( inv + ( compute-glue-dependent-cogap _ _ + ( pr1 (pr2 (stages-cocones' 0)) (left-map-span-diagram 𝒮 s)) + ( s , refl , (map-raise refl)))) ∙ + ( ap + ( apd sAn (bottom1 0) ∙_) + ( inv (inv-inv _)))) + where + open import foundation.action-on-higher-identifications-functions + prism1 (succ-ℕ n) p = + lem _ _ _ _ _ + ( ( ap + ( _∙ (top1 (succ-ℕ n) (sAn _) ∙ ap m'n (left (succ-ℕ n)))) + ( ( inv (ap-inv (tr QAn (bottom1 (succ-ℕ n))) (far (succ-ℕ n)))) ∙ + ( ap² (tr QAn (bottom1 (succ-ℕ n))) (inv-inv _)))) ∙ + ( inv + ( compute-glue-dependent-cogap _ _ + ( pr1 (pr2 (stages-cocones' (succ-ℕ n))) (left-map-span-diagram 𝒮 s)) + ( s , refl , p))) ∙ + -- ( [i]) ∙ + ( ap + ( apd sAn (bottom1 (succ-ℕ n)) ∙_) + ( inv (inv-inv _)))) + where + open import foundation.action-on-higher-identifications-functions + + prism2 : (n : ℕ) → PRISM2 n + -- prism2 = {!!} + prism2 0 p = + lem _ _ _ _ _ + ( ( ap + ( _∙ (top2 0 (sBn p) ∙ ap f'n (mid 0))) + ( ( inv (ap-inv (tr QBn (bottom2 0)) (near 0))) ∙ + ( ap² (tr (QBn {1}) (bottom2 0)) (inv-inv _)))) ∙ + -- ( inv [ii]) ∙ + ( inv + ( ( compute-glue-dependent-cogap _ _ + ( pr1 (stages-cocones' 1) (right-map-span-diagram 𝒮 s)) + ( s , refl , p)) ∙ + ( ap + ( λ q → + ap (tr QBn _) (compute-inl-dependent-cogap _ _ _ _) ∙ + (top2 0 (sBn p) ∙ ap f'n (inv q))) + ( right-unit)))) ∙ + ( ap + ( apd sBn (bottom2 0) ∙_) + ( inv (inv-inv _)))) + where + open import foundation.action-on-higher-identifications-functions + -- [i] = + -- -- inv + -- ( compute-glue-dependent-cogap _ _ + -- ( pr1 (stages-cocones' 1) (right-map-span-diagram 𝒮 s)) + -- ( s , refl , p)) + -- [ii] = [i] ∙ ap (λ q → ap (tr QBn _) (compute-inl-dependent-cogap _ _ _ _) ∙ (top2 0 (sBn p) ∙ ap f'n (inv q))) right-unit + prism2 (succ-ℕ n) p = + lem _ _ _ _ _ + ( ( ap + ( _∙ (top2 (succ-ℕ n) (sBn p) ∙ ap f'n (mid (succ-ℕ n)))) + ( ( inv (ap-inv (tr QBn (bottom2 (succ-ℕ n))) (near (succ-ℕ n)))) ∙ + ( ap² (tr QBn (bottom2 (succ-ℕ n))) (inv-inv _)))) ∙ + -- ( inv [ii]) ∙ + ( inv + ( ( compute-glue-dependent-cogap _ _ + ( pr1 (stages-cocones' (succ-ℕ (succ-ℕ n))) (right-map-span-diagram 𝒮 s)) + ( s , refl , p)) ∙ + ( ap + ( λ q → + ap (tr QBn _) (compute-inl-dependent-cogap _ _ _ _) ∙ + (top2 (succ-ℕ n) (sBn p) ∙ ap f'n (inv q))) + ( right-unit)))) ∙ + ( ap + ( apd sBn (bottom2 (succ-ℕ n)) ∙_) + ( inv (inv-inv _)))) + where + open import foundation.action-on-higher-identifications-functions + -- [i] = + -- -- inv + -- ( compute-glue-dependent-cogap _ _ + -- ( pr1 (stages-cocones' (succ-ℕ (succ-ℕ n))) (right-map-span-diagram 𝒮 s)) + -- ( s , refl , p)) + -- [ii] = [i] ∙ ap (λ q → ap (tr QBn _) (compute-inl-dependent-cogap _ _ _ _) ∙ (top2 (succ-ℕ n) (sBn p) ∙ ap f'n (inv q))) right-unit + + cube : (n : ℕ) → CUBE n + cube n = + pasting-sections-triangles-over gn fn fn hn g'n f'n f'n h'n mn m'n sAn sBn sAn sBn + ( λ p → far n {p}) + ( λ p → left n {p}) + ( λ p → right n {p}) + ( λ p → near n {p}) + ( λ p → mid n {p}) + ( inv-htpy (λ p → bottom1 n {p})) + ( λ p → bottom2 n {p}) + ( inv-htpy-over QAn (λ p → bottom1 n {p}) g'n (m'n ∘ f'n) (top1 n)) + ( top2 n) + ( get-section-triangle-over' fn gn mn f'n g'n m'n sAn sBn sAn + ( λ p → left n {p}) + ( λ p → far n {p}) + ( λ p → mid n {p}) + ( inv-htpy (λ p → bottom1 n {p})) + ( inv-htpy-over QAn (λ p → bottom1 n {p}) g'n (m'n ∘ f'n) (top1 n)) + ( inv-section-htpy-over + ( λ p → bottom1 n {p}) + ( top1 n) + sAn sAn _ _ + ( unget-section-triangle-over fn gn mn f'n g'n m'n sAn sBn sAn + ( λ p → left n {p}) + ( λ p → far n {p}) + ( λ p → mid n {p}) + ( λ p → bottom1 n {p}) + ( top1 n) + ( prism1 n)))) + ( prism2 n) + + + opaque + unfolding Φ' -- square-over-diagram-square-over-colimit γ + + realign-top : + (s : spanning-type-span-diagram 𝒮) (n : ℕ) → + (p : vertices.PAn s n) → + sides.top s n {p} ~ + square-over-diagram-square-over-colimit + ( up-standard-sequential-colimit) + ( shift-once-cocone-sequential-diagram + ( cocone-standard-sequential-colimit _)) + ( hom-diagram-zigzag-sequential-diagram + ( zigzag-sequential-diagram-zigzag-id-pushout 𝒮 a₀ s)) + ( ev-pair + ( left-family-descent-data-pushout R) + ( left-map-span-diagram 𝒮 s)) + ( ev-pair + ( right-family-descent-data-pushout R) + ( right-map-span-diagram 𝒮 s)) + ( ev-pair + ( equiv-family-descent-data-pushout R) + ( s)) + ( n) + ( p) + realign-top s = + compute-square-over-zigzag-square-over-colimit + ( up-standard-sequential-colimit) + ( shift-once-cocone-sequential-diagram + ( cocone-standard-sequential-colimit _)) + ( zigzag-sequential-diagram-zigzag-id-pushout 𝒮 a₀ s) + ( ev-pair + ( left-family-descent-data-pushout R) + ( left-map-span-diagram 𝒮 s)) + ( ev-pair + ( right-family-descent-data-pushout R) + ( right-map-span-diagram 𝒮 s)) + ( ev-pair + ( equiv-family-descent-data-pushout R) + ( s)) + + KS-in-diagram : + (s : spanning-type-span-diagram 𝒮) (n : ℕ) → + section-square-over + ( vertices.gn s) + ( vertices.fn s) + ( vertices.fn s) + ( vertices.hn s) + ( vertices.g'n s) + ( vertices.f'n s) + ( vertices.f'n s) + ( vertices.h'n s) + ( vertices.sAn s) + ( vertices.sBn s) + ( vertices.sAn s) + ( vertices.sBn s) + ( λ p → sides.far s n) + ( λ p → sides.left s n) + ( λ p → sides.right s n) + ( λ p → sides.near s n) + ( λ p → sides.bottom s n) + ( sides.top s n) + KS-in-diagram = cube.cube + + alt-section-RA : + (a : domain-span-diagram 𝒮) + (p : left-id-pushout 𝒮 a₀ a) → + left-family-descent-data-pushout R (a , p) + alt-section-RA a = + sect-family-sect-dd-sequential-colimit + ( up-standard-sequential-colimit) + ( _) + ( tA a , KA a) + + alt-section-RB : + (b : codomain-span-diagram 𝒮) + (p : right-id-pushout 𝒮 a₀ b) → + right-family-descent-data-pushout R (b , p) + alt-section-RB b = + sect-family-sect-dd-sequential-colimit + ( up-shift-cocone-sequential-diagram 1 up-standard-sequential-colimit) + ( _) + ( tB b ∘ succ-ℕ , KB b ∘ succ-ℕ) + + alt-ind-coherence : + (s : spanning-type-span-diagram 𝒮) + (p : left-id-pushout 𝒮 a₀ (left-map-span-diagram 𝒮 s)) → + map-family-descent-data-pushout R + ( s , p) + ( alt-section-RA (left-map-span-diagram 𝒮 s) p) ＝ + alt-section-RB + ( right-map-span-diagram 𝒮 s) + ( map-sequential-colimit-hom-sequential-diagram + ( up-standard-sequential-colimit) + ( shift-once-cocone-sequential-diagram + ( cocone-standard-sequential-colimit _)) + ( hom-diagram-zigzag-sequential-diagram + ( zigzag-sequential-diagram-zigzag-id-pushout 𝒮 a₀ s)) + ( p)) + alt-ind-coherence s p = + square-colimit-cube-diagram + ( up-standard-sequential-colimit) + ( up-shift-cocone-sequential-diagram 1 up-standard-sequential-colimit) + ( hom-diagram-zigzag-sequential-diagram + ( zigzag-sequential-diagram-zigzag-id-pushout 𝒮 a₀ s)) + ( tA (left-map-span-diagram 𝒮 s) , KA (left-map-span-diagram 𝒮 s)) + ( tB (right-map-span-diagram 𝒮 s) ∘ succ-ℕ , + KB (right-map-span-diagram 𝒮 s) ∘ succ-ℕ) + ( λ p → equiv-family-descent-data-pushout R (s , p)) + ( tS-in-diagram s) + ( λ n p → + ap + ( λ H → H ∙ ap (vertices.f'n s) (sides.far s n) ∙ sides.right s n) + ( inv (realign-top s n p (vertices.sAn s p))) ∙ KS-in-diagram s n p) + ( p) + + alt-ind-singleton-zigzag-id-pushout' : section-descent-data-pushout R + pr1 alt-ind-singleton-zigzag-id-pushout' = + ind-Σ alt-section-RA + pr1 (pr2 alt-ind-singleton-zigzag-id-pushout') = + ind-Σ alt-section-RB + pr2 (pr2 alt-ind-singleton-zigzag-id-pushout') = + ind-Σ alt-ind-coherence + + is-identity-system-zigzag-id-pushout : + is-identity-system-descent-data-pushout + ( descent-data-zigzag-id-pushout 𝒮 a₀) + ( refl-id-pushout 𝒮 a₀) + is-identity-system-zigzag-id-pushout = + is-identity-system-descent-data-pushout-ind-singleton up-c + ( descent-data-zigzag-id-pushout 𝒮 a₀) + ( refl-id-pushout 𝒮 a₀) + -- ( ind-singleton-zigzag-id-pushout') + ( alt-ind-singleton-zigzag-id-pushout') +``` diff --git a/src/synthetic-homotopy-theory/zigzags-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/zigzags-sequential-diagrams.lagda.md index 71068b80e1..c521df41bf 100644 --- a/src/synthetic-homotopy-theory/zigzags-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/zigzags-sequential-diagrams.lagda.md @@ -247,10 +247,9 @@ module _ (z : zigzag-sequential-diagram A B) where - hom-diagram-zigzag-sequential-diagram : hom-sequential-diagram A B - pr1 hom-diagram-zigzag-sequential-diagram = - map-zigzag-sequential-diagram z - pr2 hom-diagram-zigzag-sequential-diagram n = + naturality-map-hom-diagram-zigzag-sequential-diagram : + naturality-hom-sequential-diagram A B (map-zigzag-sequential-diagram z) + naturality-map-hom-diagram-zigzag-sequential-diagram n = horizontal-pasting-up-diagonal-coherence-triangle-maps ( map-sequential-diagram A n) ( map-zigzag-sequential-diagram z n) @@ -259,6 +258,12 @@ module _ ( inv-htpy (upper-triangle-zigzag-sequential-diagram z n)) ( lower-triangle-zigzag-sequential-diagram z n) + hom-diagram-zigzag-sequential-diagram : hom-sequential-diagram A B + pr1 hom-diagram-zigzag-sequential-diagram = + map-zigzag-sequential-diagram z + pr2 hom-diagram-zigzag-sequential-diagram = + naturality-map-hom-diagram-zigzag-sequential-diagram + module _ {l1 l2 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2} (z : zigzag-sequential-diagram A B)