diff --git a/codespell-dictionary.txt b/codespell-dictionary.txt
index 0f87b4ee0b..61dc2a0609 100644
--- a/codespell-dictionary.txt
+++ b/codespell-dictionary.txt
@@ -4,11 +4,15 @@ Kuratowsky->Kuratowski
 Lavwere->Lawvere
 anamorhpism->anamorphism
 anamorhpisms->anamorphisms
+anamorhpsim->anamorphism
+anamorhpsims->anamorphisms
 anamorphsim->anamorphism
 anamorphsim->anamorphism
 anamorphsims->anamorphisms
 automorhpism->automorphism
 automorhpisms->automorphisms
+automorhpsim->automorphism
+automorhpsims->automorphisms
 automorphsim->automorphism
 automorphsims->automorphisms
 cagegory->category
@@ -16,27 +20,39 @@ consistsing->consisting
 eacy->each,easy
 endomorhpism->endomorphism
 endomorhpisms->endomorphisms
+endomorhpsim->endomorphism
+endomorhpsims->endomorphisms
 endomorphsim->endomorphism
 endomorphsims->endomorphisms
 epimorhpism->epimorphism
 epimorhpisms->epimorphisms
+epimorhpsim->epimorphism
+epimorhpsims->epimorphisms
 epimorphsim->epimorphism
 epimorphsims->epimorphisms
 foundaiton->foundation
 homomorhpism->homomorphism
 homomorhpisms->homomorphisms
+homomorhpsim->homomorphism
+homomorhpsims->homomorphisms
 homomorphsim->homomorphism
 homomorphsims->homomorphisms
 isomorhpism->isomorphism
 isomorhpisms->isomorphisms
+isomorhpsim->isomorphism
+isomorhpsims->isomorphisms
 isomorphsim->isomorphism
 isomorphsims->isomorphisms
 monomorhpism->monomorphism
 monomorhpisms->monomorphisms
+monomorhpsim->monomorphism
+monomorhpsims->monomorphisms
 monomorphsim->monomorphism
 monomorphsims->monomorphisms
 morhpism->morphism
 morhpisms->morphisms
+morhpsim->morphism
+morhpsims->morphisms
 morphsim->morphism
 morphsims->morphisms
 outout->output
diff --git a/references.bib b/references.bib
index 497d9567bd..d3df3f0b4e 100644
--- a/references.bib
+++ b/references.bib
@@ -659,6 +659,15 @@ @phdthesis{Qui16
   langid        = {english},
 }
 
+@online{Rezk10HomotopyToposes,
+  title         = {Toposes and homotopy toposes},
+  author        = {Rezk, Charles},
+  year          = 2010,
+  month         = {01},
+  url           = {https://rezk.web.illinois.edu/homotopy-topos-sketch.pdf},
+  version       = {0.15},
+}
+
 @book{Rie17,
   title         = {Category {{Theory}} in {{Context}}},
   author        = {Riehl, Emily},
diff --git a/src/foundation-core/fibers-of-maps.lagda.md b/src/foundation-core/fibers-of-maps.lagda.md
index 12a441cd2d..0376de9e04 100644
--- a/src/foundation-core/fibers-of-maps.lagda.md
+++ b/src/foundation-core/fibers-of-maps.lagda.md
@@ -52,6 +52,13 @@ module _
 
   compute-value-inclusion-fiber : (y : fiber f b) → f (inclusion-fiber y) ＝ b
   compute-value-inclusion-fiber = pr2
+
+  inclusion-fiber' : fiber' f b → A
+  inclusion-fiber' = pr1
+
+  compute-value-inclusion-fiber' :
+    (y : fiber' f b) → b ＝ f (inclusion-fiber' y)
+  compute-value-inclusion-fiber' = pr2
 ```
 
 ## Properties
@@ -280,9 +287,7 @@ module _
   triangle-map-equiv-total-fiber t = inv (pr2 (pr2 t))
 
   map-inv-equiv-total-fiber : A → Σ B (fiber f)
-  pr1 (map-inv-equiv-total-fiber x) = f x
-  pr1 (pr2 (map-inv-equiv-total-fiber x)) = x
-  pr2 (pr2 (map-inv-equiv-total-fiber x)) = refl
+  map-inv-equiv-total-fiber x = (f x , x , refl)
 
   is-retraction-map-inv-equiv-total-fiber :
     is-retraction map-equiv-total-fiber map-inv-equiv-total-fiber
@@ -316,6 +321,51 @@ module _
   pr2 inv-equiv-total-fiber = is-equiv-map-inv-equiv-total-fiber
 ```
 
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  map-equiv-total-fiber' : Σ B (fiber' f) → A
+  map-equiv-total-fiber' t = pr1 (pr2 t)
+
+  triangle-map-equiv-total-fiber' : pr1 ~ f ∘ map-equiv-total-fiber'
+  triangle-map-equiv-total-fiber' t = pr2 (pr2 t)
+
+  map-inv-equiv-total-fiber' : A → Σ B (fiber' f)
+  map-inv-equiv-total-fiber' x = (f x , x , refl)
+
+  is-retraction-map-inv-equiv-total-fiber' :
+    is-retraction map-equiv-total-fiber' map-inv-equiv-total-fiber'
+  is-retraction-map-inv-equiv-total-fiber' (.(f x) , x , refl) = refl
+
+  is-section-map-inv-equiv-total-fiber' :
+    is-section map-equiv-total-fiber' map-inv-equiv-total-fiber'
+  is-section-map-inv-equiv-total-fiber' x = refl
+
+  is-equiv-map-equiv-total-fiber' : is-equiv map-equiv-total-fiber'
+  is-equiv-map-equiv-total-fiber' =
+    is-equiv-is-invertible
+      map-inv-equiv-total-fiber'
+      is-section-map-inv-equiv-total-fiber'
+      is-retraction-map-inv-equiv-total-fiber'
+
+  is-equiv-map-inv-equiv-total-fiber' : is-equiv map-inv-equiv-total-fiber'
+  is-equiv-map-inv-equiv-total-fiber' =
+    is-equiv-is-invertible
+      map-equiv-total-fiber'
+      is-retraction-map-inv-equiv-total-fiber'
+      is-section-map-inv-equiv-total-fiber'
+
+  equiv-total-fiber' : Σ B (fiber' f) ≃ A
+  pr1 equiv-total-fiber' = map-equiv-total-fiber'
+  pr2 equiv-total-fiber' = is-equiv-map-equiv-total-fiber'
+
+  inv-equiv-total-fiber' : A ≃ Σ B (fiber' f)
+  pr1 inv-equiv-total-fiber' = map-inv-equiv-total-fiber'
+  pr2 inv-equiv-total-fiber' = is-equiv-map-inv-equiv-total-fiber'
+```
+
 ### Fibers of compositions
 
 ```agda
diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md
index 332e6e96e2..0170c208fc 100644
--- a/src/foundation-core/pullbacks.lagda.md
+++ b/src/foundation-core/pullbacks.lagda.md
@@ -309,6 +309,86 @@ the vertical maps is a family of equivalences
               f
 ```
 
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
+  (f : A → X) (g : B → X) (c : cone f g C)
+  where
+
+  triangle-tot-map-fiber-vertical-map-cone' :
+    tot (map-fiber-vertical-map-cone' f g c) ~
+    gap f g c ∘ map-equiv-total-fiber' (vertical-map-cone f g c)
+  triangle-tot-map-fiber-vertical-map-cone'
+    (.(vertical-map-cone f g c x) , x , refl) = refl
+
+  abstract
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' :
+      is-pullback f g c →
+      is-fiberwise-equiv (map-fiber-vertical-map-cone' f g c)
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb =
+      is-fiberwise-equiv-is-equiv-tot
+        ( is-equiv-left-map-triangle
+          ( tot (map-fiber-vertical-map-cone' f g c))
+          ( gap f g c)
+          ( map-equiv-total-fiber' (vertical-map-cone f g c))
+          ( triangle-tot-map-fiber-vertical-map-cone')
+          ( is-equiv-map-equiv-total-fiber' (vertical-map-cone f g c))
+          ( pb))
+
+  fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' :
+      is-pullback f g c → (x : A) →
+      fiber' (vertical-map-cone f g c) x ≃ fiber' g (f x)
+  fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb x =
+    ( map-fiber-vertical-map-cone' f g c x ,
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb x)
+
+  equiv-tot-map-fiber-vertical-map-cone-is-pullback' :
+      is-pullback f g c →
+      Σ A (fiber' (vertical-map-cone f g c)) ≃ Σ A (fiber' g ∘ f)
+  equiv-tot-map-fiber-vertical-map-cone-is-pullback' pb =
+    equiv-tot (fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb)
+
+  abstract
+    is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone' :
+      is-fiberwise-equiv (map-fiber-vertical-map-cone' f g c) →
+      is-pullback f g c
+    is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone' is-equiv-fsq =
+      is-equiv-right-map-triangle
+        ( tot (map-fiber-vertical-map-cone' f g c))
+        ( gap f g c)
+        ( map-equiv-total-fiber' (vertical-map-cone f g c))
+        ( triangle-tot-map-fiber-vertical-map-cone')
+        ( is-equiv-tot-is-fiberwise-equiv is-equiv-fsq)
+        ( is-equiv-map-equiv-total-fiber' (vertical-map-cone f g c))
+
+  abstract
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' :
+      universal-property-pullback f g c →
+      is-fiberwise-equiv (map-fiber-vertical-map-cone' f g c)
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+      up =
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback'
+        ( is-pullback-universal-property-pullback f g c up)
+
+  fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' :
+      universal-property-pullback f g c → (x : A) →
+      fiber' (vertical-map-cone f g c) x ≃ fiber' g (f x)
+  fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+    pb x =
+    ( map-fiber-vertical-map-cone' f g c x ,
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+        ( pb)
+        ( x))
+
+  equiv-tot-map-fiber-vertical-map-cone-universal-property-pullback' :
+      universal-property-pullback f g c →
+      Σ A (fiber' (vertical-map-cone f g c)) ≃ Σ A (fiber' g ∘ f)
+  equiv-tot-map-fiber-vertical-map-cone-universal-property-pullback' pb =
+    equiv-tot
+      ( fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+        ( pb))
+```
+
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
@@ -356,6 +436,15 @@ module _
           ( λ x →
             is-equiv-tot-is-fiberwise-equiv (λ y → is-equiv-inv (g y) (f x))))
         ( is-equiv-tot-is-fiberwise-equiv is-equiv-fsq)
+
+  abstract
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback :
+      universal-property-pullback f g c →
+      is-fiberwise-equiv (map-fiber-vertical-map-cone f g c)
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback
+      up =
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
+        ( is-pullback-universal-property-pullback f g c up)
 ```
 
 ### A cone is a pullback if and only if it induces a family of equivalences between the fibers of the horizontal maps
diff --git a/src/foundation/equivalences-arrows.lagda.md b/src/foundation/equivalences-arrows.lagda.md
index 23e82b5948..de15f1eb08 100644
--- a/src/foundation/equivalences-arrows.lagda.md
+++ b/src/foundation/equivalences-arrows.lagda.md
@@ -87,8 +87,7 @@ module _
     coherence-hom-arrow f g (map-equiv i) (map-equiv j)
 
   equiv-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  equiv-arrow =
-    Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i))
+  equiv-arrow = Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i))
 
   module _
     (e : equiv-arrow)
@@ -100,6 +99,9 @@ module _
     map-domain-equiv-arrow : A → X
     map-domain-equiv-arrow = map-equiv equiv-domain-equiv-arrow
 
+    map-inv-domain-equiv-arrow : X → A
+    map-inv-domain-equiv-arrow = map-inv-equiv equiv-domain-equiv-arrow
+
     is-equiv-map-domain-equiv-arrow : is-equiv map-domain-equiv-arrow
     is-equiv-map-domain-equiv-arrow =
       is-equiv-map-equiv equiv-domain-equiv-arrow
@@ -110,6 +112,9 @@ module _
     map-codomain-equiv-arrow : B → Y
     map-codomain-equiv-arrow = map-equiv equiv-codomain-equiv-arrow
 
+    map-inv-codomain-equiv-arrow : Y → B
+    map-inv-codomain-equiv-arrow = map-inv-equiv equiv-codomain-equiv-arrow
+
     is-equiv-map-codomain-equiv-arrow : is-equiv map-codomain-equiv-arrow
     is-equiv-map-codomain-equiv-arrow =
       is-equiv-map-equiv equiv-codomain-equiv-arrow
diff --git a/src/foundation/fibers-of-maps.lagda.md b/src/foundation/fibers-of-maps.lagda.md
index 01e4a3f77b..c6205c190d 100644
--- a/src/foundation/fibers-of-maps.lagda.md
+++ b/src/foundation/fibers-of-maps.lagda.md
@@ -141,6 +141,45 @@ module _
     {y y' : B} (p : y ＝ y') (u : fiber f y) →
     tot (λ x → concat' _ p) u ＝ tr (fiber f) p u
   compute-tr-fiber refl u = ap (pair _) right-unit
+
+  inv-compute-tr-fiber :
+    {y y' : B} (p : y ＝ y') (u : fiber f y) →
+    tr (fiber f) p u ＝ tot (λ x → concat' _ p) u
+  inv-compute-tr-fiber p u = inv (compute-tr-fiber p u)
+
+  compute-tr-fiber' :
+    {y y' : B} (p : y ＝ y') (u : fiber' f y) →
+    tot (λ x q → inv p ∙ q) u ＝ tr (fiber' f) p u
+  compute-tr-fiber' refl u = refl
+
+  inv-compute-tr-fiber' :
+    {y y' : B} (p : y ＝ y') (u : fiber' f y) →
+    tr (fiber' f) p u ＝ tot (λ x q → inv p ∙ q) u
+  inv-compute-tr-fiber' p u = inv (compute-tr-fiber' p u)
+```
+
+### Transport in fibers along the fiber
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  compute-tr-self-fiber :
+    {y : B} (u : fiber f y) → (pr1 u , refl) ＝ tr (fiber f) (inv (pr2 u)) u
+  compute-tr-self-fiber (._ , refl) = refl
+
+  inv-compute-tr-self-fiber :
+    {y : B} (u : fiber f y) → tr (fiber f) (inv (pr2 u)) u ＝ (pr1 u , refl)
+  inv-compute-tr-self-fiber u = inv (compute-tr-self-fiber u)
+
+  compute-tr-self-fiber' :
+    {y : B} (u : fiber' f y) → (pr1 u , refl) ＝ tr (fiber' f) (pr2 u) u
+  compute-tr-self-fiber' (._ , refl) = refl
+
+  inv-compute-tr-self-fiber' :
+    {y : B} (u : fiber' f y) → tr (fiber' f) (pr2 u) u ＝ (pr1 u , refl)
+  inv-compute-tr-self-fiber' u = inv (compute-tr-self-fiber' u)
 ```
 
 ## Table of files about fibers of maps
diff --git a/src/foundation/functoriality-fibers-of-maps.lagda.md b/src/foundation/functoriality-fibers-of-maps.lagda.md
index 9a6698953a..7ecce36751 100644
--- a/src/foundation/functoriality-fibers-of-maps.lagda.md
+++ b/src/foundation/functoriality-fibers-of-maps.lagda.md
@@ -103,6 +103,41 @@ module _
   pr1 hom-arrow-fiber = map-domain-hom-arrow-fiber
   pr1 (pr2 hom-arrow-fiber) = map-codomain-hom-arrow-fiber
   pr2 (pr2 hom-arrow-fiber) = coh-hom-arrow-fiber
+
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y) (α : hom-arrow f g) (b : B)
+  where
+
+  map-domain-hom-arrow-fiber' :
+    fiber' f b → fiber' g (map-codomain-hom-arrow f g α b)
+  map-domain-hom-arrow-fiber' =
+    map-Σ _
+      ( map-domain-hom-arrow f g α)
+      ( λ a p → ap (map-codomain-hom-arrow f g α) p ∙ coh-hom-arrow f g α a)
+
+  map-fiber' :
+    fiber' f b → fiber' g (map-codomain-hom-arrow f g α b)
+  map-fiber' = map-domain-hom-arrow-fiber'
+
+  map-codomain-hom-arrow-fiber' : A → X
+  map-codomain-hom-arrow-fiber' = map-domain-hom-arrow f g α
+
+  coh-hom-arrow-fiber' :
+    coherence-square-maps
+      ( map-domain-hom-arrow-fiber')
+      ( inclusion-fiber' f)
+      ( inclusion-fiber' g)
+      ( map-domain-hom-arrow f g α)
+  coh-hom-arrow-fiber' = refl-htpy
+
+  hom-arrow-fiber' :
+    hom-arrow
+      ( inclusion-fiber' f {b})
+      ( inclusion-fiber' g {map-codomain-hom-arrow f g α b})
+  pr1 hom-arrow-fiber' = map-domain-hom-arrow-fiber'
+  pr1 (pr2 hom-arrow-fiber') = map-codomain-hom-arrow-fiber'
+  pr2 (pr2 hom-arrow-fiber') = coh-hom-arrow-fiber'
 ```
 
 ### Any cone induces a family of maps between the fibers of the vertical maps
