From 9652db7d7773454e3bcf401041e2fecf6cf4a4d0 Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Sat, 7 Oct 2023 18:28:05 +0200 Subject: [PATCH] Flattening lemma for descent data for pushouts --- .../equality-dependent-pair-types.lagda.md | 18 ++- ...unctoriality-dependent-pair-types.lagda.md | 18 ++- .../flattening-lemma-pushouts.lagda.md | 124 +++++++++++++++++- 3 files changed, 155 insertions(+), 5 deletions(-) diff --git a/src/foundation/equality-dependent-pair-types.lagda.md b/src/foundation/equality-dependent-pair-types.lagda.md index 68770562f6f..ea47b8a1b75 100644 --- a/src/foundation/equality-dependent-pair-types.lagda.md +++ b/src/foundation/equality-dependent-pair-types.lagda.md @@ -116,11 +116,25 @@ module _ { l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {Y : UU l3} (f : Σ A B → Y) where - ap-eq-pair-Σ : + compute-ap-eq-pair-Σ : { x y : A} (p : x ＝ y) {b : B x} {b' : B y} → ( q : dependent-identification B p b b') → ap f (eq-pair-Σ p q) ＝ (ap f (eq-pair-Σ p refl) ∙ ap (ev-pair f y) q) - ap-eq-pair-Σ refl refl = refl + compute-ap-eq-pair-Σ refl refl = refl +``` + +### Equality of dependent pair types consists of two orthogonal components + +```agda +module _ + { l1 l2 : Level} {A : UU l1} (B : A → UU l2) + where + + orthogonal-eq-pair-Σ : + { a a' : A} (p : a ＝ a') → + { b : B a} {b' : B a'} (q : dependent-identification B p b b') → + eq-pair-Σ p q ＝ (eq-pair-Σ p refl ∙ eq-pair-Σ refl q) + orthogonal-eq-pair-Σ refl q = refl ``` ## See also diff --git a/src/foundation/functoriality-dependent-pair-types.lagda.md b/src/foundation/functoriality-dependent-pair-types.lagda.md index 321df443226..4c68002608c 100644 --- a/src/foundation/functoriality-dependent-pair-types.lagda.md +++ b/src/foundation/functoriality-dependent-pair-types.lagda.md @@ -9,8 +9,10 @@ open import foundation-core.functoriality-dependent-pair-types public
Imports ```agda +open import foundation.action-on-identifications-functions open import foundation.cones-over-cospans open import foundation.dependent-pair-types +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels @@ -22,7 +24,6 @@ open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.pullbacks -open import foundation-core.transport-along-identifications ```
@@ -264,6 +265,21 @@ module _ coherence-square-maps-map-Σ-map-base H (a , p) = eq-pair-Σ (H a) refl ``` +### The action of `map-Σ-map-base` on identifications of the form `eq-pair-Σ` is given by the action on the base + +```agda +module _ + { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (C : B → UU l3) + where + + compute-ap-map-Σ-map-base-eq-pair-Σ : + { s s' : A} (p : s ＝ s') {t : C (f s)} {t' : C (f s')} + ( q : tr (C ∘ f) p t ＝ t') → + ap (map-Σ-map-base f C) (eq-pair-Σ p q) ＝ + eq-pair-Σ (ap f p) (substitution-law-tr C f p ∙ q) + compute-ap-map-Σ-map-base-eq-pair-Σ refl refl = refl +``` + ## See also - Arithmetical laws involving dependent pair types are recorded in diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md index 06542295a2c..d71888f573a 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md @@ -7,6 +7,8 @@ module synthetic-homotopy-theory.flattening-lemma-pushouts where
Imports ```agda +open import foundation.action-on-identifications-functions +open import foundation.commuting-cubes-of-maps open import foundation.commuting-squares-of-maps open import foundation.commuting-triangles-of-maps open import foundation.dependent-pair-types @@ -155,7 +157,7 @@ module _ coherence-square-cocone-flattening-descent-data-pushout : coherence-square-maps ( map-Σ (pr1 (pr2 P)) g (λ s → map-equiv (pr2 (pr2 P) s))) - ( map-Σ (pr1 P) f (λ s → id)) + ( map-Σ-map-base f (pr1 P)) ( vertical-map-cocone-flattening-descent-data-pushout) ( horizontal-map-cocone-flattening-descent-data-pushout) coherence-square-cocone-flattening-descent-data-pushout = @@ -166,7 +168,7 @@ module _ cocone-flattening-descent-data-pushout : cocone - ( map-Σ (pr1 P) f (λ s → id)) + ( map-Σ-map-base f (pr1 P)) ( map-Σ (pr1 (pr2 P)) g (λ s → map-equiv (pr2 (pr2 P) s))) ( Σ X Q) pr1 cocone-flattening-descent-data-pushout = @@ -279,3 +281,121 @@ module _ ( dup-pushout (λ x → P x → Y)))) ( is-equiv-ind-Σ) ``` + +### Proof of the descent data statement of the flattening lemma + +The proof is carried out by constructing a commuting cube, which has +equivalences for vertical maps, the `cocone-flattening-pushout` square for the +bottom, and the `cocone-flattening-descent-data-pushout` square for the top. + +The bottom is a pushout by the above flattening lemma, which implies that the +top is also a pushout. + +The other parts of the cube are defined naturally, and come from the following +map of spans: + +```text + Σ (a : A) (PA a) <------- Σ (s : S) (PA (f s)) -----> Σ (b : B) (PB b) + | | | + | | | + v v v +Σ (a : A) (P (i a)) <---- Σ (s : S) (P (i (f s))) ---> Σ (b : B) (P (j b)) +``` + +where the vertical maps are equivalences given fiberwise by the equivalence of +descent data. + +```agda +module _ + { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} + ( f : S → A) (g : S → B) (c : cocone f g X) + ( P : Fam-pushout l5 f g) + ( Q : X → UU l5) + ( e : equiv-Fam-pushout P (desc-fam c Q)) + where + + coherence-cube-flattening-lemma-descent-data-pushout : + coherence-cube-maps + ( map-Σ-map-base f (Q ∘ horizontal-map-cocone f g c)) + ( map-Σ + ( Q ∘ vertical-map-cocone f g c) + ( g) + ( λ s → tr Q (coherence-square-cocone f g c s))) + ( horizontal-map-cocone-flattening-pushout Q f g c) + ( vertical-map-cocone-flattening-pushout Q f g c) + ( map-Σ-map-base f (pr1 P)) + ( map-Σ (pr1 (pr2 P)) g (λ s → map-equiv (pr2 (pr2 P) s))) + ( horizontal-map-cocone-flattening-descent-data-pushout f g c P Q e) + ( vertical-map-cocone-flattening-descent-data-pushout f g c P Q e) + ( tot (λ s → map-equiv (pr1 e (f s)))) + ( tot (λ a → map-equiv (pr1 e a))) + ( tot (λ b → map-equiv (pr1 (pr2 e) b))) + ( id) + ( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e) + ( refl-htpy) + ( htpy-map-Σ + ( Q ∘ vertical-map-cocone f g c) + ( refl-htpy) + ( λ s → + tr Q (coherence-square-cocone f g c s) ∘ (map-equiv (pr1 e (f s)))) + ( λ s → inv-htpy (pr2 (pr2 e) s))) + ( refl-htpy) + ( refl-htpy) + ( coherence-square-cocone-flattening-pushout Q f g c) + coherence-cube-flattening-lemma-descent-data-pushout (s , t) = + ( ap-id + ( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e + ( s , t))) ∙ + ( orthogonal-eq-pair-Σ Q + ( coherence-square-cocone f g c s) + ( inv (pr2 (pr2 e) s t))) ∙ + ( ap + ( eq-pair-Σ (coherence-square-cocone f g c s) refl ∙_) + ( inv + ( ( right-unit) ∙ + ( compute-ap-map-Σ-map-base-eq-pair-Σ + ( vertical-map-cocone f g c) + ( Q) + ( refl) + ( inv (pr2 (pr2 e) s t)))))) + + flattening-lemma-descent-data-pushout : + flattening-lemma-descent-data-pushout-statement f g c P Q e + flattening-lemma-descent-data-pushout dup-pushout = + universal-property-pushout-top-universal-property-pushout-bottom-cube-is-equiv + ( map-Σ-map-base f (Q ∘ horizontal-map-cocone f g c)) + ( map-Σ + ( Q ∘ vertical-map-cocone f g c) + ( g) + ( λ s → tr Q (coherence-square-cocone f g c s))) + ( horizontal-map-cocone-flattening-pushout Q f g c) + ( vertical-map-cocone-flattening-pushout Q f g c) + ( map-Σ-map-base f (pr1 P)) + ( map-Σ (pr1 (pr2 P)) g (λ s → map-equiv (pr2 (pr2 P) s))) + ( horizontal-map-cocone-flattening-descent-data-pushout f g c P Q e) + ( vertical-map-cocone-flattening-descent-data-pushout f g c P Q e) + ( tot (λ s → map-equiv (pr1 e (f s)))) + ( tot (λ a → map-equiv (pr1 e a))) + ( tot (λ b → map-equiv (pr1 (pr2 e) b))) + ( id) + ( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e) + ( refl-htpy) + ( htpy-map-Σ + ( Q ∘ vertical-map-cocone f g c) + ( refl-htpy) + ( λ s → + tr Q (coherence-square-cocone f g c s) ∘ (map-equiv (pr1 e (f s)))) + ( λ s → inv-htpy (pr2 (pr2 e) s))) + ( refl-htpy) + ( refl-htpy) + ( coherence-square-cocone-flattening-pushout Q f g c) + ( coherence-cube-flattening-lemma-descent-data-pushout) + ( is-equiv-tot-is-fiberwise-equiv + ( λ s → is-equiv-map-equiv (pr1 e (f s)))) + ( is-equiv-tot-is-fiberwise-equiv + ( λ a → is-equiv-map-equiv (pr1 e a))) + ( is-equiv-tot-is-fiberwise-equiv + ( λ b → is-equiv-map-equiv (pr1 (pr2 e) b))) + ( is-equiv-id) + ( flattening-lemma-pushout Q f g c dup-pushout) +```