diff --git a/src/foundation/commuting-triangles-of-maps.lagda.md b/src/foundation/commuting-triangles-of-maps.lagda.md
index f657e5d08d..ef0e081b0a 100644
--- a/src/foundation/commuting-triangles-of-maps.lagda.md
+++ b/src/foundation/commuting-triangles-of-maps.lagda.md
@@ -56,6 +56,18 @@ module _
   (left : A → X) (right : B → X) (e : A ≃ B)
   where
 
+  equiv-coherence-triangle-maps-inv-top' :
+    coherence-triangle-maps left right (map-equiv e) ≃
+    coherence-triangle-maps' right left (map-inv-equiv e)
+  equiv-coherence-triangle-maps-inv-top' =
+    equiv-Π
+      ( λ b → left (map-inv-equiv e b) ＝ right b)
+      ( e)
+      ( λ a →
+        equiv-concat
+          ( ap left (is-retraction-map-inv-equiv e a))
+          ( right (map-equiv e a)))
+
   equiv-coherence-triangle-maps-inv-top :
     coherence-triangle-maps left right (map-equiv e) ≃
     coherence-triangle-maps right left (map-inv-equiv e)
@@ -63,13 +75,7 @@ module _
     ( equiv-inv-htpy
       ( left ∘ (map-inv-equiv e))
       ( right)) ∘e