@@ -121,6 +156,15 @@ module _
       ( g)
       ( hom-arrow-cone f g c)
       ( a)
+
+  map-fiber-vertical-map-cone' :
+    fiber' (vertical-map-cone f g c) a → fiber' g (f a)
+  map-fiber-vertical-map-cone' =
+    map-domain-hom-arrow-fiber'
+      ( vertical-map-cone f g c)
+      ( g)
+      ( hom-arrow-cone f g c)
+      ( a)
 ```
 
 ### Any cone induces a family of maps between the fibers of the vertical maps
@@ -139,6 +183,15 @@ module _
       ( f)
       ( hom-arrow-cone' f g c)
       ( b)
+
+  map-fiber-horizontal-map-cone' :
+    fiber' (horizontal-map-cone f g c) b → fiber' f (g b)
+  map-fiber-horizontal-map-cone' =
+    map-domain-hom-arrow-fiber'
+      ( horizontal-map-cone f g c)
+      ( f)
+      ( hom-arrow-cone' f g c)
+      ( b)
 ```
 
 ### For any `f : A → B` and any identification `p : b ＝ b'` in `B`, we obtain a morphism of arrows between the fiber inclusion at `b` to the fiber inclusion at `b'`
diff --git a/src/foundation/morphisms-arrows.lagda.md b/src/foundation/morphisms-arrows.lagda.md
index b80513a416..7abfa99887 100644
--- a/src/foundation/morphisms-arrows.lagda.md
+++ b/src/foundation/morphisms-arrows.lagda.md
@@ -10,6 +10,8 @@ module foundation.morphisms-arrows where
 open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
+open import foundation.postcomposition-functions
+open import foundation.precomposition-functions
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
@@ -19,8 +21,6 @@ open import foundation-core.functoriality-dependent-function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
-open import foundation-core.postcomposition-functions
-open import foundation-core.precomposition-functions
 ```
 
 </details>
@@ -309,19 +309,25 @@ A morphism of arrows `α : f → g` gives a morphism of precomposition arrows
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level}
+  {l1 l2 l3 l4 l : Level}
   {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
   (f : A → B) (g : X → Y) (α : hom-arrow f g)
+  (S : UU l)
   where
 
-  precomp-hom-arrow :
-    {l : Level} (S : UU l) → hom-arrow (precomp g S) (precomp f S)
-  pr1 (precomp-hom-arrow S) =
-    precomp (map-codomain-hom-arrow f g α) S
-  pr1 (pr2 (precomp-hom-arrow S)) =
-    precomp (map-domain-hom-arrow f g α) S
-  pr2 (pr2 (precomp-hom-arrow S)) h =
-    inv (eq-htpy (h ·l coh-hom-arrow f g α))
+  transpose-precomp-hom-arrow :
+    hom-arrow
+      ( precomp (map-codomain-hom-arrow f g α) S)
+      ( precomp (map-domain-hom-arrow f g α) S)
+  transpose-precomp-hom-arrow =
+    ( precomp g S , precomp f S , htpy-precomp (coh-hom-arrow f g α) S)
+
+  precomp-hom-arrow : hom-arrow (precomp g S) (precomp f S)
+  precomp-hom-arrow =
+    transpose-hom-arrow
+      ( precomp (map-codomain-hom-arrow f g α) S)
+      ( precomp (map-domain-hom-arrow f g α) S)
+      ( transpose-precomp-hom-arrow)
 ```
 
 ### Morphisms of arrows give morphisms of postcomposition arrows
@@ -338,12 +344,10 @@ module _
 
   postcomp-hom-arrow :
     {l : Level} (S : UU l) → hom-arrow (postcomp S f) (postcomp S g)
-  pr1 (postcomp-hom-arrow S) =
-    postcomp S (map-domain-hom-arrow f g α)
-  pr1 (pr2 (postcomp-hom-arrow S)) =
-    postcomp S (map-codomain-hom-arrow f g α)
-  pr2 (pr2 (postcomp-hom-arrow S)) h =
-    eq-htpy (coh-hom-arrow f g α ·r h)
+  postcomp-hom-arrow S =
+    ( postcomp S (map-domain-hom-arrow f g α) ,
+      postcomp S (map-codomain-hom-arrow f g α) ,
+      htpy-postcomp S (coh-hom-arrow f g α))
 ```
 
 ## See also
diff --git a/src/foundation/postcomposition-pullbacks.lagda.md b/src/foundation/postcomposition-pullbacks.lagda.md
index b24c28bb74..f5f0528db2 100644
--- a/src/foundation/postcomposition-pullbacks.lagda.md
+++ b/src/foundation/postcomposition-pullbacks.lagda.md
@@ -11,6 +11,7 @@ open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.identity-types
+open import foundation.postcomposition-functions
 open import foundation.standard-pullbacks
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
@@ -21,7 +22,6 @@ open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
-open import foundation-core.postcomposition-functions
 open import foundation-core.pullbacks
 open import foundation-core.universal-property-pullbacks
 ```
@@ -68,9 +68,10 @@ postcomp-cone :
   {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} (T : UU l5)
   (f : A → X) (g : B → X) (c : cone f g C) →
   cone (postcomp T f) (postcomp T g) (T → C)
-pr1 (postcomp-cone T f g c) h = vertical-map-cone f g c ∘ h
-pr1 (pr2 (postcomp-cone T f g c)) h = horizontal-map-cone f g c ∘ h
-pr2 (pr2 (postcomp-cone T f g c)) h = eq-htpy (coherence-square-cone f g c ·r h)
+postcomp-cone T f g c =
+  ( postcomp T (vertical-map-cone f g c) ,
+    postcomp T (horizontal-map-cone f g c) ,
+    htpy-postcomp T (coherence-square-cone f g c))
 ```
 
 ## Properties
@@ -121,38 +122,33 @@ triangle-map-standard-pullback-postcomp T f g c h =
 ### Pullbacks are closed under postcomposition exponentiation
 
 ```agda
-abstract
-  is-pullback-postcomp-is-pullback :
-    {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
-    (f : A → X) (g : B → X) (c : cone f g C) → is-pullback f g c →
-    (T : UU l5) →
-    is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c)
-  is-pullback-postcomp-is-pullback f g c is-pb-c T =
-    is-equiv-top-map-triangle
-      ( cone-map f g c)
-      ( map-standard-pullback-postcomp f g T)
-      ( gap (f ∘_) (g ∘_) (postcomp-cone T f g c))
-      ( triangle-map-standard-pullback-postcomp T f g c)
-      ( is-equiv-map-standard-pullback-postcomp f g T)
-      ( universal-property-pullback-is-pullback f g c is-pb-c T)
-
-abstract
-  is-pullback-is-pullback-postcomp :
-    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
-    (f : A → X) (g : B → X) (c : cone f g C) →
-    ( {l5 : Level} (T : UU l5) →
-      is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c)) →
-    is-pullback f g c
-  is-pullback-is-pullback-postcomp f g c is-pb-postcomp =
-    is-pullback-universal-property-pullback f g c
-      ( λ T →
-        is-equiv-left-map-triangle
-          ( cone-map f g c)
-          ( map-standard-pullback-postcomp f g T)
-          ( gap (f ∘_) (g ∘_) (postcomp-cone T f g c))
-          ( triangle-map-standard-pullback-postcomp T f g c)
-          ( is-pb-postcomp T)
-          ( is-equiv-map-standard-pullback-postcomp f g T))
+module _
+  {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
+  (f : A → X) (g : B → X) (c : cone f g C)
+  where
+
+  abstract
+    is-pullback-postcomp-is-pullback :
+      is-pullback f g c → (T : UU l5) →
+      is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c)
+    is-pullback-postcomp-is-pullback is-pb-c T =
+      is-equiv-top-map-triangle _ _ _
+        ( triangle-map-standard-pullback-postcomp T f g c)
+        ( is-equiv-map-standard-pullback-postcomp f g T)
+        ( universal-property-pullback-is-pullback f g c is-pb-c T)
+
+  abstract
+    is-pullback-is-pullback-postcomp :
+      ( {l5 : Level} (T : UU l5) →
+        is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c)) →
+      is-pullback f g c
+    is-pullback-is-pullback-postcomp is-pb-postcomp =
+      is-pullback-universal-property-pullback f g c
+        ( λ T →
+          is-equiv-left-map-triangle _ _ _
+            ( triangle-map-standard-pullback-postcomp T f g c)
+            ( is-pb-postcomp T)
+            ( is-equiv-map-standard-pullback-postcomp f g T))
 ```
 
 ### Cones satisfying the universal property of pullbacks are closed under postcomposition exponentiation
diff --git a/src/foundation/type-arithmetic-standard-pullbacks.lagda.md b/src/foundation/type-arithmetic-standard-pullbacks.lagda.md
index 09335074fa..73a755edc1 100644
--- a/src/foundation/type-arithmetic-standard-pullbacks.lagda.md
+++ b/src/foundation/type-arithmetic-standard-pullbacks.lagda.md
@@ -243,7 +243,9 @@ module _
 
 ### Unit laws for standard pullbacks
 
-Pulling back along the identity map
+Pulling back along the identity map is the identity operation.
+
+#### Left unit law for standard pullbacks
 
 ```agda
 module _
@@ -302,7 +304,7 @@ module _
 
 ### Unit laws for standard pullbacks
 
-Pulling back along the identity map is the identity operation.
+#### Right unit law for standard pullbacks
 
 ```agda
 module _
diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 959b2cb9b4..ffe775806e 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -58,11 +58,13 @@ open import synthetic-homotopy-theory.descent-property-pushouts public
 open import synthetic-homotopy-theory.descent-property-sequential-colimits public
 open import synthetic-homotopy-theory.double-loop-spaces public
 open import synthetic-homotopy-theory.eckmann-hilton-argument public
-open import synthetic-homotopy-theory.equifibered-sequential-diagrams public
+open import synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams public
+open import synthetic-homotopy-theory.equifibered-dependent-span-diagrams public
 open import synthetic-homotopy-theory.equivalences-cocones-under-equivalences-sequential-diagrams public
 open import synthetic-homotopy-theory.equivalences-coforks-under-equivalences-double-arrows public
 open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams public
 open import synthetic-homotopy-theory.equivalences-descent-data-pushouts public
+open import synthetic-homotopy-theory.equivalences-equifibered-dependent-span-diagrams public
 open import synthetic-homotopy-theory.equivalences-sequential-diagrams public
 open import synthetic-homotopy-theory.families-descent-data-pushouts public
 open import synthetic-homotopy-theory.families-descent-data-sequential-colimits public
@@ -91,6 +93,7 @@ open import synthetic-homotopy-theory.left-half-smash-products public
 open import synthetic-homotopy-theory.loop-homotopy-circle public
 open import synthetic-homotopy-theory.loop-spaces public
 open import synthetic-homotopy-theory.maps-of-prespectra public
+open import synthetic-homotopy-theory.mathers-second-cube-theorem public
 open import synthetic-homotopy-theory.mere-spheres public
 open import synthetic-homotopy-theory.morphisms-cocones-under-morphisms-sequential-diagrams public
 open import synthetic-homotopy-theory.morphisms-coforks-under-morphisms-double-arrows 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..6a9f85290f 100644
--- a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
@@ -26,7 +26,7 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import synthetic-homotopy-theory.dependent-sequential-diagrams
-open import synthetic-homotopy-theory.equifibered-sequential-diagrams
+open import synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams
 open import synthetic-homotopy-theory.sequential-diagrams
 ```
 
@@ -266,7 +266,7 @@ which gives us a collection of type families `Pₙ : Aₙ → 𝒰`, and a colle
 equivalences `Pₙ a ≃ Pₙ₊₁ (aₙ a)` induced by
 [transporting](foundation-core.transport-along-identifications.md) in `P` along
 `Hₙ`. This data comes together to form an
-[equifibered sequential diagram](synthetic-homotopy-theory.equifibered-sequential-diagrams.md)
+[equifibered sequential diagram](synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams.md)
 over `A`.
 
 ```agda
@@ -276,24 +276,24 @@ module _
   (P : X → UU l3)
   where
 
-  equifibered-sequential-diagram-family-cocone :
-    equifibered-sequential-diagram A l3
-  pr1 equifibered-sequential-diagram-family-cocone n a =
+  equifibered-dependent-sequential-diagram-family-cocone :
+    equifibered-dependent-sequential-diagram A l3
+  pr1 equifibered-dependent-sequential-diagram-family-cocone n a =
     P (map-cocone-sequential-diagram c n a)
-  pr2 equifibered-sequential-diagram-family-cocone n a =
+  pr2 equifibered-dependent-sequential-diagram-family-cocone n a =
     equiv-tr P (coherence-cocone-sequential-diagram c n a)
 
   dependent-sequential-diagram-family-cocone : dependent-sequential-diagram A l3
   dependent-sequential-diagram-family-cocone =
-    dependent-sequential-diagram-equifibered-sequential-diagram
-      ( equifibered-sequential-diagram-family-cocone)
+    dependent-sequential-diagram-equifibered-dependent-sequential-diagram
+      ( equifibered-dependent-sequential-diagram-family-cocone)
 
   is-equifibered-dependent-sequential-diagram-family-cocone :
     is-equifibered-dependent-sequential-diagram
       ( dependent-sequential-diagram-family-cocone)
   is-equifibered-dependent-sequential-diagram-family-cocone =
-    is-equifibered-dependent-sequential-diagram-equifibered-sequential-diagram
-      ( equifibered-sequential-diagram-family-cocone)
+    is-equifibered-dependent-sequential-diagram-equifibered-dependent-sequential-diagram
+      ( equifibered-dependent-sequential-diagram-family-cocone)
 ```
 
 ## 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
index 7095433e23..ebea5fa249 100644
--- 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
@@ -60,18 +60,19 @@ for [pushouts](synthetic-homotopy-theory.pushouts.md) `P ≈ (PA, PB, PS)` and
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : 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)
+  (P : family-with-descent-data-pushout c l5 l6 l7)
+  (R : family-with-descent-data-pushout c l8 l9 l10)
   where
 
-  family-cocone-equivalence-type-pushout : X → UU (l5 ⊔ l6)
+  family-cocone-equivalence-type-pushout : X → UU (l7 ⊔ l10)
   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)
+  descent-data-equivalence-type-pushout :
+    descent-data-pushout 𝒮 (l5 ⊔ l8) (l6 ⊔ l9)
   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
@@ -169,7 +170,7 @@ module _
     coherence-equiv-descent-data-equivalence-type-pushout
 
   family-with-descent-data-equivalence-type-pushout :
-    family-with-descent-data-pushout c (l5 ⊔ l6)
+    family-with-descent-data-pushout c (l5 ⊔ l8) (l6 ⊔ l9) (l7 ⊔ l10)
   pr1 family-with-descent-data-equivalence-type-pushout =
     family-cocone-equivalence-type-pushout
   pr1 (pr2 family-with-descent-data-equivalence-type-pushout) =
@@ -184,10 +185,10 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : 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)
+  (P : family-with-descent-data-pushout c l5 l6 l7)
+  (R : family-with-descent-data-pushout c l8 l9 l10)
   where
 
   equiv-section-descent-data-equivalence-type-pushout :
