Flattening lemma for descent data for pushouts

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

src/foundation/functoriality-dependent-pair-types.lagda.md

@@ -9,8 +9,10 @@ open import foundation-core.functoriality-dependent-pair-types public
 <details><summary>Imports</summary>
 
 ```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
 ```
 
 </details>
@@ -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

src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md

@@ -7,6 +7,8 @@ module synthetic-homotopy-theory.flattening-lemma-pushouts where
 <details><summary>Imports</summary>
 
 ```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)
+```