-    ( equiv-Π
-      ( λ b → left (map-inv-equiv e b) ＝ right b)
-      ( e)
-      ( λ a →
-        equiv-concat
-          ( ap left (is-retraction-map-inv-equiv e a))
-          ( right (map-equiv e a))))
+    ( equiv-coherence-triangle-maps-inv-top')
 
   coherence-triangle-maps-inv-top :
     coherence-triangle-maps left right (map-equiv e) →
diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md
index 0a3a32779f..354fa98d51 100644
--- a/src/foundation/equivalences.lagda.md
+++ b/src/foundation/equivalences.lagda.md
@@ -16,6 +16,7 @@ open import foundation.equivalence-extensionality
 open import foundation.function-extensionality
 open import foundation.functoriality-fibers-of-maps
 open import foundation.logical-equivalences
+open import foundation.transport-along-identifications
 open import foundation.transposition-identifications-along-equivalences
 open import foundation.truncated-maps
 open import foundation.universal-property-equivalences
@@ -572,6 +573,19 @@ pr1 (equiv-precomp-equiv e C) = _∘e e
 pr2 (equiv-precomp-equiv e C) = is-equiv-precomp-equiv-equiv e
 ```
 
+### Computing transport in the type of equivalences
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
+  where
+
+  tr-equiv-type :
+    {x y : A} (p : x ＝ y) (e : B x ≃ C x) →
+    tr (λ x → B x ≃ C x) p e ＝ equiv-tr C p ∘e e ∘e equiv-tr B (inv p)
+  tr-equiv-type refl e = eq-htpy-equiv refl-htpy
+```
+
 ### A cospan in which one of the legs is an equivalence is a pullback if and only if the corresponding map on the cone is an equivalence
 
 ```agda
diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 307d4ac9a6..4717610eb4 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -47,6 +47,9 @@ open import synthetic-homotopy-theory.descent-circle-dependent-pair-types public
 open import synthetic-homotopy-theory.descent-circle-equivalence-types public
 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-identity-types-over-pushouts public
 open import synthetic-homotopy-theory.descent-data-pushouts public
 open import synthetic-homotopy-theory.descent-data-sequential-colimits public
 open import synthetic-homotopy-theory.descent-property-pushouts public
@@ -103,6 +106,7 @@ open import synthetic-homotopy-theory.recursion-principle-pushouts public
 open import synthetic-homotopy-theory.retracts-of-sequential-diagrams public
 open import synthetic-homotopy-theory.rewriting-pushouts public
 open import synthetic-homotopy-theory.sections-descent-circle public
+open import synthetic-homotopy-theory.sections-descent-data-pushouts public
 open import synthetic-homotopy-theory.sequential-colimits public
 open import synthetic-homotopy-theory.sequential-diagrams public
 open import synthetic-homotopy-theory.sequentially-compact-types public
diff --git a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
index f3b33ac51b..cfba684dd3 100644
--- a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
@@ -27,6 +27,7 @@ open import foundation.homotopy-induction
 open import foundation.identity-types
 open import foundation.retractions
 open import foundation.sections
+open import foundation.span-diagrams
 open import foundation.structure-identity-principle
 open import foundation.torsorial-type-families
 open import foundation.transport-along-higher-identifications
@@ -104,6 +105,13 @@ module _
         ( horizontal-map-dependent-cocone (f s))
         ( vertical-map-dependent-cocone (g s))
     coherence-square-dependent-cocone = pr2 (pr2 d)
+
+dependent-cocone-span-diagram :
+  { l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4}
+  ( c : cocone-span-diagram 𝒮 X) (P : X → UU l5) →
+  UU (l1 ⊔ l2 ⊔ l3 ⊔ l5)
+dependent-cocone-span-diagram {𝒮 = 𝒮} =
+  dependent-cocone (left-map-span-diagram 𝒮) (right-map-span-diagram 𝒮)
 ```
 
 ### Cocones equipped with dependent cocones
@@ -188,6 +196,13 @@ pr1 (pr2 (dependent-cocone-map f g c P h)) b =
   h (vertical-map-cocone f g c b)
 pr2 (pr2 (dependent-cocone-map f g c P h)) s =
   apd h (coherence-square-cocone f g c s)
+
+dependent-cocone-map-span-diagram :
+  { l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4}
+  ( c : cocone-span-diagram 𝒮 X) (P : X → UU l5) →
+  ( (x : X) → P x) → dependent-cocone-span-diagram c P
+dependent-cocone-map-span-diagram {𝒮 = 𝒮} c =
+  dependent-cocone-map (left-map-span-diagram 𝒮) (right-map-span-diagram 𝒮) c
 ```
 
 ## Properties
diff --git a/src/synthetic-homotopy-theory/descent-data-equivalence-types-over-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-equivalence-types-over-pushouts.lagda.md
new file mode 100644
index 0000000000..7095433e23
--- /dev/null
+++ b/src/synthetic-homotopy-theory/descent-data-equivalence-types-over-pushouts.lagda.md
@@ -0,0 +1,385 @@
+# Descent data for type families of equivalence types over pushouts
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module synthetic-homotopy-theory.descent-data-equivalence-types-over-pushouts where
+```
+
+<details><summary>Imports</summary>
+
+```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.equivalence-extensionality
+open import foundation.equivalences
+open import foundation.fibers-of-maps
+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.span-diagrams
+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-spans
+open import synthetic-homotopy-theory.descent-data-pushouts
+open import synthetic-homotopy-theory.equivalences-descent-data-pushouts
+open import synthetic-homotopy-theory.families-descent-data-pushouts
+open import synthetic-homotopy-theory.morphisms-descent-data-pushouts
+open import synthetic-homotopy-theory.sections-descent-data-pushouts
+open import synthetic-homotopy-theory.universal-property-pushouts
+```
+
+</details>
+
+## Idea
+
+Given two
+[families with descent data](synthetic-homotopy-theory.families-descent-data-pushouts.md)
+for [pushouts](synthetic-homotopy-theory.pushouts.md) `P ≈ (PA, PB, PS)` and
+`R ≈ (RA, RB, RS)`, we show that
+[fiberwise equivalences](foundation-core.families-of-equivalences.md)
+`(x : X) → P x ≃ R x` correspond to
+[equivalences](synthetic-homotopy-theory.equivalences-descent-data-pushouts.md)
+`(PA, PB, PS) ≃ (RA, RB, RS)`.
+
+**Proof:** The proof follows exactly the same pattern as the one in
+[`descent-data-function-types-over-pushouts`](synthetic-homotopy-theory.descent-data-function-types-over-pushouts.md).
+
+## Definitions
+
+### The type family of fiberwise equivalences with corresponding descent data for pushouts
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {X : UU l4} {c : cocone-span-diagram 𝒮 X}
+  (P : family-with-descent-data-pushout c l5)
+  (R : family-with-descent-data-pushout c l6)
+  where
+
+  family-cocone-equivalence-type-pushout : X → UU (l5 ⊔ l6)
+  family-cocone-equivalence-type-pushout x =
+    family-cocone-family-with-descent-data-pushout P x ≃
+    family-cocone-family-with-descent-data-pushout R x
+
+  descent-data-equivalence-type-pushout : descent-data-pushout 𝒮 (l5 ⊔ l6)
+  pr1 descent-data-equivalence-type-pushout a =
+    left-family-family-with-descent-data-pushout P a ≃
+    left-family-family-with-descent-data-pushout R a
+  pr1 (pr2 descent-data-equivalence-type-pushout) b =
+    right-family-family-with-descent-data-pushout P b ≃
+    right-family-family-with-descent-data-pushout R b
+  pr2 (pr2 descent-data-equivalence-type-pushout) s =
+    ( equiv-postcomp-equiv
+      ( equiv-family-family-with-descent-data-pushout R s)
+      ( _)) ∘e
+    ( equiv-precomp-equiv
+      ( inv-equiv (equiv-family-family-with-descent-data-pushout P s))
+      ( _))
+
+  left-equiv-equiv-descent-data-equivalence-type-pushout :
+    (a : domain-span-diagram 𝒮) →
+    ( family-cocone-family-with-descent-data-pushout P
+        ( horizontal-map-cocone _ _ c a) ≃
+      family-cocone-family-with-descent-data-pushout R
+        ( horizontal-map-cocone _ _ c a)) ≃
+    ( left-family-family-with-descent-data-pushout P a ≃
+      left-family-family-with-descent-data-pushout R a)
+  left-equiv-equiv-descent-data-equivalence-type-pushout a =
+    ( equiv-postcomp-equiv
+      ( left-equiv-family-with-descent-data-pushout R a)
+      ( _)) ∘e
+    ( equiv-precomp-equiv
+      ( inv-equiv (left-equiv-family-with-descent-data-pushout P a))
+      ( _))
+
+  right-equiv-equiv-descent-data-equivalence-type-pushout :
+    (b : codomain-span-diagram 𝒮) →
+    ( family-cocone-family-with-descent-data-pushout P
+        ( vertical-map-cocone _ _ c b) ≃
+      family-cocone-family-with-descent-data-pushout R
+        ( vertical-map-cocone _ _ c b)) ≃
+    ( right-family-family-with-descent-data-pushout P b ≃
+      right-family-family-with-descent-data-pushout R b)
+  right-equiv-equiv-descent-data-equivalence-type-pushout b =
+    ( equiv-postcomp-equiv
+      ( right-equiv-family-with-descent-data-pushout R b)
+      ( _)) ∘e
+    ( equiv-precomp-equiv
+      ( inv-equiv (right-equiv-family-with-descent-data-pushout P b))
+      ( _))
+
+  coherence-equiv-descent-data-equivalence-type-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    coherence-square-maps
+      ( map-equiv
+        ( left-equiv-equiv-descent-data-equivalence-type-pushout
+          ( left-map-span-diagram 𝒮 s)))
+      ( tr
+        ( family-cocone-equivalence-type-pushout)
+        ( coherence-square-cocone _ _ c s))
+      ( map-family-descent-data-pushout
+        ( descent-data-equivalence-type-pushout)
+        ( s))
+      ( map-equiv
+        ( right-equiv-equiv-descent-data-equivalence-type-pushout
+          ( right-map-span-diagram 𝒮 s)))
+  coherence-equiv-descent-data-equivalence-type-pushout s =
+    ( ( map-equiv
+      ( right-equiv-equiv-descent-data-equivalence-type-pushout
+        ( right-map-span-diagram 𝒮 s))) ·l
+      ( tr-equiv-type
+        ( family-cocone-family-with-descent-data-pushout P)
+        ( family-cocone-family-with-descent-data-pushout R)
+        ( coherence-square-cocone _ _ c s))) ∙h
+    ( λ e →
+      eq-htpy-equiv
+        ( horizontal-concat-htpy
+          ( coherence-family-with-descent-data-pushout R s ·r map-equiv e)
+          ( coherence-square-maps-inv-equiv
+            ( equiv-tr
+              ( family-cocone-family-with-descent-data-pushout P)
+              ( coherence-square-cocone _ _ c s))
+            ( left-equiv-family-with-descent-data-pushout P
+              ( left-map-span-diagram 𝒮 s))
+            ( right-equiv-family-with-descent-data-pushout P
+              ( right-map-span-diagram 𝒮 s))
+            ( equiv-family-family-with-descent-data-pushout P s)
+            ( inv-htpy (coherence-family-with-descent-data-pushout P s)))))
+
+  equiv-descent-data-equivalence-type-pushout :
+    equiv-descent-data-pushout
+      ( descent-data-family-cocone-span-diagram c
+        ( family-cocone-equivalence-type-pushout))
+      ( descent-data-equivalence-type-pushout)
+  pr1 equiv-descent-data-equivalence-type-pushout =
+    left-equiv-equiv-descent-data-equivalence-type-pushout
+  pr1 (pr2 equiv-descent-data-equivalence-type-pushout) =
+    right-equiv-equiv-descent-data-equivalence-type-pushout
+  pr2 (pr2 equiv-descent-data-equivalence-type-pushout) =
+    coherence-equiv-descent-data-equivalence-type-pushout
+
+  family-with-descent-data-equivalence-type-pushout :
+    family-with-descent-data-pushout c (l5 ⊔ l6)
+  pr1 family-with-descent-data-equivalence-type-pushout =
+    family-cocone-equivalence-type-pushout
+  pr1 (pr2 family-with-descent-data-equivalence-type-pushout) =
+    descent-data-equivalence-type-pushout
+  pr2 (pr2 family-with-descent-data-equivalence-type-pushout) =
+    equiv-descent-data-equivalence-type-pushout
+```
+
+## Properties
+
+### Sections of descent data for families of equivalences correspond to equivalences of descent data
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {X : UU l4} {c : cocone-span-diagram 𝒮 X}
+  (P : family-with-descent-data-pushout c l5)
+  (R : family-with-descent-data-pushout c l6)
+  where
+
+  equiv-section-descent-data-equivalence-type-pushout :
+    section-descent-data-pushout
+      ( descent-data-equivalence-type-pushout P R) →
+    equiv-descent-data-pushout
+      ( descent-data-family-with-descent-data-pushout P)
+      ( descent-data-family-with-descent-data-pushout R)
+  equiv-section-descent-data-equivalence-type-pushout =
+    tot
+      ( λ tA →
+        tot
+          ( λ tB tS s →
+            inv-htpy
+              ( map-inv-equiv
+                ( equiv-coherence-triangle-maps-inv-top'
+                  ( ( map-family-family-with-descent-data-pushout R s) ∘
+                    ( map-equiv (tA (left-map-span-diagram 𝒮 s))))
+                  ( map-equiv (tB (right-map-span-diagram 𝒮 s)))
+                  ( equiv-family-family-with-descent-data-pushout P s))
+                ( htpy-eq-equiv (tS s)))))
+
+  abstract
+    is-equiv-equiv-section-descent-data-equivalence-type-pushout :
+      is-equiv equiv-section-descent-data-equivalence-type-pushout
+    is-equiv-equiv-section-descent-data-equivalence-type-pushout =
+      is-equiv-tot-is-fiberwise-equiv
+        ( λ tA →
+          is-equiv-tot-is-fiberwise-equiv
+            ( λ tB →
+              is-equiv-map-Π-is-fiberwise-equiv
+                ( λ s →
+                  is-equiv-comp _ _
+                    ( is-equiv-map-equiv (extensionality-equiv _ _))
+                    ( is-equiv-comp _ _
+                      ( is-equiv-map-inv-equiv
+                        ( equiv-coherence-triangle-maps-inv-top'
+                          ( (map-family-family-with-descent-data-pushout R s) ∘
+                            ( map-equiv (tA (left-map-span-diagram 𝒮 s))))
+                          ( map-equiv (tB (right-map-span-diagram 𝒮 s)))
+                          ( equiv-family-family-with-descent-data-pushout P s)))
+                      ( is-equiv-inv-htpy _ _)))))
+
+  equiv-descent-data-equiv-family-cocone-span-diagram :
+    ( (x : X) →
+      family-cocone-family-with-descent-data-pushout P x ≃
+      family-cocone-family-with-descent-data-pushout R x) →
+    equiv-descent-data-pushout
+      ( descent-data-family-with-descent-data-pushout P)
+      ( descent-data-family-with-descent-data-pushout R)
+  equiv-descent-data-equiv-family-cocone-span-diagram =
+    ( equiv-section-descent-data-equivalence-type-pushout) ∘
+    ( section-descent-data-section-family-cocone-span-diagram
+      ( family-with-descent-data-equivalence-type-pushout P R))
+
+  abstract
+    is-equiv-equiv-descent-data-equiv-family-cocone-span-diagram :
+      universal-property-pushout _ _ c →
+      is-equiv equiv-descent-data-equiv-family-cocone-span-diagram
+    is-equiv-equiv-descent-data-equiv-family-cocone-span-diagram up-c =
+      is-equiv-comp _ _
+        ( is-equiv-section-descent-data-section-family-cocone-span-diagram _
+          ( up-c))
+        ( is-equiv-equiv-section-descent-data-equivalence-type-pushout)
+```
+
+As a corollary, given an equivalence
+`(hA, hB, hS) : (PA, PB, PS) ≃ (RA, RB, RS)`, there is a unique family of
+equivalences `h : (x : X) → P x → R x` such that its induced equivalence is
+homotopic to `(hA, hB, hS)`. The homotopy provides us in particular with the
+component-wise [homotopies](foundation-core.homotopies.md)
+
+```text
+                 hA a                               hB a
+          PA a --------> RA a                PB b --------> RB b
+            |              ∧                   |              ∧
+  (eᴾA a)⁻¹ |              | eᴿA a   (eᴾB b)⁻¹ |              | eᴿB b
+            |              |                   |              |
+            ∨              |                   ∨              |
+         P (ia) ------> R (ia)              P (jb) ------> R (jb)
+                h (ia)                             h (jb)
+```
+
+which we can turn into the computation rules
+
+```text
+              eᴾA a                           eᴾB a
+      P (ia) -------> PA a            P (jb) -------> PB b
+         |              |                |              |
+  h (ia) |              | hA a    h (jb) |              | hB b
+         |              |                |              |
+         ∨              ∨                ∨              ∨
+      R (ia) -------> RA a            R (jb) -------> RB b
+              eᴿA a                           eᴿB b
+```
+
+by inverting the inverted equivalences.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {X : UU l4} {c : cocone-span-diagram 𝒮 X}
+  (up-c : universal-property-pushout _ _ c)
+  (P : family-with-descent-data-pushout c l5)
+  (R : family-with-descent-data-pushout c l6)
+  (e :
+    equiv-descent-data-pushout
+      ( descent-data-family-with-descent-data-pushout P)
+      ( descent-data-family-with-descent-data-pushout R))
+  where
+
+  abstract
+    uniqueness-equiv-equiv-descent-data-pushout :
+      is-contr
+        ( Σ ( (x : X) →
+              family-cocone-family-with-descent-data-pushout P x ≃
+              family-cocone-family-with-descent-data-pushout R x)
+            ( λ h →
+              htpy-equiv-descent-data-pushout
+                ( descent-data-family-with-descent-data-pushout P)
+                ( descent-data-family-with-descent-data-pushout R)
+                ( equiv-descent-data-equiv-family-cocone-span-diagram P R h)
+                ( e)))
+    uniqueness-equiv-equiv-descent-data-pushout =
+      is-contr-equiv'
+        ( fiber (equiv-descent-data-equiv-family-cocone-span-diagram P R) e)
+        ( equiv-tot
+          ( λ f → extensionality-equiv-descent-data-pushout _ e))
+        ( is-contr-map-is-equiv
+          ( is-equiv-equiv-descent-data-equiv-family-cocone-span-diagram P R
+            ( up-c))
+          ( e))
+
+  equiv-equiv-descent-data-pushout :
+    (x : X) →
+    family-cocone-family-with-descent-data-pushout P x ≃
+    family-cocone-family-with-descent-data-pushout R x
+  equiv-equiv-descent-data-pushout =
+    pr1 (center uniqueness-equiv-equiv-descent-data-pushout)
+
+  map-equiv-descent-data-pushout :
+    (x : X) →
+    family-cocone-family-with-descent-data-pushout P x →
+    family-cocone-family-with-descent-data-pushout R x
+  map-equiv-descent-data-pushout x =
+    map-equiv (equiv-equiv-descent-data-pushout x)
+
+  compute-left-map-equiv-equiv-descent-data-pushout :
+    (a : domain-span-diagram 𝒮) →
+    coherence-square-maps
+      ( left-map-family-with-descent-data-pushout P a)
+      ( map-equiv-descent-data-pushout (horizontal-map-cocone _ _ c a))
+      ( left-map-equiv-descent-data-pushout
+        ( descent-data-family-with-descent-data-pushout P)
+        ( descent-data-family-with-descent-data-pushout R)
+        ( e)
+        ( a))
+      ( left-map-family-with-descent-data-pushout R a)
+  compute-left-map-equiv-equiv-descent-data-pushout a =
+    map-inv-equiv
+      ( equiv-coherence-triangle-maps-inv-top'
+        ( left-map-family-with-descent-data-pushout R a ∘
+          map-equiv-descent-data-pushout (horizontal-map-cocone _ _ c a))
+        ( left-map-equiv-descent-data-pushout
+          ( descent-data-family-with-descent-data-pushout P)
+          ( descent-data-family-with-descent-data-pushout R)
+          ( e)
+          ( a))
+        ( left-equiv-family-with-descent-data-pushout P a))
+      ( pr1 (pr2 (center uniqueness-equiv-equiv-descent-data-pushout)) a)
+
+  compute-right-map-equiv-equiv-descent-data-pushout :
+    (b : codomain-span-diagram 𝒮) →
+    coherence-square-maps
+      ( right-map-family-with-descent-data-pushout P b)
+      ( map-equiv-descent-data-pushout (vertical-map-cocone _ _ c b))
+      ( right-map-equiv-descent-data-pushout
+        ( descent-data-family-with-descent-data-pushout P)
+        ( descent-data-family-with-descent-data-pushout R)
+        ( e)
+        ( b))
+      ( right-map-family-with-descent-data-pushout R b)
+  compute-right-map-equiv-equiv-descent-data-pushout b =
+    map-inv-equiv
+      ( equiv-coherence-triangle-maps-inv-top'
+        ( right-map-family-with-descent-data-pushout R b ∘
+          map-equiv-descent-data-pushout (vertical-map-cocone _ _ c b))
+        ( right-map-equiv-descent-data-pushout
+          ( descent-data-family-with-descent-data-pushout P)
+          ( descent-data-family-with-descent-data-pushout R)
+          ( e)
+          ( b))
+        ( right-equiv-family-with-descent-data-pushout P b))
+      ( pr1 (pr2 (pr2 (center uniqueness-equiv-equiv-descent-data-pushout))) b)
+```
diff --git a/src/synthetic-homotopy-theory/descent-data-function-types-over-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-function-types-over-pushouts.lagda.md
new file mode 100644
index 0000000000..ac284b320a
--- /dev/null
+++ b/src/synthetic-homotopy-theory/descent-data-function-types-over-pushouts.lagda.md
@@ -0,0 +1,415 @@
+# Descent data for type families of function types over pushouts
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module synthetic-homotopy-theory.descent-data-function-types-over-pushouts where
+```
+
+<details><summary>Imports</summary>
+
+```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.span-diagrams
+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-spans
+open import synthetic-homotopy-theory.descent-data-pushouts
+open import synthetic-homotopy-theory.equivalences-descent-data-pushouts
+open import synthetic-homotopy-theory.families-descent-data-pushouts
+open import synthetic-homotopy-theory.morphisms-descent-data-pushouts
+open import synthetic-homotopy-theory.sections-descent-data-pushouts
+open import synthetic-homotopy-theory.universal-property-pushouts
+```
+
+</details>
+
+## Idea
+
+Given two
+[families with descent data](synthetic-homotopy-theory.families-descent-data-pushouts.md)
+for [pushouts](synthetic-homotopy-theory.pushouts.md) `P ≈ (PA, PB, PS)` and
+`R ≈ (RA, RB, RS)`, we show that
+[fiberwise maps](foundation.families-of-maps.md) `(x : X) → P x → R x`
+correspond to
+[morphisms](synthetic-homotopy-theory.morphisms-descent-data-pushouts.md)
+`(PA, PB, PS) → (RA, RB, RS)`.
+
+**Proof:** We first characterize the type family `x ↦ (P x → R x)`. The
+corresponding [descent data](synthetic-homotopy-theory.descent-data-pushouts.md)
+consists of the type families
+
+```text
+  a ↦ (PA a → RA a)
+  b ↦ (PB b → RB b),
+```
+
+and the gluing data sending `h : PA (fs) → RA (fs)` to
+`(RS s ∘ h ∘ (PS s)⁻¹) : PB (gs) → RB (gs)`.
+
+**Note:** It is important to differentiate between families of _function types_,
+i.e. a type family that to every `x : X` assigns the _type_ `P x → R x`, and
+families of _functions_, i.e. a family that to every `x : X` assigns a
+_function_ from `P x` to R x`. Descent data plays the role of a family of types,
+so it makes sense to talk about "descent data corresponding to a family of
+function types", but it doesn't make sense to talk about "descent data
+corresponding to a family of functions". The kind of data that corresponds to
+families of functions are the _sections_ of the descent data of a family of
+function types.
+
+It suffices to show that the sections correspond to morphisms. The first two
+components of a section and a morphism agree, namely they are
+
+```text
+  sA : (a : A) → PA a → RA a
+  sB : (b : B) → PB b → RB b,
+```
+
+respectively. The coherence datum of a section has the type
+
+```text
+  (s : S) → RS s ∘ sA (fs) ∘ (RS s)⁻¹ = sB (gs),
+```
+
+which we can massage into a coherence of the morphism as
+
+```text
+  RS s ∘ sA (fs) ∘ (PS s)⁻¹ = sB (gs)
+  ≃ RS s ∘ sA (fs) ∘ (PS s)⁻¹ ~ sB (gs)  by function extensionality
+  ≃ RS s ∘ sA (fs) ~ sB (gs) ∘ PS s      by transposition of (PS s)
+  ≃ sB (gs) ∘ PS s ~ RS s ∘ sA (fs)      by symmetry of homotopies.
+```
+
+## Definitions
+
+### The type family of fiberwise functions with corresponding descent data for pushouts
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {X : UU l4} {c : cocone-span-diagram 𝒮 X}
+  (P : family-with-descent-data-pushout c l5)
+  (R : family-with-descent-data-pushout c l6)
+  where
+
+  family-cocone-function-type-pushout : X → UU (l5 ⊔ l6)
+  family-cocone-function-type-pushout x =
+    family-cocone-family-with-descent-data-pushout P x →
+    family-cocone-family-with-descent-data-pushout R x
+
+  descent-data-function-type-pushout : descent-data-pushout 𝒮 (l5 ⊔ l6)
+  pr1 descent-data-function-type-pushout a =
+    left-family-family-with-descent-data-pushout P a →
+    left-family-family-with-descent-data-pushout R a
+  pr1 (pr2 descent-data-function-type-pushout) b =
+    right-family-family-with-descent-data-pushout P b →
+    right-family-family-with-descent-data-pushout R b
+  pr2 (pr2 descent-data-function-type-pushout) s =
+    ( equiv-postcomp _
+      ( equiv-family-family-with-descent-data-pushout R s)) ∘e
+    ( equiv-precomp
+      ( inv-equiv (equiv-family-family-with-descent-data-pushout P s))
+      ( _))
+
+  left-equiv-equiv-descent-data-function-type-pushout :
+    (a : domain-span-diagram 𝒮) →
+    ( family-cocone-family-with-descent-data-pushout P
+        ( horizontal-map-cocone _ _ c a) →
+      family-cocone-family-with-descent-data-pushout R
+        ( horizontal-map-cocone _ _ c a)) ≃
+    ( left-family-family-with-descent-data-pushout P a →
+      left-family-family-with-descent-data-pushout R a)
+  left-equiv-equiv-descent-data-function-type-pushout a =
+    ( equiv-postcomp _
+      ( left-equiv-family-with-descent-data-pushout R a)) ∘e
+    ( equiv-precomp
+      ( inv-equiv (left-equiv-family-with-descent-data-pushout P a))
+      ( _))
+
+  right-equiv-equiv-descent-data-function-type-pushout :
+    (b : codomain-span-diagram 𝒮) →
+    ( family-cocone-family-with-descent-data-pushout P
+        ( vertical-map-cocone _ _ c b) →
+      family-cocone-family-with-descent-data-pushout R
+        ( vertical-map-cocone _ _ c b)) ≃
+    ( right-family-family-with-descent-data-pushout P b →
+      right-family-family-with-descent-data-pushout R b)
+  right-equiv-equiv-descent-data-function-type-pushout b =
+    ( equiv-postcomp _
+      ( right-equiv-family-with-descent-data-pushout R b)) ∘e
+    ( equiv-precomp
+      ( inv-equiv (right-equiv-family-with-descent-data-pushout P b))
+      ( _))
+
+  coherence-equiv-descent-data-function-type-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    coherence-square-maps
+      ( map-equiv
+        ( left-equiv-equiv-descent-data-function-type-pushout
+          ( left-map-span-diagram 𝒮 s)))
+      ( tr
+        ( family-cocone-function-type-pushout)
+        ( coherence-square-cocone _ _ c s))
+      ( map-family-descent-data-pushout
+        ( descent-data-function-type-pushout)
+        ( s))
+      ( map-equiv
+        ( right-equiv-equiv-descent-data-function-type-pushout
+          ( right-map-span-diagram 𝒮 s)))
+  coherence-equiv-descent-data-function-type-pushout s =
+    ( ( map-equiv
+        ( right-equiv-equiv-descent-data-function-type-pushout
+          ( right-map-span-diagram 𝒮 s))) ·l
+      ( tr-function-type
+        ( family-cocone-family-with-descent-data-pushout P)
+        ( family-cocone-family-with-descent-data-pushout R)
+        ( coherence-square-cocone _ _ c s))) ∙h
+    ( λ h →
+      eq-htpy
+        ( horizontal-concat-htpy
+          ( coherence-family-with-descent-data-pushout R s ·r h)
+          ( coherence-square-maps-inv-equiv
+            ( equiv-tr
+              ( family-cocone-family-with-descent-data-pushout P)
+              ( coherence-square-cocone _ _ c s))
+            ( left-equiv-family-with-descent-data-pushout P
+              ( left-map-span-diagram 𝒮 s))
+            ( right-equiv-family-with-descent-data-pushout P
+              ( right-map-span-diagram 𝒮 s))
+            ( equiv-family-family-with-descent-data-pushout P s)
+            ( inv-htpy (coherence-family-with-descent-data-pushout P s)))))
+
+  equiv-descent-data-function-type-pushout :
+    equiv-descent-data-pushout
+      ( descent-data-family-cocone-span-diagram c
+        ( family-cocone-function-type-pushout))
+      ( descent-data-function-type-pushout)
+  pr1 equiv-descent-data-function-type-pushout =
+    left-equiv-equiv-descent-data-function-type-pushout
+  pr1 (pr2 equiv-descent-data-function-type-pushout) =
+    right-equiv-equiv-descent-data-function-type-pushout
+  pr2 (pr2 equiv-descent-data-function-type-pushout) =
+    coherence-equiv-descent-data-function-type-pushout
+
+  family-with-descent-data-function-type-pushout :
+    family-with-descent-data-pushout c (l5 ⊔ l6)
+  pr1 family-with-descent-data-function-type-pushout =
+    family-cocone-function-type-pushout
+  pr1 (pr2 family-with-descent-data-function-type-pushout) =
+    descent-data-function-type-pushout
+  pr2 (pr2 family-with-descent-data-function-type-pushout) =
+    equiv-descent-data-function-type-pushout
+```
+
+## Properties
+
+### Sections of descent data for families of functions correspond to morphisms of descent data
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {X : UU l4} {c : cocone-span-diagram 𝒮 X}
+  (P : family-with-descent-data-pushout c l5)
+  (R : family-with-descent-data-pushout c l6)
+  where
+
+  hom-section-descent-data-function-type-pushout :
+    section-descent-data-pushout (descent-data-function-type-pushout P R) →
+    hom-descent-data-pushout
+      ( descent-data-family-with-descent-data-pushout P)
+      ( descent-data-family-with-descent-data-pushout R)
+  hom-section-descent-data-function-type-pushout =
+    tot
+      ( λ tA →
+        tot
+        ( λ tB tS s →
+          inv-htpy
+            ( map-inv-equiv
+              ( equiv-coherence-triangle-maps-inv-top'
+                ( ( map-family-family-with-descent-data-pushout R s) ∘
+                  ( tA (left-map-span-diagram 𝒮 s)))
+                ( tB (right-map-span-diagram 𝒮 s))
+                ( equiv-family-family-with-descent-data-pushout P s))
+              ( htpy-eq (tS s)))))
+
+  abstract
+    is-equiv-hom-section-descent-data-function-type-pushout :
+      is-equiv
+        ( hom-section-descent-data-function-type-pushout)
+    is-equiv-hom-section-descent-data-function-type-pushout =
+      is-equiv-tot-is-fiberwise-equiv
+        ( λ tA →
+          is-equiv-tot-is-fiberwise-equiv
+            ( λ tB →
+              is-equiv-map-Π-is-fiberwise-equiv
+                ( λ s →
+                  is-equiv-comp _ _
+                    ( funext _ _)
+                    ( is-equiv-comp _ _
+                      ( is-equiv-map-inv-equiv
+                        ( equiv-coherence-triangle-maps-inv-top'
+                          ( ( map-family-family-with-descent-data-pushout R s) ∘
+                            ( tA (left-map-span-diagram 𝒮 s)))
+                          ( tB (right-map-span-diagram 𝒮 s))
+                          ( equiv-family-family-with-descent-data-pushout P s)))
+                      ( is-equiv-inv-htpy _ _)))))
+
+  hom-descent-data-map-family-cocone-span-diagram :
+    ( (x : X) →
+      family-cocone-family-with-descent-data-pushout P x →
+      family-cocone-family-with-descent-data-pushout R x) →
+    hom-descent-data-pushout
+      ( descent-data-family-with-descent-data-pushout P)
+      ( descent-data-family-with-descent-data-pushout R)
+  hom-descent-data-map-family-cocone-span-diagram =
+    ( hom-section-descent-data-function-type-pushout) ∘
+    ( section-descent-data-section-family-cocone-span-diagram
+      ( family-with-descent-data-function-type-pushout P R))
+
+  abstract
+    is-equiv-hom-descent-data-map-family-cocone-span-diagram :
+      universal-property-pushout _ _ c →
+      is-equiv hom-descent-data-map-family-cocone-span-diagram
+    is-equiv-hom-descent-data-map-family-cocone-span-diagram up-c =
+      is-equiv-comp _ _
+        ( is-equiv-section-descent-data-section-family-cocone-span-diagram _
+          ( up-c))
+        ( is-equiv-hom-section-descent-data-function-type-pushout)
+```
+
+As a corollary, given a morphism `(hA, hB, hS) : (PA, PB, PS) → (RA, RB, RS)`,
+there is a unique family of maps `h : (x : X) → P x → R x` such that its induced
+morphism is homotopic to `(hA, hB, hS)`. The homotopy provides us in particular
+with the component-wise [homotopies](foundation-core.homotopies.md)
+
+```text
+                 hA a                               hB a
+          PA a --------> RA a                PB b --------> RB b
+            |              ∧                   |              ∧
+  (eᴾA a)⁻¹ |              | eᴿA a   (eᴾB b)⁻¹ |              | eᴿB b
+            |              |                   |              |
+            ∨              |                   ∨              |
+         P (ia) ------> R (ia)              P (jb) ------> R (jb)
+                h (ia)                             h (jb)
+```
+
+which we can turn into the computation rules
+
+```text
+              eᴾA a                           eᴾB a
+      P (ia) -------> PA a            P (jb) -------> PB b
+         |              |                |              |
+  h (ia) |              | hA a    h (jb) |              | hB b
+         |              |                |              |
+         ∨              ∨                ∨              ∨
+      R (ia) -------> RA a            R (jb) -------> RB b
+              eᴿA a                           eᴿB b
+```
+
+by inverting the inverted equivalences.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {X : UU l4} {c : cocone-span-diagram 𝒮 X}
+  (up-c : universal-property-pushout _ _ c)
+  (P : family-with-descent-data-pushout c l5)
+  (R : family-with-descent-data-pushout c l6)
+  (m :
+    hom-descent-data-pushout
+      ( descent-data-family-with-descent-data-pushout P)
+      ( descent-data-family-with-descent-data-pushout R))
+  where
+
+  abstract
+    uniqueness-map-hom-descent-data-pushout :
+      is-contr
+        ( Σ ( (x : X) →
+              family-cocone-family-with-descent-data-pushout P x →
+              family-cocone-family-with-descent-data-pushout R x)
+            ( λ h →
+              htpy-hom-descent-data-pushout
+                ( descent-data-family-with-descent-data-pushout P)
+                ( descent-data-family-with-descent-data-pushout R)
+                ( hom-descent-data-map-family-cocone-span-diagram P R h)
+                ( m)))
+    uniqueness-map-hom-descent-data-pushout =
+      is-contr-equiv'
+        ( fiber (hom-descent-data-map-family-cocone-span-diagram P R) m)
+        ( equiv-tot
+          ( λ h → extensionality-hom-descent-data-pushout _ _ _ m))
+        ( is-contr-map-is-equiv
+          ( is-equiv-hom-descent-data-map-family-cocone-span-diagram P R up-c)
+          ( m))
+
+  map-hom-descent-data-pushout :
+    (x : X) →
+    family-cocone-family-with-descent-data-pushout P x →
+    family-cocone-family-with-descent-data-pushout R x
+  map-hom-descent-data-pushout =
+    pr1 (center uniqueness-map-hom-descent-data-pushout)
+
+  compute-left-map-map-hom-descent-data-pushout :
+    (a : domain-span-diagram 𝒮) →
+    coherence-square-maps
+      ( left-map-family-with-descent-data-pushout P a)
+      ( map-hom-descent-data-pushout (horizontal-map-cocone _ _ c a))
+      ( left-map-hom-descent-data-pushout
+        ( descent-data-family-with-descent-data-pushout P)
+        ( descent-data-family-with-descent-data-pushout R)
+        ( m)
+        ( a))
+      ( left-map-family-with-descent-data-pushout R a)
+  compute-left-map-map-hom-descent-data-pushout a =
+    map-inv-equiv
+      ( equiv-coherence-triangle-maps-inv-top'
+        ( left-map-family-with-descent-data-pushout R a ∘
+          map-hom-descent-data-pushout (horizontal-map-cocone _ _ c a))
+        ( left-map-hom-descent-data-pushout
+          ( descent-data-family-with-descent-data-pushout P)
+          ( descent-data-family-with-descent-data-pushout R)
+          ( m)
+          ( a))
+        ( left-equiv-family-with-descent-data-pushout P a))
+      ( pr1 (pr2 (center uniqueness-map-hom-descent-data-pushout)) a)
+
+  compute-right-map-map-hom-descent-data-pushout :
+    (b : codomain-span-diagram 𝒮) →
+    coherence-square-maps
+      ( right-map-family-with-descent-data-pushout P b)
+      ( map-hom-descent-data-pushout (vertical-map-cocone _ _ c b))
+      ( right-map-hom-descent-data-pushout
+        ( descent-data-family-with-descent-data-pushout P)
+        ( descent-data-family-with-descent-data-pushout R)
+        ( m)
+        ( b))
+      ( right-map-family-with-descent-data-pushout R b)
+  compute-right-map-map-hom-descent-data-pushout b =
+    map-inv-equiv
+      ( equiv-coherence-triangle-maps-inv-top'
+        ( right-map-family-with-descent-data-pushout R b ∘
+          map-hom-descent-data-pushout (vertical-map-cocone _ _ c b))
+        ( right-map-hom-descent-data-pushout
+          ( descent-data-family-with-descent-data-pushout P)
+          ( descent-data-family-with-descent-data-pushout R)
+          ( m)
+          ( b))
+        ( right-equiv-family-with-descent-data-pushout P b))
+      ( pr1 (pr2 (pr2 (center uniqueness-map-hom-descent-data-pushout))) b)
+```
diff --git a/src/synthetic-homotopy-theory/descent-data-identity-types-over-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-identity-types-over-pushouts.lagda.md
new file mode 100644
index 0000000000..6244d587ce
--- /dev/null
+++ b/src/synthetic-homotopy-theory/descent-data-identity-types-over-pushouts.lagda.md
@@ -0,0 +1,95 @@
+# Descent data for type families of identity types over pushouts
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module synthetic-homotopy-theory.descent-data-identity-types-over-pushouts where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.identity-types
+open import foundation.span-diagrams
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.descent-data-pushouts
+open import synthetic-homotopy-theory.equivalences-descent-data-pushouts
+open import synthetic-homotopy-theory.families-descent-data-pushouts
+```
+
+</details>
+
+## Idea
+
+Given a [cocone](synthetic-homotopy-theory.cocones-under-spans.md) under a
+[span diagram](foundation.span-diagrams.md)
+
+```text
+        g
+    S -----> B
+    |        |
+  f |        | j
+    ∨        ∨
+    A -----> X
+        i
+```
+
+and a point `x₀ : X`, the type family of
+[identity types](foundation-core.identity-types.md) based at `x₀`,
+`x ↦ (x₀ = x)`, is
+[characterized](synthetic-homotopy-theory.families-descent-data-pushouts.md) by
+the [descent data](synthetic-homotopy-theory.descent-data-pushouts.md)
+`(IA, IB, IS)`, where `IA` and `IB` are families of identity types
+
+```text
+  IA a := (x₀ = ia)
+  IB b := (x₀ = jb),
+```
+
+and the gluing data `IS s : (x₀ = ifs) ≃ (x₀ = jgs)` is given by concatenation
+with the coherence of the cocone `H s : ifs = jgs`.
+
+## Definitions
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {X : UU l4} (c : cocone-span-diagram 𝒮 X)
+  (x₀ : X)
+  where
+
+  family-cocone-identity-type-pushout : X → UU l4
+  family-cocone-identity-type-pushout x = x₀ ＝ x
+
+  descent-data-identity-type-pushout : descent-data-pushout 𝒮 l4
+  pr1 descent-data-identity-type-pushout a =
+    x₀ ＝ horizontal-map-cocone _ _ c a
+  pr1 (pr2 descent-data-identity-type-pushout) b =
+    x₀ ＝ vertical-map-cocone _ _ c b
+  pr2 (pr2 descent-data-identity-type-pushout) s =
+    equiv-concat' x₀ (coherence-square-cocone _ _ c s)
+
+  equiv-descent-data-identity-type-pushout :
+    equiv-descent-data-pushout
+      ( descent-data-family-cocone-span-diagram c
+        ( family-cocone-identity-type-pushout))
+      ( descent-data-identity-type-pushout)
+  pr1 equiv-descent-data-identity-type-pushout a = id-equiv
+  pr1 (pr2 equiv-descent-data-identity-type-pushout) b = id-equiv
+  pr2 (pr2 equiv-descent-data-identity-type-pushout) s =
+    tr-Id-right (coherence-square-cocone _ _ c s)
+
+  family-with-descent-data-identity-type-pushout :
+    family-with-descent-data-pushout c l4
+  pr1 family-with-descent-data-identity-type-pushout =
+    family-cocone-identity-type-pushout
+  pr1 (pr2 family-with-descent-data-identity-type-pushout) =
+    descent-data-identity-type-pushout
+  pr2 (pr2 family-with-descent-data-identity-type-pushout) =
+    equiv-descent-data-identity-type-pushout
+```
diff --git a/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
index 66b2c0803f..a95a4a12a1 100644
--- a/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
@@ -121,6 +121,13 @@ module _
     is-equiv-left-map-equiv-descent-data-pushout a =
       is-equiv-map-equiv (left-equiv-equiv-descent-data-pushout a)
 
+    inv-left-map-equiv-descent-data-pushout :
+      (a : domain-span-diagram 𝒮) →
+      left-family-descent-data-pushout Q a →
+      left-family-descent-data-pushout P a
+    inv-left-map-equiv-descent-data-pushout a =
+      map-inv-equiv (left-equiv-equiv-descent-data-pushout a)
+
     right-equiv-equiv-descent-data-pushout :
       (b : codomain-span-diagram 𝒮) →
       right-family-descent-data-pushout P b ≃
@@ -140,6 +147,13 @@ module _
     is-equiv-right-map-equiv-descent-data-pushout b =
       is-equiv-map-equiv (right-equiv-equiv-descent-data-pushout b)
 
+    inv-right-map-equiv-descent-data-pushout :
+      (b : codomain-span-diagram 𝒮) →
+      right-family-descent-data-pushout Q b →
+      right-family-descent-data-pushout P b
+    inv-right-map-equiv-descent-data-pushout b =
+      map-inv-equiv (right-equiv-equiv-descent-data-pushout b)
+
     coherence-equiv-descent-data-pushout :
       (s : spanning-type-span-diagram 𝒮) →
       coherence-square-maps
diff --git a/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md
index ec5d935b6c..573147d1a5 100644
--- a/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md
@@ -145,6 +145,18 @@ module _
       ( descent-data-family-with-descent-data-pushout)
       ( equiv-descent-data-family-with-descent-data-pushout)
 
+  inv-left-map-family-with-descent-data-pushout :
+    (a : domain-span-diagram 𝒮) →
+    left-family-family-with-descent-data-pushout a →
+    family-cocone-family-with-descent-data-pushout
+      ( horizontal-map-cocone _ _ c a)
+  inv-left-map-family-with-descent-data-pushout =
+    inv-left-map-equiv-descent-data-pushout
+      ( descent-data-family-cocone-span-diagram c
+        ( family-cocone-family-with-descent-data-pushout))
+      ( descent-data-family-with-descent-data-pushout)
+      ( equiv-descent-data-family-with-descent-data-pushout)
+
   right-equiv-family-with-descent-data-pushout :
     (b : codomain-span-diagram 𝒮) →
     family-cocone-family-with-descent-data-pushout
@@ -169,6 +181,28 @@ module _
       ( descent-data-family-with-descent-data-pushout)
       ( equiv-descent-data-family-with-descent-data-pushout)
 
+  is-equiv-right-map-family-with-descent-data-pushout :
+    (b : codomain-span-diagram 𝒮) →
+    is-equiv (right-map-family-with-descent-data-pushout b)
+  is-equiv-right-map-family-with-descent-data-pushout =
+    is-equiv-right-map-equiv-descent-data-pushout
+      ( descent-data-family-cocone-span-diagram c
+        ( family-cocone-family-with-descent-data-pushout))
+      ( descent-data-family-with-descent-data-pushout)
+      ( equiv-descent-data-family-with-descent-data-pushout)
+
+  inv-right-map-family-with-descent-data-pushout :
+    (b : codomain-span-diagram 𝒮) →
+    right-family-family-with-descent-data-pushout b →
+    family-cocone-family-with-descent-data-pushout
+      ( vertical-map-cocone _ _ c b)
+  inv-right-map-family-with-descent-data-pushout =
+    inv-right-map-equiv-descent-data-pushout
+      ( descent-data-family-cocone-span-diagram c
+        ( family-cocone-family-with-descent-data-pushout))
+      ( descent-data-family-with-descent-data-pushout)
+      ( equiv-descent-data-family-with-descent-data-pushout)
+
   coherence-family-with-descent-data-pushout :
     (s : spanning-type-span-diagram 𝒮) →
     coherence-square-maps
diff --git a/src/synthetic-homotopy-theory/sections-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/sections-descent-data-pushouts.lagda.md
new file mode 100644
index 0000000000..583235db13
--- /dev/null
+++ b/src/synthetic-homotopy-theory/sections-descent-data-pushouts.lagda.md
@@ -0,0 +1,429 @@
+# Sections of descent data for pushouts
+
+```agda
+module synthetic-homotopy-theory.sections-descent-data-pushouts where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-dependent-functions
+open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-identifications
+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.embeddings
+open import foundation.equivalences
+open import foundation.fibers-of-maps
+open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
+open import foundation.homotopy-induction
+open import foundation.identity-types
+open import foundation.span-diagrams
+open import foundation.structure-identity-principle
+open import foundation.torsorial-type-families
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.dependent-cocones-under-spans
+open import synthetic-homotopy-theory.dependent-universal-property-pushouts
+open import synthetic-homotopy-theory.descent-data-pushouts
+open import synthetic-homotopy-theory.families-descent-data-pushouts
+open import synthetic-homotopy-theory.universal-property-pushouts
+```
+
+</details>
+
+## Idea
+
+Given [descent data](synthetic-homotopy-theory.descent-data-pushouts.md)
+`(PA, PB, PS)` for the [pushout](synthetic-homotopy-theory.pushouts.md) of a
+[span diagram](foundation.span-diagrams.md) `𝒮`, we define the type of
+{{#concept "sections" Disambiguation="descent data for pushouts" Agda=section-descent-data-pushout}}
+to be the type of triples `(tA, tB, tS)`, where
+
+```text
+  tA : (a : A) → PA a
+  tB : (b : B) → PB b
+```
+
+are [sections](foundation.dependent-function-types.md) of the type families `PA`
+and `PB`, respectively, and `tS` is a coherence datum, witnessing that for every
+`s : S`, the dependent triangle
+
+```text
+           tA ∘ f
+  (s : S) --------> PA (f s)
+          \       /
+    tB ∘ g  \   / PS s
+             ∨ ∨
+          PB (g s)
+```
+
+[commutes](foundation.commuting-triangles-of-maps.md).
+
+We show that for a
+[family with descent data](synthetic-homotopy-theory.families-descent-data-pushouts.md)
+`P ≈ (PA, PB, PS)`, the type of sections `(x : X) → P x` of `P` is
+[equivalent](foundation-core.equivalences.md) to the type of sections of
+`(PA, PB, PS)`.
+
+Furthermore, a
+{{#concept "homotopy" Disambiguation="sections of descent data for pushouts" Agda=htpy-section-descent-data-pushout}}
+between sections `(tA, tB, tS)` and `(rA, rB, rS)` consists of component-wise
+[homotopies](foundation-core.homotopies.md)
+
+```text
+  HA : tA ~ rA
+  HB : tB ~ rB
+```
+
+and a coherence datum `HS`, witnessing that for each `s : S`, the square of
+identifications
+
+```text
+               PS s ·l HA fs
+  PS s (tA fs) ------------> PS s (rA fs)
+       |                          |
+  tS s |                          | rS s
+       |                          |
+       ∨                          ∨
+     tB gs -------------------> rB gs
+                   HB gs
+```
+
+[commutes](foundation-core.commuting-squares-of-identifications.md).
+
+We show that the identity types of sections of descent data are characterized by
+homotopies between them.
+
+## Definitions
+
+### Sections of descent data for pushouts
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
+  where
+
+  section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  section-descent-data-pushout =
+    Σ ( (a : domain-span-diagram 𝒮) → left-family-descent-data-pushout P a)
+      ( λ tA →
+        Σ ( (b : codomain-span-diagram 𝒮) →
+            right-family-descent-data-pushout P b)
+          ( λ tB →
+            (s : spanning-type-span-diagram 𝒮) →
+            map-family-descent-data-pushout P s
+              ( tA (left-map-span-diagram 𝒮 s)) ＝
+            tB (right-map-span-diagram 𝒮 s)))
+
+  module _
+    (t : section-descent-data-pushout)
+    where
+
+    left-map-section-descent-data-pushout :
+      (a : domain-span-diagram 𝒮) → left-family-descent-data-pushout P a
+    left-map-section-descent-data-pushout = pr1 t
+
+    right-map-section-descent-data-pushout :
+      (b : codomain-span-diagram 𝒮) → right-family-descent-data-pushout P b
+    right-map-section-descent-data-pushout = pr1 (pr2 t)
+
+    coherence-section-descent-data-pushout :
+      (s : spanning-type-span-diagram 𝒮) →
+      map-family-descent-data-pushout P s
+        ( left-map-section-descent-data-pushout (left-map-span-diagram 𝒮 s)) ＝
+      right-map-section-descent-data-pushout (right-map-span-diagram 𝒮 s)
+    coherence-section-descent-data-pushout = pr2 (pr2 t)
+```
+
+### Homotopies of sections of descent data for pushouts
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
+  (r t : section-descent-data-pushout P)
+  where
+
+  htpy-section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  htpy-section-descent-data-pushout =
+    Σ ( left-map-section-descent-data-pushout P r ~
+        left-map-section-descent-data-pushout P t)
+      ( λ HA →
+        Σ ( right-map-section-descent-data-pushout P r ~
+            right-map-section-descent-data-pushout P t)
+          ( λ HB →
+            (s : spanning-type-span-diagram 𝒮) →
+            coherence-square-identifications
+              ( ap
+                ( map-family-descent-data-pushout P s)
+                ( HA (left-map-span-diagram 𝒮 s)))
+              ( coherence-section-descent-data-pushout P r s)
+              ( coherence-section-descent-data-pushout P t s)
+              ( HB (right-map-span-diagram 𝒮 s))))
+```
+
+### The reflexive homotopy of sections of descent data for pushouts
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
+  (r : section-descent-data-pushout P)
+  where
+
+  refl-htpy-section-descent-data-pushout :
+    htpy-section-descent-data-pushout P r r
+  pr1 refl-htpy-section-descent-data-pushout = refl-htpy
+  pr1 (pr2 refl-htpy-section-descent-data-pushout) = refl-htpy
+  pr2 (pr2 refl-htpy-section-descent-data-pushout) = right-unit-htpy
+```
+
+## Properties
+
+### Characterization of identity types of sections of descent data for pushouts
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
+  (r : section-descent-data-pushout P)
+  where
+
+  htpy-eq-section-descent-data-pushout :
+    (t : section-descent-data-pushout P) →
+    (r ＝ t) → htpy-section-descent-data-pushout P r t
+  htpy-eq-section-descent-data-pushout .r refl =
+    refl-htpy-section-descent-data-pushout P r
+
+  abstract
+    is-torsorial-htpy-section-descent-data-pushout :
+      is-torsorial (htpy-section-descent-data-pushout P r)
+    is-torsorial-htpy-section-descent-data-pushout =
+      is-torsorial-Eq-structure
+        ( is-torsorial-htpy (left-map-section-descent-data-pushout P r))
+        ( left-map-section-descent-data-pushout P r , refl-htpy)
+        ( is-torsorial-Eq-structure
+          ( is-torsorial-htpy (right-map-section-descent-data-pushout P r))
+          ( right-map-section-descent-data-pushout P r , refl-htpy)
+          ( is-torsorial-htpy
+            ( coherence-section-descent-data-pushout P r ∙h refl-htpy)))
+
+  is-equiv-htpy-eq-section-descent-data-pushout :
+    (t : section-descent-data-pushout P) →
+    is-equiv (htpy-eq-section-descent-data-pushout t)
+  is-equiv-htpy-eq-section-descent-data-pushout =
+    fundamental-theorem-id
+      ( is-torsorial-htpy-section-descent-data-pushout)
+      ( htpy-eq-section-descent-data-pushout)
+
+  extensionality-section-descent-data-pushout :
+    (t : section-descent-data-pushout P) →
+    (r ＝ t) ≃ htpy-section-descent-data-pushout P r t
+  pr1 (extensionality-section-descent-data-pushout t) =
+    htpy-eq-section-descent-data-pushout t
+  pr2 (extensionality-section-descent-data-pushout t) =
+    is-equiv-htpy-eq-section-descent-data-pushout t
+```
+
+### Sections of families over a pushout correspond to sections of the corresponding descent data
+
+**Proof:** Given a family with descent data `P ≈ (PA, PB, PS)`, note that a
+section `t : (x : X) → P x` of `P` induces a section `(tA, tB, tS)` of
+`(PA, PB, PS)`, where
+
+```text
+  tA a := eA (tia)
+  tB b := eB (tjb),
+```
+
+and `tS s` is given by the chain of identifications
+
+```text
+  PS s (eA (tifs))
+  = eB (tr P (H s) (tifs))   by coherence of P ≈ (PA, PB, PS)
+  = eB (tjgs)                by apd t (H s)
+```
+
+This map factors through the dependent cocone map
+
+```text
+                dependent-cocone-map
+  (x : X) → P x --------------------> dependent-cocone P
+                \                  /
+                  \              /
+                    \          /
+                      ∨      ∨
+                section (PA, PB, PS),
+```
+
+where the right map takes `(dA, dB, dS)` to
+
+```text
+  tA a := eA (dA a)
+  tB b := eB (dB a)
+  tS s : PS s (eA (dA fs))
+         = eB (tr P (H s) (dA fs))  by coherence of P ≈ (PA, PB, PS)
+         = eB (dB gs)               by dS.
+```
+
+The top map is an equivalence, since we assume `X` to be a pushout, and the
+right map is an equivalence, since concatenating an identification is an
+equivalence, and the action on identifications of equivalences is an
+equivalence. It follows that the left map is an equivalence
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {X : UU l4} {c : cocone-span-diagram 𝒮 X}
+  (P : family-with-descent-data-pushout c l5)
+  where
+
+  section-descent-data-section-family-cocone-span-diagram :
+    ((x : X) → family-cocone-family-with-descent-data-pushout P x) →
+    section-descent-data-pushout
+      ( descent-data-family-with-descent-data-pushout P)
+  pr1 (section-descent-data-section-family-cocone-span-diagram f) a =
+    left-map-family-with-descent-data-pushout P a
+      ( f (horizontal-map-cocone _ _ c a))
+  pr1 (pr2 (section-descent-data-section-family-cocone-span-diagram f)) b =
+    right-map-family-with-descent-data-pushout P b
+      ( f (vertical-map-cocone _ _ c b))
+  pr2 (pr2 (section-descent-data-section-family-cocone-span-diagram f)) s =
+    ( inv
+      ( coherence-family-with-descent-data-pushout P s
+        ( f (horizontal-map-cocone _ _ c (left-map-span-diagram 𝒮 s))))) ∙
+    ( ap
+      ( right-map-family-with-descent-data-pushout P
+        ( right-map-span-diagram 𝒮 s))
+      ( apd f (coherence-square-cocone _ _ c s)))
+
+  section-descent-data-dependent-cocone-span-diagram :
+    dependent-cocone-span-diagram c
+      ( family-cocone-family-with-descent-data-pushout P) →
+    section-descent-data-pushout
+      ( descent-data-family-with-descent-data-pushout P)
+  pr1 (section-descent-data-dependent-cocone-span-diagram d) a =
+    left-map-family-with-descent-data-pushout P a
+      ( horizontal-map-dependent-cocone _ _ _ _ d a)
+  pr1 (pr2 (section-descent-data-dependent-cocone-span-diagram d)) b =
+    right-map-family-with-descent-data-pushout P b
+      ( vertical-map-dependent-cocone _ _ _ _ d b)
+  pr2 (pr2 (section-descent-data-dependent-cocone-span-diagram d)) s =
+    ( inv (coherence-family-with-descent-data-pushout P s _)) ∙
+    ( ap
+      ( right-map-family-with-descent-data-pushout P
+        ( right-map-span-diagram 𝒮 s))
+      ( coherence-square-dependent-cocone _ _ _ _ d s))
+
+  abstract
+    is-equiv-section-descent-data-depedent-cocone-span-diagram :
+      is-equiv section-descent-data-dependent-cocone-span-diagram
+    is-equiv-section-descent-data-depedent-cocone-span-diagram =
+      is-equiv-map-Σ _
+        ( is-equiv-map-Π-is-fiberwise-equiv
+          ( is-equiv-left-map-family-with-descent-data-pushout P))
+        ( λ tA →
+          is-equiv-map-Σ _
+            ( is-equiv-map-Π-is-fiberwise-equiv
+              ( is-equiv-right-map-family-with-descent-data-pushout P))
+            ( λ tB →
+              is-equiv-map-Π-is-fiberwise-equiv
+                ( λ s →
+                  is-equiv-comp _ _
+                    ( is-emb-equiv
+                      ( right-equiv-family-with-descent-data-pushout P
+                        ( right-map-span-diagram 𝒮 s))
+                      ( _)
+                      ( _))
+                    ( is-equiv-inv-concat _ _))))
+
+  triangle-section-descent-data-section-family-cocone-span-diagram :
+    coherence-triangle-maps
+      ( section-descent-data-section-family-cocone-span-diagram)
+      ( section-descent-data-dependent-cocone-span-diagram)
+      ( dependent-cocone-map-span-diagram c
+        ( family-cocone-family-with-descent-data-pushout P))
+  triangle-section-descent-data-section-family-cocone-span-diagram = refl-htpy
+
+  abstract
+    is-equiv-section-descent-data-section-family-cocone-span-diagram :
+      universal-property-pushout _ _ c →
+      is-equiv (section-descent-data-section-family-cocone-span-diagram)
+    is-equiv-section-descent-data-section-family-cocone-span-diagram up-c =
+      is-equiv-left-map-triangle
+        ( section-descent-data-section-family-cocone-span-diagram)
+        ( section-descent-data-dependent-cocone-span-diagram)
+        ( dependent-cocone-map-span-diagram c
+          ( family-cocone-family-with-descent-data-pushout P))
+        ( triangle-section-descent-data-section-family-cocone-span-diagram)
+        ( dependent-universal-property-universal-property-pushout _ _ _ up-c
+          ( family-cocone-family-with-descent-data-pushout P))
+        ( is-equiv-section-descent-data-depedent-cocone-span-diagram)
+```
+
+As a corollary, for any given section `(tA, tB, tS)` of `(PA, PB, PS)`, there is
+a unique section `t : (x : X) → P x` of `P` such that its induced section of
+`(PA, PB, PS)` is homotopic to `(tA, tB, tS)`.
+
+**Proof:** Since the map taking sections of `P` to sections of `(PA, PB, PS)` is
+an equivalence, it has contractible fibers. The fiber at `(tA, tB, tS)` is the
+type of sections of `P` that induce a section of `(PA, PB, PS)` which is
+identified with `(tA, tB, tS)`, and such identifications are characterized by
+homotopies of sections of `(PA, PB, PS)`.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {X : UU l4} {c : cocone-span-diagram 𝒮 X}
+  (up-c : universal-property-pushout _ _ c)
+  (P : family-with-descent-data-pushout c l5)
+  (t :
+    section-descent-data-pushout
+      ( descent-data-family-with-descent-data-pushout P))
+  where
+
+  abstract
+    uniqueness-section-family-section-descent-data-pushout :
+      is-contr
+        ( Σ ( (x : X) → family-cocone-family-with-descent-data-pushout P x)
+            ( λ h →
+              htpy-section-descent-data-pushout
+                ( descent-data-family-with-descent-data-pushout P)
+                ( section-descent-data-section-family-cocone-span-diagram P h)
+                ( t)))
+    uniqueness-section-family-section-descent-data-pushout =
+      is-contr-equiv'
+        ( fiber (section-descent-data-section-family-cocone-span-diagram P) t)
+        ( equiv-tot
+          ( λ h →
+            extensionality-section-descent-data-pushout
+              ( descent-data-family-with-descent-data-pushout P)
+              ( _)
+              ( t)))
+        ( is-contr-map-is-equiv
+          ( is-equiv-section-descent-data-section-family-cocone-span-diagram P
+            ( up-c))
+          ( t))
+
+  section-family-section-descent-data-pushout :
+    (x : X) → family-cocone-family-with-descent-data-pushout P x
+  section-family-section-descent-data-pushout =
+    pr1 (center uniqueness-section-family-section-descent-data-pushout)
+
+  htpy-section-family-section-descent-data-pushout :
+    htpy-section-descent-data-pushout
+      ( descent-data-family-with-descent-data-pushout P)
+      ( section-descent-data-section-family-cocone-span-diagram P
+        ( section-family-section-descent-data-pushout))
+      ( t)
+  htpy-section-family-section-descent-data-pushout =
+    pr2 (center uniqueness-section-family-section-descent-data-pushout)
+```