@@ -288,11 +289,11 @@ by inverting the inverted equivalences.
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : 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)
+  (P : family-with-descent-data-pushout c l5 l6 l7)
+  (R : family-with-descent-data-pushout c l8 l9 l10)
   (e :
     equiv-descent-data-pushout
       ( descent-data-family-with-descent-data-pushout P)
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
index 6cbec40faf..5bd1e7ae81 100644
--- 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
@@ -102,18 +102,19 @@ which we can massage into a coherence of the morphism as
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : 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)
+  (P : family-with-descent-data-pushout c l5 l6 l7)
+  (R : family-with-descent-data-pushout c l8 l9 l10)
   where
 
-  family-cocone-function-type-pushout : X → UU (l5 ⊔ l6)
+  family-cocone-function-type-pushout : X → UU (l7 ⊔ l10)
   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)
+  descent-data-function-type-pushout :
+    descent-data-pushout 𝒮 (l5 ⊔ l8) (l6 ⊔ l9)
   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
@@ -208,7 +209,7 @@ module _
     coherence-equiv-descent-data-function-type-pushout
 
   family-with-descent-data-function-type-pushout :
-    family-with-descent-data-pushout c (l5 ⊔ l6)
+    family-with-descent-data-pushout c (l5 ⊔ l8) (l6 ⊔ l9) (l7 ⊔ l10)
   pr1 family-with-descent-data-function-type-pushout =
     family-cocone-function-type-pushout
   pr1 (pr2 family-with-descent-data-function-type-pushout) =
@@ -223,10 +224,10 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : 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)
+  (P : family-with-descent-data-pushout c l5 l6 l7)
+  (R : family-with-descent-data-pushout c l8 l9 l10)
   where
 
   hom-section-descent-data-function-type-pushout :
@@ -250,8 +251,7 @@ module _
 
   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-hom-section-descent-data-function-type-pushout =
       is-equiv-tot-is-fiberwise-equiv
         ( λ tA →
@@ -326,11 +326,11 @@ by inverting the inverted equivalences.
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : 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)
+  (P : family-with-descent-data-pushout c l5 l6 l7)
+  (R : family-with-descent-data-pushout c l8 l9 l10)
   (m :
     hom-descent-data-pushout
       ( descent-data-family-with-descent-data-pushout P)
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
index 6244d587ce..89d5e10cc6 100644
--- 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
@@ -66,7 +66,7 @@ module _
   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
+  descent-data-identity-type-pushout : descent-data-pushout 𝒮 l4 l4
   pr1 descent-data-identity-type-pushout a =
     x₀ ＝ horizontal-map-cocone _ _ c a
   pr1 (pr2 descent-data-identity-type-pushout) b =
@@ -85,7 +85,7 @@ module _
     tr-Id-right (coherence-square-cocone _ _ c s)
 
   family-with-descent-data-identity-type-pushout :
-    family-with-descent-data-pushout c l4
+    family-with-descent-data-pushout c l4 l4 l4
   pr1 family-with-descent-data-identity-type-pushout =
     family-cocone-identity-type-pushout
   pr1 (pr2 family-with-descent-data-identity-type-pushout) =
diff --git a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
index 020d2dcefb..6047c03a40 100644
--- a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
@@ -7,6 +7,7 @@ module synthetic-homotopy-theory.descent-data-pushouts where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.function-types
@@ -69,11 +70,11 @@ module _
   {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3)
   where
 
-  descent-data-pushout : (l4 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4)
-  descent-data-pushout l =
-    Σ ( domain-span-diagram 𝒮 → UU l)
+  descent-data-pushout : (l4 l5 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4 ⊔ lsuc l5)
+  descent-data-pushout l4 l5 =
+    Σ ( domain-span-diagram 𝒮 → UU l4)
       ( λ PA →
-        Σ ( codomain-span-diagram 𝒮 → UU l)
+        Σ ( codomain-span-diagram 𝒮 → UU l5)
           ( λ PB →
             (s : spanning-type-span-diagram 𝒮) →
             PA (left-map-span-diagram 𝒮 s) ≃ PB (right-map-span-diagram 𝒮 s)))
@@ -83,14 +84,14 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
   where
 
   left-family-descent-data-pushout : domain-span-diagram 𝒮 → UU l4
   left-family-descent-data-pushout = pr1 P
 
-  right-family-descent-data-pushout : codomain-span-diagram 𝒮 → UU l4
+  right-family-descent-data-pushout : codomain-span-diagram 𝒮 → UU l5
   right-family-descent-data-pushout = pr1 (pr2 P)
 
   equiv-family-descent-data-pushout :
@@ -106,6 +107,13 @@ module _
   map-family-descent-data-pushout s =
     map-equiv (equiv-family-descent-data-pushout s)
 
+  map-inv-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)
+  map-inv-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)
@@ -140,11 +148,15 @@ module _
   where
 
   descent-data-family-cocone-span-diagram :
-    {l5 : Level} → (X → UU l5) → descent-data-pushout 𝒮 l5
-  pr1 (descent-data-family-cocone-span-diagram P) =
-    P ∘ horizontal-map-cocone _ _ c
-  pr1 (pr2 (descent-data-family-cocone-span-diagram P)) =
-    P ∘ vertical-map-cocone _ _ c
-  pr2 (pr2 (descent-data-family-cocone-span-diagram P)) s =
-    equiv-tr P (coherence-square-cocone _ _ c s)
+    {l5 : Level} → (X → UU l5) → descent-data-pushout 𝒮 l5 l5
+  descent-data-family-cocone-span-diagram P =
+    ( P ∘ horizontal-map-cocone _ _ c) ,
+    ( P ∘ vertical-map-cocone _ _ c) ,
+    ( equiv-tr P ∘ coherence-square-cocone _ _ c)
 ```
+
+## See also
+
+- [Equifibered dependent span diagrams](synthetic-homotopy-theory.equifibered-dependent-span-diagrams.md)
+  is a variant descent data for pushouts where an additional type family over
+  the middle vertex is specified.
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..4f840820b2 100644
--- a/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md
@@ -15,7 +15,7 @@ open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
 open import synthetic-homotopy-theory.dependent-sequential-diagrams
-open import synthetic-homotopy-theory.equifibered-sequential-diagrams
+open import synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams
 open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams
 open import synthetic-homotopy-theory.morphisms-dependent-sequential-diagrams
 open import synthetic-homotopy-theory.sequential-diagrams
@@ -32,7 +32,7 @@ Given a [sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md)
 The data required to construct a type family is called
 {{#concept "descent data" Disambiguation="sequential colimits" Agda=descent-data-sequential-colimit}}
 for sequential colimits, and it is exactly an
-[equifibered sequential diagram](synthetic-homotopy-theory.equifibered-sequential-diagrams.md).
+[equifibered sequential diagram](synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams.md).
 
 The fact that the type of descent data for a sequential diagram is equivalent to
 the type of type families over its colimit is recorded in
@@ -49,7 +49,7 @@ module _
 
   descent-data-sequential-colimit : (l2 : Level) → UU (l1 ⊔ lsuc l2)
   descent-data-sequential-colimit =
-    equifibered-sequential-diagram A
+    equifibered-dependent-sequential-diagram A
 ```
 
 ### Components of descent data for sequential colimits
@@ -89,7 +89,7 @@ module _
 
   dependent-sequential-diagram-descent-data : dependent-sequential-diagram A l2
   dependent-sequential-diagram-descent-data =
-    dependent-sequential-diagram-equifibered-sequential-diagram B
+    dependent-sequential-diagram-equifibered-dependent-sequential-diagram B
 ```
 
 ### Morphisms of descent data for sequential colimits
@@ -104,8 +104,8 @@ module _
   hom-descent-data-sequential-colimit : UU (l1 ⊔ l2 ⊔ l3)
   hom-descent-data-sequential-colimit =
     hom-dependent-sequential-diagram
-      ( dependent-sequential-diagram-equifibered-sequential-diagram B)
-      ( dependent-sequential-diagram-equifibered-sequential-diagram C)
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram B)
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C)
 ```
 
 ### Equivalences of descent data for sequential colimits
@@ -120,55 +120,58 @@ module _
   equiv-descent-data-sequential-colimit : UU (l1 ⊔ l2 ⊔ l3)
   equiv-descent-data-sequential-colimit =
     equiv-dependent-sequential-diagram
-      ( dependent-sequential-diagram-equifibered-sequential-diagram B)
-      ( dependent-sequential-diagram-equifibered-sequential-diagram C)
-
-  module _
-    (e : equiv-descent-data-sequential-colimit)
-    where
-
-    equiv-equiv-descent-data-sequential-colimit :
-      (n : ℕ) (a : family-sequential-diagram A n) →
-      family-descent-data-sequential-colimit B n a ≃
-      family-descent-data-sequential-colimit C n a
-    equiv-equiv-descent-data-sequential-colimit =
-      equiv-equiv-dependent-sequential-diagram
-        ( dependent-sequential-diagram-equifibered-sequential-diagram C)
-        ( e)
-
-    map-equiv-descent-data-sequential-colimit :
-      (n : ℕ) (a : family-sequential-diagram A n) →
-      family-descent-data-sequential-colimit B n a →
-      family-descent-data-sequential-colimit C n a
-    map-equiv-descent-data-sequential-colimit =
-      map-equiv-dependent-sequential-diagram
-        ( dependent-sequential-diagram-equifibered-sequential-diagram C)
-        ( e)
-
-    is-equiv-map-equiv-descent-data-sequential-colimit :
-      (n : ℕ) (a : family-sequential-diagram A n) →
-      is-equiv (map-equiv-descent-data-sequential-colimit n a)
-    is-equiv-map-equiv-descent-data-sequential-colimit =
-      is-equiv-map-equiv-dependent-sequential-diagram
-        ( dependent-sequential-diagram-equifibered-sequential-diagram C)
-        ( e)
-
-    coh-equiv-descent-data-sequential-colimit :
-      coherence-equiv-dependent-sequential-diagram
-        ( dependent-sequential-diagram-equifibered-sequential-diagram B)
-        ( dependent-sequential-diagram-equifibered-sequential-diagram C)
-        ( equiv-equiv-descent-data-sequential-colimit)
-    coh-equiv-descent-data-sequential-colimit =
-      coh-equiv-dependent-sequential-diagram
-        ( dependent-sequential-diagram-equifibered-sequential-diagram C)
-        ( e)
-
-    hom-equiv-descent-data-sequential-colimit :
-      hom-descent-data-sequential-colimit B C
-    hom-equiv-descent-data-sequential-colimit =
-      hom-equiv-dependent-sequential-diagram
-        ( dependent-sequential-diagram-equifibered-sequential-diagram C)
-        ( e)
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram B)
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C)
+
+module _
+  {l1 l2 l3 : Level} {A : sequential-diagram l1}
+  (B : descent-data-sequential-colimit A l2)
+  (C : descent-data-sequential-colimit A l3)
+  (e : equiv-descent-data-sequential-colimit B C)
+  where
+
+  equiv-equiv-descent-data-sequential-colimit :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    family-descent-data-sequential-colimit B n a ≃
+    family-descent-data-sequential-colimit C n a
+  equiv-equiv-descent-data-sequential-colimit =
+    equiv-equiv-dependent-sequential-diagram
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C)
+      ( e)
+
+  map-equiv-descent-data-sequential-colimit :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    family-descent-data-sequential-colimit B n a →
+    family-descent-data-sequential-colimit C n a
+  map-equiv-descent-data-sequential-colimit =
+    map-equiv-dependent-sequential-diagram
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C)
+      ( e)
+
+  is-equiv-map-equiv-descent-data-sequential-colimit :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    is-equiv (map-equiv-descent-data-sequential-colimit n a)
+  is-equiv-map-equiv-descent-data-sequential-colimit =
+    is-equiv-map-equiv-dependent-sequential-diagram
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C)
+      ( e)
+
+  coh-equiv-descent-data-sequential-colimit :
+    coherence-equiv-dependent-sequential-diagram
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram B)
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C)
+      ( equiv-equiv-descent-data-sequential-colimit)
+  coh-equiv-descent-data-sequential-colimit =
+    coh-equiv-dependent-sequential-diagram
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C)
+      ( e)
+
+  hom-equiv-descent-data-sequential-colimit :
+    hom-descent-data-sequential-colimit B C
+  hom-equiv-descent-data-sequential-colimit =
+    hom-equiv-dependent-sequential-diagram
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C)
+      ( e)
 
 module _
   {l1 l2 : Level} {A : sequential-diagram l1}
@@ -179,7 +182,7 @@ module _
     equiv-descent-data-sequential-colimit B B
   id-equiv-descent-data-sequential-colimit =
     id-equiv-dependent-sequential-diagram
-      ( dependent-sequential-diagram-equifibered-sequential-diagram B)
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram B)
 ```
 
 ### Descent data induced by families over cocones under sequential diagrams
@@ -193,5 +196,5 @@ module _
   descent-data-family-cocone-sequential-diagram :
     {l3 : Level} → (X → UU l3) → descent-data-sequential-colimit A l3
   descent-data-family-cocone-sequential-diagram =
-    equifibered-sequential-diagram-family-cocone c
+    equifibered-dependent-sequential-diagram-family-cocone c
 ```
diff --git a/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
index 6d1f56638f..5d8b09bc77 100644
--- a/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
@@ -120,18 +120,16 @@ module _
   equiv-descent-data-cocone-span-diagram-UU :
     (l4 : Level) →
     cocone-span-diagram 𝒮 (UU l4) ≃
-    descent-data-pushout 𝒮 l4
+    descent-data-pushout 𝒮 l4 l4
   equiv-descent-data-cocone-span-diagram-UU _ =
     equiv-tot
       ( λ PA →
-        equiv-tot
-          ( λ PB →
-            ( equiv-Π-equiv-family (λ s → equiv-univalence))))
+        equiv-tot (λ PB → (equiv-Π-equiv-family (λ s → equiv-univalence))))
 
   descent-data-cocone-span-diagram-UU :
     {l4 : Level} →
     cocone-span-diagram 𝒮 (UU l4) →
-    descent-data-pushout 𝒮 l4
+    descent-data-pushout 𝒮 l4 l4
   descent-data-cocone-span-diagram-UU {l4} =
     map-equiv (equiv-descent-data-cocone-span-diagram-UU l4)
 
@@ -176,7 +174,7 @@ 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 : descent-data-pushout 𝒮 l5)
+  (P : descent-data-pushout 𝒮 l5 l5)
   where
 
   abstract
@@ -293,7 +291,7 @@ module _
     map-equiv (compute-inv-right-family-cocone-descent-data-pushout b)
 
   family-with-descent-data-pushout-descent-data-pushout :
-    family-with-descent-data-pushout c l5
+    family-with-descent-data-pushout c l5 l5 l5
   pr1 family-with-descent-data-pushout-descent-data-pushout =
     family-cocone-descent-data-pushout
   pr1 (pr2 family-with-descent-data-pushout-descent-data-pushout) =
diff --git a/src/synthetic-homotopy-theory/equifibered-dependent-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/equifibered-dependent-sequential-diagrams.lagda.md
new file mode 100644
index 0000000000..f78b71f19d
--- /dev/null
+++ b/src/synthetic-homotopy-theory/equifibered-dependent-sequential-diagrams.lagda.md
@@ -0,0 +1,163 @@
+# Equifibered dependent sequential diagrams
+
+```agda
+module synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.dependent-sequential-diagrams
+open import synthetic-homotopy-theory.sequential-diagrams
+```
+
+</details>
+
+## Idea
+
+An
+{{#concept "equifibered dependent sequential diagram" Disambiguation="over a sequential diagram" Agda=equifibered-dependent-sequential-diagram}}
+over a [sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md)
+`(A, a)` consists of a type family `B : (n : ℕ) → Aₙ → 𝒰`
+[equipped](foundation.structure.md) with a family of fiberwise equivalences
+
+```text
+bₙ : (a : Aₙ) → Bₙ a ≃ Bₙ₊₁ (aₙ a) .
+```
+
+The term "equifibered" comes from the equivalent definition as
+[dependent sequential diagrams](synthetic-homotopy-theory.dependent-sequential-diagrams.md)
+over `(A, a)`
+
+```text
+     b₀      b₁      b₂
+ B₀ ---> B₁ ---> B₂ ---> ⋯
+ |       |       |
+ |       |       |
+ ↡       ↡       ↡
+ A₀ ---> A₁ ---> A₂ ---> ⋯ ,
+     a₀      a₁      a₂
+```
+
+which are said to be "fibered over `A`", whose maps `bₙ` are equivalences. This
+terminology was originally introduced by Charles Rezk in _Toposes and Homotopy
+Toposes_ {{#cite Rezk10HomotopyToposes}}.
+
+## Definitions
+
+### Equifibered dependent sequential diagrams
+
+```agda
+module _
+  {l1 : Level} (A : sequential-diagram l1)
+  where
+
+  equifibered-dependent-sequential-diagram : (l : Level) → UU (l1 ⊔ lsuc l)
+  equifibered-dependent-sequential-diagram l =
+    Σ ( (n : ℕ) → family-sequential-diagram A n → UU l)
+      ( λ B →
+        (n : ℕ) (a : family-sequential-diagram A n) →
+        B n a ≃ B (succ-ℕ n) (map-sequential-diagram A n a))
+```
+
+### Components of an equifibered dependent sequential diagram
+
+```agda
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  (B : equifibered-dependent-sequential-diagram A l2)
+  where
+
+  family-equifibered-dependent-sequential-diagram :
+    (n : ℕ) → family-sequential-diagram A n → UU l2
+  family-equifibered-dependent-sequential-diagram = pr1 B
+
+  equiv-equifibered-dependent-sequential-diagram :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    family-equifibered-dependent-sequential-diagram n a ≃
+    family-equifibered-dependent-sequential-diagram
+      ( succ-ℕ n)
+      ( map-sequential-diagram A n a)
+  equiv-equifibered-dependent-sequential-diagram = pr2 B
+
+  map-equifibered-dependent-sequential-diagram :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    family-equifibered-dependent-sequential-diagram n a →
+    family-equifibered-dependent-sequential-diagram
+      ( succ-ℕ n)
+      ( map-sequential-diagram A n a)
+  map-equifibered-dependent-sequential-diagram n a =
+    map-equiv (equiv-equifibered-dependent-sequential-diagram n a)
+
+  is-equiv-map-equifibered-dependent-sequential-diagram :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    is-equiv (map-equifibered-dependent-sequential-diagram n a)
+  is-equiv-map-equifibered-dependent-sequential-diagram n a =
+    is-equiv-map-equiv (equiv-equifibered-dependent-sequential-diagram n a)
+
+  dependent-sequential-diagram-equifibered-dependent-sequential-diagram :
+    dependent-sequential-diagram A l2
+  pr1 dependent-sequential-diagram-equifibered-dependent-sequential-diagram =
+    family-equifibered-dependent-sequential-diagram
+  pr2 dependent-sequential-diagram-equifibered-dependent-sequential-diagram =
+    map-equifibered-dependent-sequential-diagram
+```
+
+### The predicate on dependent sequential diagrams of being equifibered
+
+```agda
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  where
+
+  is-equifibered-dependent-sequential-diagram :
+    (B : dependent-sequential-diagram A l2) → UU (l1 ⊔ l2)
+  is-equifibered-dependent-sequential-diagram B =
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    is-equiv (map-dependent-sequential-diagram B n a)
+
+  is-equifibered-dependent-sequential-diagram-equifibered-dependent-sequential-diagram :
+    (B : equifibered-dependent-sequential-diagram A l2) →
+    is-equifibered-dependent-sequential-diagram
+      ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram B)
+  is-equifibered-dependent-sequential-diagram-equifibered-dependent-sequential-diagram
+    B =
+    is-equiv-map-equifibered-dependent-sequential-diagram B
+```
+
+## Properties
+
+### Dependent sequential diagrams which are equifibered are equifibered dependent sequential diagrams
+
+To construct an equifibered dependent sequential diagram over `A`, it suffices
+to construct a dependent sequential diagram `(B, b)` over `A`, and show that the
+maps `bₙ` are equivalences.
+
+```agda
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  (B : dependent-sequential-diagram A l2)
+  where
+
+  equifibered-dependent-sequential-diagram-dependent-sequential-diagram :
+    is-equifibered-dependent-sequential-diagram B →
+    equifibered-dependent-sequential-diagram A l2
+  pr1
+    ( equifibered-dependent-sequential-diagram-dependent-sequential-diagram _) =
+    family-dependent-sequential-diagram B
+  pr2
+    ( equifibered-dependent-sequential-diagram-dependent-sequential-diagram
+      is-equiv-map)
+    n a =
+    ( map-dependent-sequential-diagram B n a , is-equiv-map n a)
+```
+
+## References
+
+{{#bibliography}}
diff --git a/src/synthetic-homotopy-theory/equifibered-dependent-span-diagrams.lagda.md b/src/synthetic-homotopy-theory/equifibered-dependent-span-diagrams.lagda.md
new file mode 100644
index 0000000000..3d09b49b01
--- /dev/null
+++ b/src/synthetic-homotopy-theory/equifibered-dependent-span-diagrams.lagda.md
@@ -0,0 +1,231 @@
+# Equifibered dependent span diagrams
+
+```agda
+module synthetic-homotopy-theory.equifibered-dependent-span-diagrams where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-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
+```
+
+</details>
+
+## Idea
+
+Given a [span diagram](foundation.span-diagrams.md) `𝒮` of the form
+
+```text
+      f       g
+  A <---- S ----> B,
+```
+
+a
+{{#concept "equifibered dependent span diagram" Disambiguation="over a span diagram" Agda=equifibered-dependent-span-diagram}}
+is a triple of type families `PA`, `PB`, `PS` over the vertices of `𝒮`,
+
+```text
+  𝒰       𝒱       𝒲
+  ↑       ↑       ↑
+  A <---- S ----> B,
+```
+
+together with families of equivalences `PS s ≃ PA (f s)` and `PS s ≃ PB (g s)`
+for every `s : S`.
+
+The [identity type](foundation-core.identity-types.md) of equifibered dependent
+span diagrams is characterized in
+[`equivalences-equifibered-dependent-span-diagrams`](synthetic-homotopy-theory.equivalences-equifibered-dependent-span-diagrams.md).
+
+## Definitions
+
+### Equifibered dependent span diagrams
+
+```agda
+module _
+  {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3)
+  where
+
+  equifibered-dependent-span-diagram :
+    (l4 l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4 ⊔ lsuc l5 ⊔ lsuc l6)
+  equifibered-dependent-span-diagram l4 l5 l6 =
+    Σ ( domain-span-diagram 𝒮 → UU l4)
+      ( λ PA →
+        Σ ( codomain-span-diagram 𝒮 → UU l5)
+          ( λ PB →
+            Σ ( spanning-type-span-diagram 𝒮 → UU l6)
+              ( λ PS →
+                ( (s : spanning-type-span-diagram 𝒮) →
+                  PS s ≃ PA (left-map-span-diagram 𝒮 s)) ×
+                ( (s : spanning-type-span-diagram 𝒮) →
+                  PS s ≃ PB (right-map-span-diagram 𝒮 s)))))
+```
+
+### Components of equifibered dependent span diagrams
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : equifibered-dependent-span-diagram 𝒮 l4 l5 l6)
+  where
+
+  left-family-equifibered-dependent-span-diagram :
+    domain-span-diagram 𝒮 → UU l4
+  left-family-equifibered-dependent-span-diagram =
+    pr1 P
+
+  right-family-equifibered-dependent-span-diagram :
+    codomain-span-diagram 𝒮 → UU l5
+  right-family-equifibered-dependent-span-diagram =
+    pr1 (pr2 P)
+
+  spanning-type-family-equifibered-dependent-span-diagram :
+    spanning-type-span-diagram 𝒮 → UU l6
+  spanning-type-family-equifibered-dependent-span-diagram =
+    pr1 (pr2 (pr2 P))
+
+  equiv-left-family-equifibered-dependent-span-diagram :
+    (s : spanning-type-span-diagram 𝒮) →
+    spanning-type-family-equifibered-dependent-span-diagram s ≃
+    left-family-equifibered-dependent-span-diagram (left-map-span-diagram 𝒮 s)
+  equiv-left-family-equifibered-dependent-span-diagram =
+    pr1 (pr2 (pr2 (pr2 P)))
+
+  equiv-right-family-equifibered-dependent-span-diagram :
+    (s : spanning-type-span-diagram 𝒮) →
+    spanning-type-family-equifibered-dependent-span-diagram s ≃
+    right-family-equifibered-dependent-span-diagram (right-map-span-diagram 𝒮 s)
+  equiv-right-family-equifibered-dependent-span-diagram =
+    pr2 (pr2 (pr2 (pr2 P)))
+
+  map-left-family-equifibered-dependent-span-diagram :
+    (s : spanning-type-span-diagram 𝒮) →
+    spanning-type-family-equifibered-dependent-span-diagram s →
+    left-family-equifibered-dependent-span-diagram (left-map-span-diagram 𝒮 s)
+  map-left-family-equifibered-dependent-span-diagram =
+    map-equiv ∘ equiv-left-family-equifibered-dependent-span-diagram
+
+  map-right-family-equifibered-dependent-span-diagram :
+    (s : spanning-type-span-diagram 𝒮) →
+    spanning-type-family-equifibered-dependent-span-diagram s →
+    right-family-equifibered-dependent-span-diagram (right-map-span-diagram 𝒮 s)
+  map-right-family-equifibered-dependent-span-diagram =
+    map-equiv ∘ equiv-right-family-equifibered-dependent-span-diagram
+
+  map-inv-left-family-equifibered-dependent-span-diagram :
+    (s : spanning-type-span-diagram 𝒮) →
+    left-family-equifibered-dependent-span-diagram (left-map-span-diagram 𝒮 s) →
+    spanning-type-family-equifibered-dependent-span-diagram s
+  map-inv-left-family-equifibered-dependent-span-diagram =
+    map-inv-equiv ∘ equiv-left-family-equifibered-dependent-span-diagram
+
+  map-inv-right-family-equifibered-dependent-span-diagram :
+    (s : spanning-type-span-diagram 𝒮) →
+    right-family-equifibered-dependent-span-diagram
+      ( right-map-span-diagram 𝒮 s) →
+    spanning-type-family-equifibered-dependent-span-diagram s
+  map-inv-right-family-equifibered-dependent-span-diagram =
+    map-inv-equiv ∘ equiv-right-family-equifibered-dependent-span-diagram
+
+  is-equiv-map-left-family-equifibered-dependent-span-diagram :
+    (s : spanning-type-span-diagram 𝒮) →
+    is-equiv (map-left-family-equifibered-dependent-span-diagram s)
+  is-equiv-map-left-family-equifibered-dependent-span-diagram s =
+    is-equiv-map-equiv (equiv-left-family-equifibered-dependent-span-diagram s)
+
+  is-equiv-map-right-family-equifibered-dependent-span-diagram :
+    (s : spanning-type-span-diagram 𝒮) →
+    is-equiv (map-right-family-equifibered-dependent-span-diagram s)
+  is-equiv-map-right-family-equifibered-dependent-span-diagram s =
+    is-equiv-map-equiv (equiv-right-family-equifibered-dependent-span-diagram s)
+
+  equiv-left-right-family-equifibered-dependent-span-diagram :
+    (s : spanning-type-span-diagram 𝒮) →
+    left-family-equifibered-dependent-span-diagram (left-map-span-diagram 𝒮 s) ≃
+    right-family-equifibered-dependent-span-diagram (right-map-span-diagram 𝒮 s)
+  equiv-left-right-family-equifibered-dependent-span-diagram s =
+    equiv-right-family-equifibered-dependent-span-diagram s ∘e
+    inv-equiv (equiv-left-family-equifibered-dependent-span-diagram s)
+
+  map-left-right-family-equifibered-dependent-span-diagram :
+    (s : spanning-type-span-diagram 𝒮) →
+    left-family-equifibered-dependent-span-diagram (left-map-span-diagram 𝒮 s) →
+    right-family-equifibered-dependent-span-diagram (right-map-span-diagram 𝒮 s)
+  map-left-right-family-equifibered-dependent-span-diagram =
+    map-equiv ∘ equiv-left-right-family-equifibered-dependent-span-diagram
+
+  equiv-right-left-family-equifibered-dependent-span-diagram :
+    (s : spanning-type-span-diagram 𝒮) →
+    right-family-equifibered-dependent-span-diagram
+      ( right-map-span-diagram 𝒮 s) ≃
+    left-family-equifibered-dependent-span-diagram
+      ( left-map-span-diagram 𝒮 s)
+  equiv-right-left-family-equifibered-dependent-span-diagram s =
+    equiv-left-family-equifibered-dependent-span-diagram s ∘e
+    inv-equiv (equiv-right-family-equifibered-dependent-span-diagram s)
+
+  map-right-left-family-equifibered-dependent-span-diagram :
+    (s : spanning-type-span-diagram 𝒮) →
+    right-family-equifibered-dependent-span-diagram
+      ( right-map-span-diagram 𝒮 s) →
+    left-family-equifibered-dependent-span-diagram
+      ( left-map-span-diagram 𝒮 s)
+  map-right-left-family-equifibered-dependent-span-diagram =
+    map-equiv ∘ equiv-right-left-family-equifibered-dependent-span-diagram
+
+  descent-data-pushout-equifibered-dependent-span-diagram :
+    descent-data-pushout 𝒮 l4 l5
+  descent-data-pushout-equifibered-dependent-span-diagram =
+    ( left-family-equifibered-dependent-span-diagram ,
+      right-family-equifibered-dependent-span-diagram ,
+      equiv-left-right-family-equifibered-dependent-span-diagram)
+```
+
+### Equifibered dependent span diagrams induced by descent data for pushouts
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
+  where
+
+  equifibered-dependent-span-diagram-descent-data-pushout :
+    equifibered-dependent-span-diagram 𝒮 l4 l5 l4
+  equifibered-dependent-span-diagram-descent-data-pushout =
+    ( left-family-descent-data-pushout P) ,
+    ( right-family-descent-data-pushout P) ,
+    ( left-family-descent-data-pushout P ∘ left-map-span-diagram 𝒮) ,
+    ( λ _ → id-equiv) ,
+    ( equiv-family-descent-data-pushout P)
+```
+
+### Equifibered dependent span diagrams induced by families over cocones
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {X : UU l4} (c : cocone-span-diagram 𝒮 X)
+  where
+
+  equifibered-dependent-span-diagram-family-cocone-span-diagram :
+    {l5 : Level} → (X → UU l5) → equifibered-dependent-span-diagram 𝒮 l5 l5 l5
+  equifibered-dependent-span-diagram-family-cocone-span-diagram P =
+    equifibered-dependent-span-diagram-descent-data-pushout
+      ( descent-data-family-cocone-span-diagram c P)
+```
+
+## See also
+
+- [Descent data for pushouts](synthetic-homotopy-theory.descent-data-pushouts.md)
+  is a variant of equifibered dependent span diagrams where a type family over
+  the middle vertex is not specified.
diff --git a/src/synthetic-homotopy-theory/equifibered-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/equifibered-sequential-diagrams.lagda.md
deleted file mode 100644
index 07cb2a030f..0000000000
--- a/src/synthetic-homotopy-theory/equifibered-sequential-diagrams.lagda.md
+++ /dev/null
@@ -1,153 +0,0 @@
-# Equifibered sequential diagrams
-
-```agda
-module synthetic-homotopy-theory.equifibered-sequential-diagrams where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import elementary-number-theory.natural-numbers
-
-open import foundation.dependent-pair-types
-open import foundation.equivalences
-open import foundation.universe-levels
-
-open import synthetic-homotopy-theory.dependent-sequential-diagrams
-open import synthetic-homotopy-theory.sequential-diagrams
-```
-
-</details>
-
-## Idea
-
-An
-{{#concept "equifibered sequential diagram" Disambiguation="over a sequential diagram" Agda=equifibered-sequential-diagram}}
-over a [sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md)
-`(A, a)` consists of a type family `B : (n : ℕ) → Aₙ → 𝒰`
-[equipped](foundation.structure.md) with a family of fiberwise equivalences
-
-```text
-bₙ : (a : Aₙ) → Bₙ a ≃ Bₙ₊₁ (aₙ a) .
-```
-
-The term "equifibered" comes from the equivalent definition as
-[dependent sequential diagrams](synthetic-homotopy-theory.dependent-sequential-diagrams.md)
-over `(A, a)`
-
-```text
-     b₀      b₁      b₂
- B₀ ---> B₁ ---> B₂ ---> ⋯
- |       |       |
- |       |       |
- ↡       ↡       ↡
- A₀ ---> A₁ ---> A₂ ---> ⋯ ,
-     a₀      a₁      a₂
-```
-
-which are said to be "fibered over `A`", whose maps `bₙ` are equivalences.
-
-## Definitions
-
-### Equifibered sequential diagrams
-
-```agda
-module _
-  {l1 : Level} (A : sequential-diagram l1)
-  where
-
-  equifibered-sequential-diagram : (l : Level) → UU (l1 ⊔ lsuc l)
-  equifibered-sequential-diagram l =
-    Σ ( (n : ℕ) → family-sequential-diagram A n → UU l)
-      ( λ B →
-        (n : ℕ) (a : family-sequential-diagram A n) →
-        B n a ≃ B (succ-ℕ n) (map-sequential-diagram A n a))
-```
-
-### Components of an equifibered sequential diagram
-
-```agda
-module _
-  {l1 l2 : Level} {A : sequential-diagram l1}
-  (B : equifibered-sequential-diagram A l2)
-  where
-
-  family-equifibered-sequential-diagram :
-    (n : ℕ) → family-sequential-diagram A n → UU l2
-  family-equifibered-sequential-diagram = pr1 B
-
-  equiv-equifibered-sequential-diagram :
-    (n : ℕ) (a : family-sequential-diagram A n) →
-    family-equifibered-sequential-diagram n a ≃
-    family-equifibered-sequential-diagram
-      ( succ-ℕ n)
-      ( map-sequential-diagram A n a)
-  equiv-equifibered-sequential-diagram = pr2 B
-
-  map-equifibered-sequential-diagram :
-    (n : ℕ) (a : family-sequential-diagram A n) →
-    family-equifibered-sequential-diagram n a →
-    family-equifibered-sequential-diagram
-      ( succ-ℕ n)
-      ( map-sequential-diagram A n a)
-  map-equifibered-sequential-diagram n a =
-    map-equiv (equiv-equifibered-sequential-diagram n a)
-
-  is-equiv-map-equifibered-sequential-diagram :
-    (n : ℕ) (a : family-sequential-diagram A n) →
-    is-equiv (map-equifibered-sequential-diagram n a)
-  is-equiv-map-equifibered-sequential-diagram n a =
-    is-equiv-map-equiv (equiv-equifibered-sequential-diagram n a)
-
-  dependent-sequential-diagram-equifibered-sequential-diagram :
-    dependent-sequential-diagram A l2
-  pr1 dependent-sequential-diagram-equifibered-sequential-diagram =
-    family-equifibered-sequential-diagram
-  pr2 dependent-sequential-diagram-equifibered-sequential-diagram =
-    map-equifibered-sequential-diagram
-```
-
-### The predicate on dependent sequential diagrams of being equifibered
-
-```agda
-module _
-  {l1 l2 : Level} {A : sequential-diagram l1}
-  where
-
-  is-equifibered-dependent-sequential-diagram :
-    (B : dependent-sequential-diagram A l2) → UU (l1 ⊔ l2)
-  is-equifibered-dependent-sequential-diagram B =
-    (n : ℕ) (a : family-sequential-diagram A n) →
-    is-equiv (map-dependent-sequential-diagram B n a)
-
-  is-equifibered-dependent-sequential-diagram-equifibered-sequential-diagram :
-    (B : equifibered-sequential-diagram A l2) →
-    is-equifibered-dependent-sequential-diagram
-      ( dependent-sequential-diagram-equifibered-sequential-diagram B)
-  is-equifibered-dependent-sequential-diagram-equifibered-sequential-diagram B =
-    is-equiv-map-equifibered-sequential-diagram B
-```
-
-## Properties
-
-### Dependent sequential diagrams which are equifibered are equifibered sequential diagrams
-
-To construct an equifibered sequential diagram over `A`, it suffices to
-construct a dependent sequential diagram `(B, b)` over `A`, and show that the
-maps `bₙ` are equivalences.
-
-```agda
-module _
-  {l1 l2 : Level} {A : sequential-diagram l1}
-  (B : dependent-sequential-diagram A l2)
-  where
-
-  equifibered-sequential-diagram-dependent-sequential-diagram :
-    is-equifibered-dependent-sequential-diagram B →
-    equifibered-sequential-diagram A l2
-  pr1 (equifibered-sequential-diagram-dependent-sequential-diagram _) =
-    family-dependent-sequential-diagram B
-  pr2 (equifibered-sequential-diagram-dependent-sequential-diagram is-equiv-map)
-    n a =
-    (map-dependent-sequential-diagram B n a , is-equiv-map n a)
-```
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 a95a4a12a1..fdcf6529d8 100644
--- a/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
@@ -7,6 +7,7 @@ module synthetic-homotopy-theory.equivalences-descent-data-pushouts where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.cartesian-product-types
 open import foundation.commuting-squares-of-maps
 open import foundation.dependent-pair-types
 open import foundation.equality-dependent-function-types
@@ -76,12 +77,13 @@ the proofs of `is-equiv` of their gluing maps.
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
-  (Q : descent-data-pushout 𝒮 l5)
+  {l1 l2 l3 l4 l5 l6 l7 : Level}
+  {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
+  (Q : descent-data-pushout 𝒮 l6 l7)
   where
 
-  equiv-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
+  equiv-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7)
   equiv-descent-data-pushout =
     Σ ( (a : domain-span-diagram 𝒮) →
         left-family-descent-data-pushout P a ≃
@@ -164,20 +166,18 @@ module _
     coherence-equiv-descent-data-pushout = pr2 (pr2 e)
 
     hom-equiv-descent-data-pushout : hom-descent-data-pushout P Q
-    pr1 hom-equiv-descent-data-pushout =
-      left-map-equiv-descent-data-pushout
-    pr1 (pr2 hom-equiv-descent-data-pushout) =
-      right-map-equiv-descent-data-pushout
-    pr2 (pr2 hom-equiv-descent-data-pushout) =
-      coherence-equiv-descent-data-pushout
+    hom-equiv-descent-data-pushout =
+      ( left-map-equiv-descent-data-pushout ,
+        right-map-equiv-descent-data-pushout ,
+        coherence-equiv-descent-data-pushout)
 ```
 
 ### The identity equivalence of descent data for pushouts
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
   where
 
   id-equiv-descent-data-pushout : equiv-descent-data-pushout P P
@@ -211,9 +211,9 @@ and mirroring the coherence squares vertically to get
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
-  (Q : descent-data-pushout 𝒮 l5)
+  {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
+  (Q : descent-data-pushout 𝒮 l6 l7)
   where
 
   inv-equiv-descent-data-pushout :
@@ -236,13 +236,14 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
-  (Q : descent-data-pushout 𝒮 l5)
+  {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
+  (Q : descent-data-pushout 𝒮 l6 l7)
   where
 
   htpy-equiv-descent-data-pushout :
-    (e f : equiv-descent-data-pushout P Q) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
+    (e f : equiv-descent-data-pushout P Q) →
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7)
   htpy-equiv-descent-data-pushout e f =
     htpy-hom-descent-data-pushout P Q
       ( hom-equiv-descent-data-pushout P Q e)
@@ -255,18 +256,18 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
   where
 
   equiv-eq-descent-data-pushout :
-    (Q : descent-data-pushout 𝒮 l4) →
+    (Q : descent-data-pushout 𝒮 l4 l5) →
     P ＝ Q → equiv-descent-data-pushout P Q
   equiv-eq-descent-data-pushout .P refl = id-equiv-descent-data-pushout P
 
   abstract
     is-torsorial-equiv-descent-data-pushout :
-      is-torsorial (equiv-descent-data-pushout {l5 = l4} P)
+      is-torsorial (equiv-descent-data-pushout {l6 = l4} {l7 = l5} P)
     is-torsorial-equiv-descent-data-pushout =
       is-torsorial-Eq-structure
         ( is-torsorial-Eq-Π
@@ -281,7 +282,7 @@ module _
               is-torsorial-htpy-equiv (equiv-family-descent-data-pushout P s))))
 
     is-equiv-equiv-eq-descent-data-pushout :
-      (Q : descent-data-pushout 𝒮 l4) →
+      (Q : descent-data-pushout 𝒮 l4 l5) →
       is-equiv (equiv-eq-descent-data-pushout Q)
     is-equiv-equiv-eq-descent-data-pushout =
       fundamental-theorem-id
@@ -289,7 +290,7 @@ module _
         ( equiv-eq-descent-data-pushout)
 
   extensionality-descent-data-pushout :
-    (Q : descent-data-pushout 𝒮 l4) →
+    (Q : descent-data-pushout 𝒮 l4 l5) →
     (P ＝ Q) ≃ equiv-descent-data-pushout P Q
   pr1 (extensionality-descent-data-pushout Q) =
     equiv-eq-descent-data-pushout Q
@@ -297,7 +298,7 @@ module _
     is-equiv-equiv-eq-descent-data-pushout Q
 
   eq-equiv-descent-data-pushout :
-    (Q : descent-data-pushout 𝒮 l4) →
+    (Q : descent-data-pushout 𝒮 l4 l5) →
     equiv-descent-data-pushout P Q → P ＝ Q
   eq-equiv-descent-data-pushout Q =
     map-inv-equiv (extensionality-descent-data-pushout Q)
@@ -307,9 +308,9 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  {P : descent-data-pushout 𝒮 l4}
-  {Q : descent-data-pushout 𝒮 l5}
+  {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {P : descent-data-pushout 𝒮 l4 l5}
+  {Q : descent-data-pushout 𝒮 l6 l7}
   (e : equiv-descent-data-pushout P Q)
   where
 
diff --git a/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md b/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md
new file mode 100644
index 0000000000..a14d92f545
--- /dev/null
+++ b/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md
@@ -0,0 +1,263 @@
+# Equivalences of equifibered dependent span diagrams
+
+```agda
+module synthetic-homotopy-theory.equivalences-equifibered-dependent-span-diagrams where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-function-types
+open import foundation.equivalence-extensionality
+open import foundation.equivalences
+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.univalence
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.equifibered-dependent-span-diagrams
+```
+
+</details>
+
+## Idea
+
+An
+{{#concept "equivalence" Disambiguation="of equifibered dependent span diagrams" Agda=equiv-equifibered-dependent-span-diagram}}
+of two
+[equifibered dependent span diagrams](synthetic-homotopy-theory.equifibered-dependent-span-diagrams.md)
+is a coherent system of equivalences of families over the base
+[span diagram](foundation.span-diagrams.md).
+
+## Definitions
+
+### Equivalences of equifibered dependent span diagrams
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level}
+  {𝒮 : span-diagram l1 l2 l3}
+  (P : equifibered-dependent-span-diagram 𝒮 l4 l5 l6)
+  (Q : equifibered-dependent-span-diagram 𝒮 l7 l8 l9)
+  where
+
+  equiv-equifibered-dependent-span-diagram :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7 ⊔ l8 ⊔ l9)
+  equiv-equifibered-dependent-span-diagram =
+    Σ ( (a : domain-span-diagram 𝒮) →
+        left-family-equifibered-dependent-span-diagram P a ≃
+        left-family-equifibered-dependent-span-diagram Q a)
+      ( λ eA →
+        Σ ( (b : codomain-span-diagram 𝒮) →
+            right-family-equifibered-dependent-span-diagram P b ≃
+            right-family-equifibered-dependent-span-diagram Q b)
+          ( λ eB →
+            Σ ( (s : spanning-type-span-diagram 𝒮) →
+                spanning-type-family-equifibered-dependent-span-diagram P s ≃
+                spanning-type-family-equifibered-dependent-span-diagram Q s)
+              ( λ eS →
+                ( (s : spanning-type-span-diagram 𝒮) →
+                  coherence-square-maps
+                    ( map-equiv (eS s))
+                    ( map-left-family-equifibered-dependent-span-diagram P s)
+                    ( map-left-family-equifibered-dependent-span-diagram Q s)
+                    ( map-equiv (eA (left-map-span-diagram 𝒮 s)))) ×
+                ( (s : spanning-type-span-diagram 𝒮) →
+                  coherence-square-maps
+                    ( map-equiv (eS s))
+                    ( map-right-family-equifibered-dependent-span-diagram P s)
+                    ( map-right-family-equifibered-dependent-span-diagram Q s)
+                    ( map-equiv (eB (right-map-span-diagram 𝒮 s)))))))
+
+  module _
+    (e : equiv-equifibered-dependent-span-diagram)
+    where
+
+    left-equiv-equiv-equifibered-dependent-span-diagram :
+      (a : domain-span-diagram 𝒮) →
+      left-family-equifibered-dependent-span-diagram P a ≃
+      left-family-equifibered-dependent-span-diagram Q a
+    left-equiv-equiv-equifibered-dependent-span-diagram = pr1 e
+
+    left-map-equiv-equifibered-dependent-span-diagram :
+      (a : domain-span-diagram 𝒮) →
+      left-family-equifibered-dependent-span-diagram P a →
+      left-family-equifibered-dependent-span-diagram Q a
+    left-map-equiv-equifibered-dependent-span-diagram a =
+      map-equiv (left-equiv-equiv-equifibered-dependent-span-diagram a)
+
+    is-equiv-left-map-equiv-equifibered-dependent-span-diagram :
+      (a : domain-span-diagram 𝒮) →
+      is-equiv (left-map-equiv-equifibered-dependent-span-diagram a)
+    is-equiv-left-map-equiv-equifibered-dependent-span-diagram a =
+      is-equiv-map-equiv (left-equiv-equiv-equifibered-dependent-span-diagram a)
+
+    inv-left-map-equiv-equifibered-dependent-span-diagram :
+      (a : domain-span-diagram 𝒮) →
+      left-family-equifibered-dependent-span-diagram Q a →
+      left-family-equifibered-dependent-span-diagram P a
+    inv-left-map-equiv-equifibered-dependent-span-diagram a =
+      map-inv-equiv (left-equiv-equiv-equifibered-dependent-span-diagram a)
+
+    right-equiv-equiv-equifibered-dependent-span-diagram :
+      (b : codomain-span-diagram 𝒮) →
+      right-family-equifibered-dependent-span-diagram P b ≃
+      right-family-equifibered-dependent-span-diagram Q b
+    right-equiv-equiv-equifibered-dependent-span-diagram = pr1 (pr2 e)
+
+    right-map-equiv-equifibered-dependent-span-diagram :
+      (b : codomain-span-diagram 𝒮) →
+      right-family-equifibered-dependent-span-diagram P b →
+      right-family-equifibered-dependent-span-diagram Q b
+    right-map-equiv-equifibered-dependent-span-diagram b =
+      map-equiv (right-equiv-equiv-equifibered-dependent-span-diagram b)
+
+    is-equiv-right-map-equiv-equifibered-dependent-span-diagram :
+      (b : codomain-span-diagram 𝒮) →
+      is-equiv (right-map-equiv-equifibered-dependent-span-diagram b)
+    is-equiv-right-map-equiv-equifibered-dependent-span-diagram b =
+      is-equiv-map-equiv
+        ( right-equiv-equiv-equifibered-dependent-span-diagram b)
+
+    inv-right-map-equiv-equifibered-dependent-span-diagram :
+      (b : codomain-span-diagram 𝒮) →
+      right-family-equifibered-dependent-span-diagram Q b →
+      right-family-equifibered-dependent-span-diagram P b
+    inv-right-map-equiv-equifibered-dependent-span-diagram b =
+      map-inv-equiv (right-equiv-equiv-equifibered-dependent-span-diagram b)
+
+    spanning-type-equiv-equiv-equifibered-dependent-span-diagram :
+      (b : spanning-type-span-diagram 𝒮) →
+      spanning-type-family-equifibered-dependent-span-diagram P b ≃
+      spanning-type-family-equifibered-dependent-span-diagram Q b
+    spanning-type-equiv-equiv-equifibered-dependent-span-diagram =
+      pr1 (pr2 (pr2 e))
+
+    spanning-type-map-equiv-equifibered-dependent-span-diagram :
+      (b : spanning-type-span-diagram 𝒮) →
+      spanning-type-family-equifibered-dependent-span-diagram P b →
+      spanning-type-family-equifibered-dependent-span-diagram Q b
+    spanning-type-map-equiv-equifibered-dependent-span-diagram b =
+      map-equiv (spanning-type-equiv-equiv-equifibered-dependent-span-diagram b)
+
+    is-equiv-spanning-type-map-equiv-equifibered-dependent-span-diagram :
+      (b : spanning-type-span-diagram 𝒮) →
+      is-equiv (spanning-type-map-equiv-equifibered-dependent-span-diagram b)
+    is-equiv-spanning-type-map-equiv-equifibered-dependent-span-diagram b =
+      is-equiv-map-equiv
+        ( spanning-type-equiv-equiv-equifibered-dependent-span-diagram b)
+
+    inv-spanning-type-map-equiv-equifibered-dependent-span-diagram :
+      (b : spanning-type-span-diagram 𝒮) →
+      spanning-type-family-equifibered-dependent-span-diagram Q b →
+      spanning-type-family-equifibered-dependent-span-diagram P b
+    inv-spanning-type-map-equiv-equifibered-dependent-span-diagram b =
+      map-inv-equiv
+        ( spanning-type-equiv-equiv-equifibered-dependent-span-diagram b)
+
+    coherence-left-equiv-equifibered-dependent-span-diagram :
+      (s : spanning-type-span-diagram 𝒮) →
+      coherence-square-maps
+        ( spanning-type-map-equiv-equifibered-dependent-span-diagram s)
+        ( map-left-family-equifibered-dependent-span-diagram P s)
+        ( map-left-family-equifibered-dependent-span-diagram Q s)
+        ( left-map-equiv-equifibered-dependent-span-diagram
+          ( left-map-span-diagram 𝒮 s))
+    coherence-left-equiv-equifibered-dependent-span-diagram =
+      pr1 (pr2 (pr2 (pr2 e)))
+
+    coherence-right-equiv-equifibered-dependent-span-diagram :
+      (s : spanning-type-span-diagram 𝒮) →
+      coherence-square-maps
+        ( spanning-type-map-equiv-equifibered-dependent-span-diagram s)
+        ( map-right-family-equifibered-dependent-span-diagram P s)
+        ( map-right-family-equifibered-dependent-span-diagram Q s)
+        ( right-map-equiv-equifibered-dependent-span-diagram
+          ( right-map-span-diagram 𝒮 s))
+    coherence-right-equiv-equifibered-dependent-span-diagram =
+      pr2 (pr2 (pr2 (pr2 e)))
+
+    coherence-left-right-equiv-equifibered-dependent-span-diagram :
+      (s : spanning-type-span-diagram 𝒮) →
+      coherence-square-maps
+        ( left-map-equiv-equifibered-dependent-span-diagram
+          ( left-map-span-diagram 𝒮 s))
+        ( map-left-right-family-equifibered-dependent-span-diagram P s)
+        ( map-left-right-family-equifibered-dependent-span-diagram Q s)
+        ( right-map-equiv-equifibered-dependent-span-diagram
+          ( right-map-span-diagram 𝒮 s))
+    coherence-left-right-equiv-equifibered-dependent-span-diagram s =
+      pasting-vertical-coherence-square-maps
+        ( left-map-equiv-equifibered-dependent-span-diagram
+          ( left-map-span-diagram 𝒮 s))
+        ( map-inv-left-family-equifibered-dependent-span-diagram P s)
+        ( map-inv-left-family-equifibered-dependent-span-diagram Q s)
+        ( spanning-type-map-equiv-equifibered-dependent-span-diagram s)
+        ( map-right-family-equifibered-dependent-span-diagram P s)
+        ( map-right-family-equifibered-dependent-span-diagram Q s)
+        ( right-map-equiv-equifibered-dependent-span-diagram
+          ( right-map-span-diagram 𝒮 s))
+        (vertical-inv-equiv-coherence-square-maps
+          ( spanning-type-map-equiv-equifibered-dependent-span-diagram s)
+          ( equiv-left-family-equifibered-dependent-span-diagram P s)
+          ( equiv-left-family-equifibered-dependent-span-diagram Q s)
+          ( left-map-equiv-equifibered-dependent-span-diagram
+            ( left-map-span-diagram 𝒮 s))
+          ( coherence-left-equiv-equifibered-dependent-span-diagram s))
+        ( coherence-right-equiv-equifibered-dependent-span-diagram s)
+
+    coherence-right-left-equiv-equifibered-dependent-span-diagram :
+      (s : spanning-type-span-diagram 𝒮) →
+      coherence-square-maps
+        ( right-map-equiv-equifibered-dependent-span-diagram
+          ( right-map-span-diagram 𝒮 s))
+        ( map-right-left-family-equifibered-dependent-span-diagram P s)
+        ( map-right-left-family-equifibered-dependent-span-diagram Q s)
+        ( left-map-equiv-equifibered-dependent-span-diagram
+          ( left-map-span-diagram 𝒮 s))
+    coherence-right-left-equiv-equifibered-dependent-span-diagram s =
+      pasting-vertical-coherence-square-maps
+        ( right-map-equiv-equifibered-dependent-span-diagram
+          ( right-map-span-diagram 𝒮 s))
+        ( map-inv-right-family-equifibered-dependent-span-diagram P s)
+        ( map-inv-right-family-equifibered-dependent-span-diagram Q s)
+        ( spanning-type-map-equiv-equifibered-dependent-span-diagram s)
+        ( map-left-family-equifibered-dependent-span-diagram P s)
+        ( map-left-family-equifibered-dependent-span-diagram Q s)
+        ( left-map-equiv-equifibered-dependent-span-diagram
+          ( left-map-span-diagram 𝒮 s))
+        ( vertical-inv-equiv-coherence-square-maps
+          ( spanning-type-map-equiv-equifibered-dependent-span-diagram s)
+          ( equiv-right-family-equifibered-dependent-span-diagram P s)
+          ( equiv-right-family-equifibered-dependent-span-diagram Q s)
+          ( right-map-equiv-equifibered-dependent-span-diagram
+            ( right-map-span-diagram 𝒮 s))
+          ( coherence-right-equiv-equifibered-dependent-span-diagram s))
+        ( coherence-left-equiv-equifibered-dependent-span-diagram s)
+```
+
+### The identity equivalence of equifibered dependent span diagrams
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : equifibered-dependent-span-diagram 𝒮 l4 l5 l6)
+  where
+
+  id-equiv-equifibered-dependent-span-diagram :
+    equiv-equifibered-dependent-span-diagram P P
+  id-equiv-equifibered-dependent-span-diagram =
+    ( λ _ → id-equiv) ,
+    ( λ _ → id-equiv) ,
+    ( λ _ → id-equiv) ,
+    ( λ _ → refl-htpy) ,
+    ( λ _ → refl-htpy)
+```
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 0a68a9200c..62d678d3b2 100644
--- a/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md
@@ -50,11 +50,11 @@ module _
   where
 
   family-with-descent-data-pushout :
-    (l5 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5)
-  family-with-descent-data-pushout l5 =
-    Σ ( X → UU l5)
+    (l5 l6 l7 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6 ⊔ lsuc l7)
+  family-with-descent-data-pushout l5 l6 l7 =
+    Σ ( X → UU l7)
       ( λ P →
-        Σ ( descent-data-pushout 𝒮 l5)
+        Σ ( descent-data-pushout 𝒮 l5 l6)
           ( λ Q →
             equiv-descent-data-pushout
               ( descent-data-family-cocone-span-diagram c P)
@@ -65,15 +65,15 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
-  (P : family-with-descent-data-pushout c l5)
+  (P : family-with-descent-data-pushout c l5 l6 l7)
   where
 
-  family-cocone-family-with-descent-data-pushout : X → UU l5
+  family-cocone-family-with-descent-data-pushout : X → UU l7
   family-cocone-family-with-descent-data-pushout = pr1 P
 
-  descent-data-family-with-descent-data-pushout : descent-data-pushout 𝒮 l5
+  descent-data-family-with-descent-data-pushout : descent-data-pushout 𝒮 l5 l6
   descent-data-family-with-descent-data-pushout = pr1 (pr2 P)
 
   left-family-family-with-descent-data-pushout :
@@ -83,7 +83,7 @@ module _
       ( descent-data-family-with-descent-data-pushout)
 
   right-family-family-with-descent-data-pushout :
-    codomain-span-diagram 𝒮 → UU l5
+    codomain-span-diagram 𝒮 → UU l6
   right-family-family-with-descent-data-pushout =
     right-family-descent-data-pushout
       ( descent-data-family-with-descent-data-pushout)
@@ -224,8 +224,7 @@ module _
         ( family-cocone-family-with-descent-data-pushout)
         ( coherence-square-cocone _ _ c s))
       ( map-family-family-with-descent-data-pushout s)
-      ( right-map-family-with-descent-data-pushout
-        ( right-map-span-diagram 𝒮 s))
+      ( right-map-family-with-descent-data-pushout (right-map-span-diagram 𝒮 s))
   coherence-family-with-descent-data-pushout =
     coherence-equiv-descent-data-pushout
       ( descent-data-family-cocone-span-diagram c
@@ -243,12 +242,11 @@ module _
   where
 
   family-with-descent-data-pushout-family-cocone :
-    {l5 : Level} (P : X → UU l5) →
-    family-with-descent-data-pushout c l5
-  pr1 (family-with-descent-data-pushout-family-cocone P) = P
+    {l : Level} (P : X → UU l) → family-with-descent-data-pushout c l l l
+  pr1 (family-with-descent-data-pushout-family-cocone P) =
+    P
   pr1 (pr2 (family-with-descent-data-pushout-family-cocone P)) =
     descent-data-family-cocone-span-diagram c P
   pr2 (pr2 (family-with-descent-data-pushout-family-cocone P)) =
-    id-equiv-descent-data-pushout
-      ( descent-data-family-cocone-span-diagram c P)
+    id-equiv-descent-data-pushout (descent-data-family-cocone-span-diagram c P)
 ```
diff --git a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
index 552c91b146..abddcc385a 100644
--- a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
+++ b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
@@ -137,7 +137,7 @@ module _
       universal-property-coequalizer-universal-property-pushout
         ( double-arrow-flattening-lemma-coequalizer a P e)
         ( cofork-flattening-lemma-coequalizer a P e)
-        ( universal-property-pushout-bottom-universal-property-pushout-top-cube-is-equiv
+        ( universal-property-pushout-bottom-universal-property-pushout-top-cube-equiv
           ( vertical-map-span-cocone-cofork
             ( double-arrow-flattening-lemma-coequalizer a P e))
           ( horizontal-map-span-cocone-cofork
@@ -166,16 +166,15 @@ module _
             ( vertical-map-span-cocone-cofork a)
             ( horizontal-map-span-cocone-cofork a)
             ( cocone-codiagonal-cofork a e))
-          ( map-equiv
-            ( right-distributive-Σ-coproduct
-              ( domain-double-arrow a)
-              ( domain-double-arrow a)
-              ( ( P) ∘
-                ( horizontal-map-cocone-cofork a e) ∘
-                ( vertical-map-span-cocone-cofork a))))
-          ( id)
-          ( id)
-          ( id)
+          ( right-distributive-Σ-coproduct
+            ( domain-double-arrow a)
+            ( domain-double-arrow a)
+            ( ( P) ∘
+              ( horizontal-map-cocone-cofork a e) ∘
+              ( vertical-map-span-cocone-cofork a)))
+          ( id-equiv)
+          ( id-equiv)
+          ( id-equiv)
           ( coherence-square-cocone-flattening-pushout P
             ( vertical-map-span-cocone-cofork a)
             ( horizontal-map-span-cocone-cofork a)
@@ -191,16 +190,6 @@ module _
             ( ind-coproduct _
               ( ev-pair refl-htpy)
               ( ev-pair (λ t → ap-id _ ∙ inv right-unit))))
-          ( is-equiv-map-equiv
-            ( right-distributive-Σ-coproduct
-              ( domain-double-arrow a)
-              ( domain-double-arrow a)
-              ( ( P) ∘
-                ( horizontal-map-cocone-cofork a e) ∘
-                ( vertical-map-span-cocone-cofork a))))
-          ( is-equiv-id)
-          ( is-equiv-id)
-          ( is-equiv-id)
           ( flattening-lemma-pushout P
             ( vertical-map-span-cocone-cofork a)
             ( horizontal-map-span-cocone-cofork a)
diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md
index a5842aaa89..60e5eb54ea 100644
--- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md
@@ -29,7 +29,9 @@ 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.equifibered-dependent-span-diagrams
 open import synthetic-homotopy-theory.equivalences-descent-data-pushouts
+open import synthetic-homotopy-theory.equivalences-equifibered-dependent-span-diagrams
 open import synthetic-homotopy-theory.universal-property-pushouts
 ```
 
@@ -37,19 +39,20 @@ open import synthetic-homotopy-theory.universal-property-pushouts
 
 ## Idea
 
-The **flattening lemma** for [pushouts](synthetic-homotopy-theory.pushouts.md)
-states that pushouts commute with
-[dependent pair types](foundation.dependent-pair-types.md). More precisely,
-given a pushout square
+The
+{{#concept "flattening lemma" Disambiguation="for pushouts" Agda=flattening-lemma-pushout Agda=flattening-lemma-descent-data-pushout}}
+for [pushouts](synthetic-homotopy-theory.pushouts.md) states that pushouts
+commute with [dependent pair types](foundation.dependent-pair-types.md). More
+precisely, given a pushout square
 
 ```text
-      g
-  S -----> B
-  |        |
- f|        | j
-  ∨      ⌜ ∨
-  A -----> X
-      i
+         g
+    S ------> B
+    |         |
+  f |         | j
+    ∨       ⌜ ∨
+    A ------> X
+         i
 ```
 
 with homotopy `H : i ∘ f ~ j ∘ g`, and for any type family `P` over `X`, the
@@ -146,7 +149,7 @@ module _
       ( horizontal-map-span-flattening-pushout P _ _ c)
 ```
 
-### The statement of the flattening lemma for pushouts, phrased using descent data
+### The statement of the flattening lemma for pushouts, using descent data
 
 The above statement of the flattening lemma works with a provided type family
 over the pushout. We can instead accept a definition of this family via descent
@@ -154,58 +157,65 @@ data for the pushout.
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
   where
 
   vertical-map-span-flattening-descent-data-pushout :
     Σ ( spanning-type-span-diagram 𝒮)
-      ( λ s → pr1 P (left-map-span-diagram 𝒮 s)) →
-    Σ ( domain-span-diagram 𝒮) (pr1 P)
+      ( left-family-descent-data-pushout P ∘ left-map-span-diagram 𝒮) →
+    Σ ( domain-span-diagram 𝒮) (left-family-descent-data-pushout P)
   vertical-map-span-flattening-descent-data-pushout =
     map-Σ-map-base
       ( left-map-span-diagram 𝒮)
-      ( pr1 P)
+      ( left-family-descent-data-pushout P)
 
   horizontal-map-span-flattening-descent-data-pushout :
     Σ ( spanning-type-span-diagram 𝒮)
-      ( λ s → pr1 P (left-map-span-diagram 𝒮 s)) →
-    Σ ( codomain-span-diagram 𝒮) (pr1 (pr2 P))
+      ( left-family-descent-data-pushout P ∘ left-map-span-diagram 𝒮) →
+    Σ ( codomain-span-diagram 𝒮) (right-family-descent-data-pushout P)
   horizontal-map-span-flattening-descent-data-pushout =
     map-Σ
-      ( pr1 (pr2 P))
+      ( right-family-descent-data-pushout P)
       ( right-map-span-diagram 𝒮)
-      ( λ s → map-equiv (pr2 (pr2 P) s))
+      ( map-family-descent-data-pushout P)
 
   span-diagram-flattening-descent-data-pushout :
-    span-diagram (l1 ⊔ l4) (l2 ⊔ l4) (l3 ⊔ l4)
+    span-diagram (l1 ⊔ l4) (l2 ⊔ l5) (l3 ⊔ l4)
   span-diagram-flattening-descent-data-pushout =
     make-span-diagram
       ( vertical-map-span-flattening-descent-data-pushout)
       ( horizontal-map-span-flattening-descent-data-pushout)
 
 module _
-  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
+  { l1 l2 l3 l4 l5 l6 l7 : 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 : descent-data-pushout (make-span-diagram f g) l5)
-  ( Q : X → UU l5)
+  ( P : descent-data-pushout (make-span-diagram f g) l5 l6)
+  ( Q : X → UU l7)
   ( e :
     equiv-descent-data-pushout P (descent-data-family-cocone-span-diagram c Q))
   where
 
   horizontal-map-cocone-flattening-descent-data-pushout :
-    Σ A (pr1 P) → Σ X Q
+    Σ A (left-family-descent-data-pushout P) → Σ X Q
   horizontal-map-cocone-flattening-descent-data-pushout =
     map-Σ Q
       ( horizontal-map-cocone f g c)
-      ( λ a → map-equiv (pr1 e a))
+      ( left-map-equiv-descent-data-pushout
+        ( P)
+        ( descent-data-family-cocone-span-diagram c Q)
+        ( e))
 
   vertical-map-cocone-flattening-descent-data-pushout :
-    Σ B (pr1 (pr2 P)) → Σ X Q
+    Σ B (right-family-descent-data-pushout P) → Σ X Q
   vertical-map-cocone-flattening-descent-data-pushout =
     map-Σ Q
       ( vertical-map-cocone f g c)
-      ( λ b → map-equiv (pr1 (pr2 e) b))
+      ( right-map-equiv-descent-data-pushout
+        ( P)
+        ( descent-data-family-cocone-span-diagram c Q)
+        ( e))
 
   coherence-square-cocone-flattening-descent-data-pushout :
     coherence-square-maps
@@ -216,8 +226,16 @@ module _
   coherence-square-cocone-flattening-descent-data-pushout =
     htpy-map-Σ Q
       ( coherence-square-cocone f g c)
-      ( λ s → map-equiv (pr1 e (f s)))
-      ( λ s → inv-htpy (pr2 (pr2 e) s))
+      ( ( left-map-equiv-descent-data-pushout
+          ( P)
+          ( descent-data-family-cocone-span-diagram c Q)
+          ( e)) ∘
+        ( f))
+      ( inv-htpy ∘
+        coherence-equiv-descent-data-pushout
+          ( P)
+          ( descent-data-family-cocone-span-diagram c Q)
+          ( e))
 
   cocone-flattening-descent-data-pushout :
     cocone
@@ -240,6 +258,118 @@ module _
       ( cocone-flattening-descent-data-pushout)
 ```
 
+### The statement of the flattening lemma for pushouts, using equifibered dependent span diagrams
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : equifibered-dependent-span-diagram 𝒮 l4 l5 l6)
+  where
+
+  vertical-map-span-flattening-equifibered-dependent-span-diagram :
+    Σ ( spanning-type-span-diagram 𝒮)
+      ( spanning-type-family-equifibered-dependent-span-diagram P) →
+    Σ ( domain-span-diagram 𝒮)
+      ( left-family-equifibered-dependent-span-diagram P)
+  vertical-map-span-flattening-equifibered-dependent-span-diagram =
+    map-Σ
+      ( left-family-equifibered-dependent-span-diagram P)
+      ( left-map-span-diagram 𝒮)
+      ( map-left-family-equifibered-dependent-span-diagram P)
+
+  horizontal-map-span-flattening-equifibered-dependent-span-diagram :
+    Σ ( spanning-type-span-diagram 𝒮)
+      ( spanning-type-family-equifibered-dependent-span-diagram P) →
+    Σ ( codomain-span-diagram 𝒮)
+      ( right-family-equifibered-dependent-span-diagram P)
+  horizontal-map-span-flattening-equifibered-dependent-span-diagram =
+    map-Σ
+      ( right-family-equifibered-dependent-span-diagram P)
+      ( right-map-span-diagram 𝒮)
+      ( map-right-family-equifibered-dependent-span-diagram P)
+
+  span-diagram-flattening-equifibered-dependent-span-diagram :
+    span-diagram (l1 ⊔ l4) (l2 ⊔ l5) (l3 ⊔ l6)
+  span-diagram-flattening-equifibered-dependent-span-diagram =
+    make-span-diagram
+      ( vertical-map-span-flattening-equifibered-dependent-span-diagram)
+      ( horizontal-map-span-flattening-equifibered-dependent-span-diagram)
+
+module _
+  { l1 l2 l3 l4 l5 l6 l7 l8 : 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 : equifibered-dependent-span-diagram (make-span-diagram f g) l5 l6 l7)
+  ( Q : X → UU l8)
+  ( e :
+    equiv-equifibered-dependent-span-diagram
+      ( P)
+      ( equifibered-dependent-span-diagram-family-cocone-span-diagram c Q))
+  where
+
+  horizontal-map-cocone-flattening-equifibered-dependent-span-diagram :
+    Σ A (left-family-equifibered-dependent-span-diagram P) → Σ X Q
+  horizontal-map-cocone-flattening-equifibered-dependent-span-diagram =
+    map-Σ Q
+      ( horizontal-map-cocone f g c)
+      ( left-map-equiv-equifibered-dependent-span-diagram
+        ( P)
+        ( equifibered-dependent-span-diagram-family-cocone-span-diagram c Q)
+        ( e))
+
+  vertical-map-cocone-flattening-equifibered-dependent-span-diagram :
+    Σ B (right-family-equifibered-dependent-span-diagram P) → Σ X Q
+  vertical-map-cocone-flattening-equifibered-dependent-span-diagram =
+    map-Σ Q
+      ( vertical-map-cocone f g c)
+      ( right-map-equiv-equifibered-dependent-span-diagram
+        ( P)
+        ( equifibered-dependent-span-diagram-family-cocone-span-diagram c Q)
+        ( e))
+```
+
+> The rest remains to be formalized.
+
+```text
+  coherence-square-cocone-flattening-equifibered-dependent-span-diagram :
+    coherence-square-maps
+      ( horizontal-map-span-flattening-equifibered-dependent-span-diagram P)
+      ( vertical-map-span-flattening-equifibered-dependent-span-diagram P)
+      ( vertical-map-cocone-flattening-equifibered-dependent-span-diagram)
+      ( horizontal-map-cocone-flattening-equifibered-dependent-span-diagram)
+  coherence-square-cocone-flattening-equifibered-dependent-span-diagram =
+    htpy-map-Σ Q
+      ( coherence-square-cocone f g c)
+      ( λ s t →
+        left-map-equiv-equifibered-dependent-span-diagram
+          ( P)
+          ( equifibered-dependent-span-diagram-family-cocone-span-diagram c Q)
+          ( e)
+          ( f s)
+          ( map-left-family-equifibered-dependent-span-diagram P s t))
+      ( λ s t → {!   !})
+
+  cocone-flattening-equifibered-dependent-span-diagram :
+    cocone
+      ( vertical-map-span-flattening-equifibered-dependent-span-diagram P)
+      ( horizontal-map-span-flattening-equifibered-dependent-span-diagram P)
+      ( Σ X Q)
+  pr1 cocone-flattening-equifibered-dependent-span-diagram =
+    horizontal-map-cocone-flattening-equifibered-dependent-span-diagram
+  pr1 (pr2 cocone-flattening-equifibered-dependent-span-diagram) =
+    vertical-map-cocone-flattening-equifibered-dependent-span-diagram
+  pr2 (pr2 cocone-flattening-equifibered-dependent-span-diagram) =
+    coherence-square-cocone-flattening-equifibered-dependent-span-diagram
+
+  flattening-lemma-equifibered-dependent-span-diagram-statement : UUω
+  flattening-lemma-equifibered-dependent-span-diagram-statement =
+    universal-property-pushout f g c →
+    universal-property-pushout
+      ( vertical-map-span-flattening-equifibered-dependent-span-diagram P)
+      ( horizontal-map-span-flattening-equifibered-dependent-span-diagram P)
+      ( cocone-flattening-equifibered-dependent-span-diagram)
+```
+
 ## Properties
 
 ### Proof of the flattening lemma for pushouts
@@ -354,10 +484,11 @@ descent data.
 
 ```agda
 module _
-  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
+  { l1 l2 l3 l4 l5 l6 l7 : 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 : descent-data-pushout (make-span-diagram f g) l5)
-  ( Q : X → UU l5)
+  ( P : descent-data-pushout (make-span-diagram f g) l5 l6)
+  ( Q : X → UU l7)
   ( e :
     equiv-descent-data-pushout P (descent-data-family-cocone-span-diagram c Q))
   where
@@ -372,9 +503,22 @@ module _
       ( horizontal-map-span-flattening-descent-data-pushout P)
       ( 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)))
+      ( tot
+        ( ( left-map-equiv-descent-data-pushout
+            ( P)
+            ( descent-data-family-cocone-span-diagram c Q)
+            ( e)) ∘
+          ( f)))
+      ( tot
+        ( left-map-equiv-descent-data-pushout
+          ( P)
+          ( descent-data-family-cocone-span-diagram c Q)
+          ( e)))
+      ( tot
+        ( right-map-equiv-descent-data-pushout
+          ( P)
+          ( descent-data-family-cocone-span-diagram c Q)
+          ( e)))
       ( id)
       ( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e)
       ( refl-htpy)
@@ -382,8 +526,17 @@ module _
         ( 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)))
+          ( tr Q (coherence-square-cocone f g c s)) ∘
+          ( left-map-equiv-descent-data-pushout
+            ( P)
+            ( descent-data-family-cocone-span-diagram c Q)
+            ( e)
+            ( f s)))
+        ( inv-htpy ∘
+          coherence-equiv-descent-data-pushout
+            ( P)
+            ( descent-data-family-cocone-span-diagram c Q)
+            ( e)))
       ( refl-htpy)
       ( refl-htpy)
       ( coherence-square-cocone-flattening-pushout Q f g c)
@@ -393,7 +546,13 @@ module _
         ( s , t))) ∙
     ( triangle-eq-pair-Σ Q
       ( coherence-square-cocone f g c s)
-      ( inv (pr2 (pr2 e) s t))) ∙
+      ( inv
+        ( coherence-equiv-descent-data-pushout
+          ( P)
+          ( descent-data-family-cocone-span-diagram c Q)
+          ( e)
+          ( s)
+          ( t)))) ∙
     ( ap
       ( eq-pair-Σ (coherence-square-cocone f g c s) refl ∙_)
       ( inv
@@ -402,13 +561,19 @@ module _
             ( vertical-map-cocone f g c)
             ( Q)
             ( refl)
-            ( inv (pr2 (pr2 e) s t))))))
+            ( inv
+              ( coherence-equiv-descent-data-pushout
+                ( P)
+                ( descent-data-family-cocone-span-diagram c Q)
+                ( e)
+                ( s)
+                ( t)))))))
 
   abstract
     flattening-lemma-descent-data-pushout :
       flattening-lemma-descent-data-pushout-statement f g c P Q e
     flattening-lemma-descent-data-pushout up-c =
-      universal-property-pushout-top-universal-property-pushout-bottom-cube-is-equiv
+      universal-property-pushout-top-universal-property-pushout-bottom-cube-equiv
         ( vertical-map-span-flattening-pushout Q f g c)
         ( horizontal-map-span-flattening-pushout Q f g c)
         ( horizontal-map-cocone-flattening-pushout Q f g c)
@@ -417,28 +582,49 @@ module _
         ( horizontal-map-span-flattening-descent-data-pushout P)
         ( 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)
+        ( equiv-tot
+          ( ( left-equiv-equiv-descent-data-pushout
+              ( P)
+              ( descent-data-family-cocone-span-diagram c Q)
+              ( e)) ∘
+            ( f)))
+        ( equiv-tot
+          ( left-equiv-equiv-descent-data-pushout
+            ( P)
+            ( descent-data-family-cocone-span-diagram c Q)
+            ( e)))
+        ( equiv-tot
+          ( right-equiv-equiv-descent-data-pushout
+            ( P)
+            ( descent-data-family-cocone-span-diagram c Q)
+            ( e)))
+        ( id-equiv)
         ( 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)))
+            ( tr Q (coherence-square-cocone f g c s)) ∘
+            ( left-map-equiv-descent-data-pushout
+              ( P)
+              ( descent-data-family-cocone-span-diagram c Q)
+              ( e)
+              ( f s)))
+          ( inv-htpy ∘
+            coherence-equiv-descent-data-pushout
+              ( P)
+              ( descent-data-family-cocone-span-diagram c Q)
+              ( e)))
         ( 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 up-c)
 ```
+
+## See also
+
+- [Mather's second cube theorem](synthetic-homotopy-theory.mathers-second-cube-theorem.md)
+  is the [unstraightened](foundation.type-duality.md) version of the flattening
+  lemma for pushouts.
diff --git a/src/synthetic-homotopy-theory/identity-systems-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/identity-systems-descent-data-pushouts.lagda.md
index ed4ca2232d..d6b2c7d3f5 100644
--- a/src/synthetic-homotopy-theory/identity-systems-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/identity-systems-descent-data-pushouts.lagda.md
@@ -156,15 +156,18 @@ section of `(RΣA, RΣB, RΣS)`, respectively.
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4) {a₀ : domain-span-diagram 𝒮}
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5) {a₀ : domain-span-diagram 𝒮}
   (p₀ : left-family-descent-data-pushout P a₀)
   where
 
   ev-refl-section-descent-data-pushout :
-    {l5 : Level}
+    {l6 l7 : Level}
     (R :
-      descent-data-pushout (span-diagram-flattening-descent-data-pushout P) l5)
+      descent-data-pushout
+        ( span-diagram-flattening-descent-data-pushout P)
+        ( l6)
+        ( l7))
     (t : section-descent-data-pushout R) →
     left-family-descent-data-pushout R (a₀ , p₀)
   ev-refl-section-descent-data-pushout R t =
@@ -175,18 +178,19 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4) {a₀ : domain-span-diagram 𝒮}
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5) {a₀ : domain-span-diagram 𝒮}
   (p₀ : left-family-descent-data-pushout P a₀)
   where
 
   is-identity-system-descent-data-pushout : UUω
   is-identity-system-descent-data-pushout =
-    {l5 : Level}
+    {l6 : Level}
     (R :
       descent-data-pushout
         ( span-diagram-flattening-descent-data-pushout P)
-        ( l5)) →
+        ( l6)
+        ( l6)) →
     section (ev-refl-section-descent-data-pushout P p₀ R)
 ```
 
@@ -232,9 +236,9 @@ section if and only if the right map has a section.
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
-  (P : family-with-descent-data-pushout c l5)
+  (P : family-with-descent-data-pushout c l5 l6 l7)
   {a₀ : domain-span-diagram 𝒮}
   (p₀ : left-family-family-with-descent-data-pushout P a₀)
   where
@@ -252,7 +256,7 @@ module _
         ( inv-equiv-descent-data-family-with-descent-data-pushout P)
 
   square-ev-refl-section-descent-data-pushout :
-    {l5 : Level}
+    {l5 l6 l7 : Level}
     (R :
       family-with-descent-data-pushout
         ( cocone-flattening-descent-data-pushout _ _ c
@@ -260,7 +264,9 @@ module _
           ( family-cocone-family-with-descent-data-pushout P)
           ( inv-equiv-descent-data-pushout _ _
             ( equiv-descent-data-family-with-descent-data-pushout P)))
-        ( l5)) →
+        ( l5)
+        ( l6)
+        ( l7)) →
     coherence-square-maps
       ( section-descent-data-section-family-cocone-span-diagram R ∘ ind-Σ)
       ( ev-refl-identity-system
@@ -307,7 +313,7 @@ right map has a section, hence the left map has a section.
                 ( up-c)))))
         ( id-system-P (descent-data-family-with-descent-data-pushout fam-R))
       where
-        fam-R : family-with-descent-data-pushout cocone-flattening l
+        fam-R : family-with-descent-data-pushout cocone-flattening l l l
         fam-R =
           family-with-descent-data-pushout-family-cocone
             ( cocone-flattening)
@@ -340,7 +346,7 @@ assumption, so the right map has a section.
           ( section-map-equiv
             ( left-equiv-family-with-descent-data-pushout fam-R (a₀ , p₀))))
       where
-        fam-R : family-with-descent-data-pushout cocone-flattening l
+        fam-R : family-with-descent-data-pushout cocone-flattening l l l
         fam-R =
           family-with-descent-data-pushout-descent-data-pushout
             ( flattening-lemma-descent-data-pushout _ _ c
@@ -404,7 +410,7 @@ 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 : descent-data-pushout 𝒮 l5) {a₀ : domain-span-diagram 𝒮}
+  (P : descent-data-pushout 𝒮 l5 l5) {a₀ : domain-span-diagram 𝒮}
   (p₀ : left-family-descent-data-pushout P a₀)
   (id-system-P : is-identity-system-descent-data-pushout P p₀)
   where
@@ -446,7 +452,7 @@ module _
               ( up-c)
               ( id-system-P))))
       where
-      fam-P : family-with-descent-data-pushout c l5
+      fam-P : family-with-descent-data-pushout c l5 l5 l5
       fam-P = family-with-descent-data-pushout-descent-data-pushout up-c P
       p₀' :
         family-cocone-family-with-descent-data-pushout
@@ -481,7 +487,7 @@ 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 : descent-data-pushout 𝒮 l5) {a₀ : domain-span-diagram 𝒮}
+  (P : descent-data-pushout 𝒮 l5 l5) {a₀ : domain-span-diagram 𝒮}
   (p₀ : left-family-descent-data-pushout P a₀)
   where
 
@@ -492,6 +498,7 @@ module _
         (R :
           descent-data-pushout
             ( span-diagram-flattening-descent-data-pushout P)
+            ( l6)
             ( l6))
         (r₀ : left-family-descent-data-pushout R (a₀ , p₀)) →
         section-descent-data-pushout R) →
diff --git a/src/synthetic-homotopy-theory/mathers-second-cube-theorem.lagda.md b/src/synthetic-homotopy-theory/mathers-second-cube-theorem.lagda.md
new file mode 100644
index 0000000000..cb7ed90226
--- /dev/null
+++ b/src/synthetic-homotopy-theory/mathers-second-cube-theorem.lagda.md
@@ -0,0 +1,155 @@
+# Mather's second cube theorem
+
+```agda
+module synthetic-homotopy-theory.mathers-second-cube-theorem 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
+open import foundation.equality-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.functoriality-fibers-of-maps
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.morphisms-arrows
+open import foundation.pullbacks
+open import foundation.span-diagrams
+open import foundation.transport-along-identifications
+open import foundation.universal-property-dependent-pair-types
+open import foundation.universal-property-pullbacks
+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.equivalences-descent-data-pushouts
+open import synthetic-homotopy-theory.flattening-lemma-pushouts
+open import synthetic-homotopy-theory.pushouts
+open import synthetic-homotopy-theory.universal-property-pushouts
+```
+
+</details>
+
+## Idea
+
+{{#concept "Mather's second cube theorem" Disambiguation="for types"}} states
+that every base change of a [pushout](synthetic-homotopy-theory.pushouts.md)
+square is a pushout. In other words, if we are given a
+[commuting cube](foundation.commuting-cubes-of-maps.md) where the bottom face is
+a pushout and the vertical faces are [pullbacks](foundation-core.pullbacks.md)
+
+```text
+  ∙ ----------------> ∙
+  |⌟\ ⌟               |⌟\
+  |  \                |  \
+  |   ∨               |   ∨
+  |     ∙ ----------------> ∙
+  |     | ⌟           |     |
+  ∨     |             ∨     |
+  ∙ ----|-----------> ∙     |
+    \   |               \   |
+     \  |                \  |
+      ∨ ∨               ⌜ ∨ ∨
+        ∙ ----------------> ∙,
+```
+
+then the top face is also a pushout.
+
+## Theorem
+
+```text
+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')
+  (left : f ∘ hA ~ hB ∘ f')
+  (back : g ∘ hA ~ hC ∘ g')
+  (front : h ∘ hB ~ hD ∘ h')
+  (right : k ∘ hC ~ hD ∘ k')
+  (bottom : h ∘ f ~ k ∘ g)
+  (c :
+    coherence-cube-maps
+      f g h k f' g' h' k' hA hB hC hD
+      top left back front right bottom)
+  where
+
+  mathers-second-cube-theorem :
+    universal-property-pushout f g (h , k , bottom) →
+    universal-property-pullback h hD (hB , h' , front) →
+    universal-property-pullback k hD (hC , k' , right) →
+    universal-property-pullback f hB (hA , f' , left) →
+    universal-property-pullback g hC (hA , g' , back) →
+    universal-property-pushout f' g' (h' , k' , top)
+  mathers-second-cube-theorem po-bottom pb-front pb-right pb-left pb-back =
+    universal-property-pushout-top-universal-property-pushout-bottom-cube-equiv
+      _ _ _ _
+      f' g' h' k'
+      ( equiv-tot e-left ∘e inv-equiv-total-fiber' hA)
+      ( inv-equiv-total-fiber' hB)
+      ( inv-equiv-total-fiber' hC)
+      ( inv-equiv-total-fiber' hD)
+      ( top)
+      ( λ x →
+        eq-pair-Σ (left x) (inv-compute-tr-self-fiber' hB (f' x , left x)))
+      ( λ x →
+        eq-pair-Σ (back x) {!   !})
+      ( λ x →
+        eq-pair-Σ (front x) (inv-compute-tr-self-fiber' hD (h' x , front x)))
+      ( λ x →
+        eq-pair-Σ (right x) (inv-compute-tr-self-fiber' hD (k' x , right x)))
+      ( {!   !})
+      ( {!   !})
+      ( flattening-lemma-descent-data-pushout
+        ( f)
+        ( g)
+        ( h , k , bottom)
+        ( ( fiber' hB) ,
+          ( fiber' hC) ,
+          ( λ s →
+            ( inv-equiv (e-right (g s))) ∘e
+            ( equiv-tr (fiber' hD) (bottom s)) ∘e
+            ( e-front (f s))))
+        ( fiber' hD)
+        ( ( e-front) ,
+          ( e-right) ,
+          {!   !})
+        ( po-bottom))
+    where
+      e-left =
+        fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+          f hB (hA , f' , left) pb-left
+      e-front =
+        fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+          h hD (hB , h' , front) pb-front
+      e-right =
+        fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+          k hD (hC , k' , right) pb-right
+```
+
+## See also
+
+- Mather's second cube theorem is the
+  [unstraightened](foundation.type-duality.md) version of the
+  [flattening lemma for pushouts](synthetic-homotopy-theory.flattening-lemma-pushouts.md)
+- The
+  [descent property for pushouts](synthetic-homotopy-theory.descent-property-pushouts.md).
+
+## External links
+
+- [Mather's Second Cube Theorem](https://kerodon.net/tag/011H) on Kerodon
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..317bf3a29e 100644
--- a/src/synthetic-homotopy-theory/morphisms-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/morphisms-descent-data-pushouts.lagda.md
@@ -121,12 +121,12 @@ proofs of `is-equiv` of their gluing maps.
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
-  (Q : descent-data-pushout 𝒮 l5)
+  {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
+  (Q : descent-data-pushout 𝒮 l6 l7)
   where
 
-  hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
+  hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7)
   hom-descent-data-pushout =
     Σ ( (a : domain-span-diagram 𝒮) →
         left-family-descent-data-pushout P a →
@@ -173,8 +173,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
   where
 
   id-hom-descent-data-pushout : hom-descent-data-pushout P P
@@ -187,10 +187,10 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
-  (Q : descent-data-pushout 𝒮 l5)
-  (R : descent-data-pushout 𝒮 l6)
+  {l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
+  (Q : descent-data-pushout 𝒮 l6 l7)
+  (R : descent-data-pushout 𝒮 l8 l9)
   (g : hom-descent-data-pushout Q R)
   (f : hom-descent-data-pushout P Q)
   where
@@ -223,13 +223,13 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
-  (Q : descent-data-pushout 𝒮 l5)
+  {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
+  (Q : descent-data-pushout 𝒮 l6 l7)
   (f g : hom-descent-data-pushout P Q)
   where
 
-  htpy-hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
+  htpy-hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7)
   htpy-hom-descent-data-pushout =
     Σ ( (a : domain-span-diagram 𝒮) →
         left-map-hom-descent-data-pushout P Q f a ~
@@ -253,9 +253,9 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
-  (Q : descent-data-pushout 𝒮 l5)
+  {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
+  (Q : descent-data-pushout 𝒮 l6 l7)
   (f : hom-descent-data-pushout P Q)
   where
 
@@ -271,9 +271,9 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
-  (Q : descent-data-pushout 𝒮 l5)
+  {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
+  (Q : descent-data-pushout 𝒮 l6 l7)
   (f : hom-descent-data-pushout P Q)
   where
 
diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index 8c280f7233..e2737409b4 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -33,6 +33,7 @@ open import synthetic-homotopy-theory.dependent-cocones-under-spans
 open import synthetic-homotopy-theory.dependent-universal-property-pushouts
 open import synthetic-homotopy-theory.flattening-lemma-pushouts
 open import synthetic-homotopy-theory.induction-principle-pushouts
+open import synthetic-homotopy-theory.pullback-property-pushouts
 open import synthetic-homotopy-theory.universal-property-pushouts
 ```
 
@@ -459,6 +460,27 @@ module _
       ( up-pushout f g)
 ```
 
+### Pushout cocones satisfy the pullback property of the pushout
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X)
+  where
+
+  pullback-property-pushout-is-pushout :
+    is-pushout f g c → pullback-property-pushout f g c
+  pullback-property-pushout-is-pushout po =
+    pullback-property-pushout-universal-property-pushout f g c
+      ( universal-property-pushout-is-pushout f g c po)
+
+  is-pushout-pullback-property-pushout :
+    pullback-property-pushout f g c → is-pushout f g c
+  is-pushout-pullback-property-pushout pb =
+    is-pushout-universal-property-pushout f g c
+      ( universal-property-pushout-pullback-property-pushout f g c pb)
+```
+
 ### Fibers of the cogap map
 
 We characterize the [fibers](foundation-core.fibers-of-maps.md) of the cogap map
diff --git a/src/synthetic-homotopy-theory/sections-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/sections-descent-data-pushouts.lagda.md
index d62567bd92..3aa96421eb 100644
--- a/src/synthetic-homotopy-theory/sections-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/sections-descent-data-pushouts.lagda.md
@@ -107,11 +107,11 @@ homotopies between them.
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
   where
 
-  section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
   section-descent-data-pushout =
     Σ ( (a : domain-span-diagram 𝒮) → left-family-descent-data-pushout P a)
       ( λ tA →
@@ -147,12 +147,12 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
   (r t : section-descent-data-pushout P)
   where
 
-  htpy-section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  htpy-section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
   htpy-section-descent-data-pushout =
     Σ ( left-map-section-descent-data-pushout P r ~
         left-map-section-descent-data-pushout P t)
@@ -174,8 +174,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
   (r : section-descent-data-pushout P)
   where
 
@@ -192,8 +192,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4 l5)
   (r : section-descent-data-pushout P)
   where
 
@@ -281,9 +281,9 @@ equivalence. It follows that the left map is an equivalence
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
-  (P : family-with-descent-data-pushout c l5)
+  (P : family-with-descent-data-pushout c l5 l6 l7)
   where
 
   section-descent-data-section-family-cocone-span-diagram :
@@ -381,10 +381,10 @@ homotopies of sections of `(PA, PB, PS)`.
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 l7 : 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)
+  (P : family-with-descent-data-pushout c l5 l6 l7)
   (t :
     section-descent-data-pushout
       ( descent-data-family-with-descent-data-pushout P))
diff --git a/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md b/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md
index 14abaccfc2..31d4fe2ff3 100644
--- a/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md
@@ -195,7 +195,7 @@ module _
     universal-property-coequalizer a c
   universal-property-coequalizer-equiv-cofork-equiv-double-arrow up-c' =
     universal-property-coequalizer-universal-property-pushout a c
-      ( universal-property-pushout-top-universal-property-pushout-bottom-cube-is-equiv
+      ( universal-property-pushout-top-universal-property-pushout-bottom-cube-equiv
         ( vertical-map-span-cocone-cofork a')
         ( horizontal-map-span-cocone-cofork a')
         ( horizontal-map-cocone-cofork a' c')
@@ -204,11 +204,12 @@ module _
         ( horizontal-map-span-cocone-cofork a)
         ( horizontal-map-cocone-cofork a c)
         ( vertical-map-cocone-cofork a c)
-        ( spanning-map-hom-span-diagram-cofork-hom-double-arrow a a'
-          ( hom-equiv-double-arrow a a' e))
-        ( domain-map-equiv-double-arrow a a' e)
-        ( codomain-map-equiv-double-arrow a a' e)
-        ( map-equiv-cofork-equiv-double-arrow c c' e e')
+        ( equiv-coproduct
+          ( domain-equiv-equiv-double-arrow a a' e)
+          ( domain-equiv-equiv-double-arrow a a' e))
+        ( domain-equiv-equiv-double-arrow a a' e)
+        (codomain-equiv-equiv-double-arrow a a' e)
+        ( equiv-equiv-cofork-equiv-double-arrow c c' e e')
         ( coherence-square-cocone-cofork a c)
         ( inv-htpy
           ( left-square-hom-span-diagram-cofork-hom-double-arrow a a'
@@ -264,12 +265,6 @@ module _
             ( ind-coproduct _
               ( right-unit-htpy)
               ( coh-equiv-cofork-equiv-double-arrow c c' e e'))))
-        ( is-equiv-map-coproduct
-          ( is-equiv-domain-map-equiv-double-arrow a a' e)
-          ( is-equiv-domain-map-equiv-double-arrow a a' e))
-        ( is-equiv-domain-map-equiv-double-arrow a a' e)
-        ( is-equiv-codomain-map-equiv-double-arrow a a' e)
-        ( is-equiv-map-equiv-cofork-equiv-double-arrow c c' e e')
         ( universal-property-pushout-universal-property-coequalizer a' c'
           ( up-c')))
 
diff --git a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md
index 06f4082d85..2191989aef 100644
--- a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md
@@ -998,4 +998,75 @@ module _
             ( h' , k' , top)
             ( up-top)
             ( W)))
+
+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 : coherence-square-maps g' f' k' h')
+  ( back-left : coherence-square-maps f' (map-equiv hA) (map-equiv hB) f)
+  ( back-right : coherence-square-maps g' (map-equiv hA) (map-equiv hC) g)
+  ( front-left : coherence-square-maps h' (map-equiv hB) (map-equiv hD) h)
+  ( front-right : coherence-square-maps k' (map-equiv hC) (map-equiv hD) k)
+  ( bottom : coherence-square-maps g f k h)
+  ( c :
+    coherence-cube-maps f g h k f' g' h' k'
+      ( map-equiv hA)
+      ( map-equiv hB)
+      ( map-equiv hC)
+      ( map-equiv hD)
+      ( top)
+      ( back-left)
+      ( back-right)
+      ( front-left)
+      ( front-right)
+      ( bottom))
+  where
+
+  universal-property-pushout-top-universal-property-pushout-bottom-cube-equiv :
+    universal-property-pushout f g (h , k , bottom) →
+    universal-property-pushout f' g' (h' , k' , top)
+  universal-property-pushout-top-universal-property-pushout-bottom-cube-equiv =
+    universal-property-pushout-top-universal-property-pushout-bottom-cube-is-equiv
+      f g h k f' g' h' k'
+      ( map-equiv hA)
+      ( map-equiv hB)
+      ( map-equiv hC)
+      ( map-equiv hD)
+      ( top)
+      ( back-left)
+      ( back-right)
+      ( front-left)
+      ( front-right)
+      ( bottom)
+      ( c)
+      ( is-equiv-map-equiv hA)
+      ( is-equiv-map-equiv hB)
+      ( is-equiv-map-equiv hC)
+      ( is-equiv-map-equiv hD)
+
+  universal-property-pushout-bottom-universal-property-pushout-top-cube-equiv :
+    universal-property-pushout f' g' (h' , k' , top) →
+    universal-property-pushout f g (h , k , bottom)
+  universal-property-pushout-bottom-universal-property-pushout-top-cube-equiv =
+    universal-property-pushout-bottom-universal-property-pushout-top-cube-is-equiv
+      f g h k f' g' h' k'
+      ( map-equiv hA)
+      ( map-equiv hB)
+      ( map-equiv hC)
+      ( map-equiv hD)
+      ( top)
+      ( back-left)
+      ( back-right)
+      ( front-left)
+      ( front-right)
+      ( bottom)
+      ( c)
+      ( is-equiv-map-equiv hA)
+      ( is-equiv-map-equiv hB)
+      ( is-equiv-map-equiv hC)
+      ( is-equiv-map-equiv hD)
 ```