From 4a7158b9247c29e16678e660e5b3df90110bf1a9 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 10 Mar 2025 18:09:41 +0000
Subject: [PATCH 01/13] anodyne maps

---
 src/foundation/equivalences-arrows.lagda.md   |   9 +-
 src/foundation/morphisms-arrows.lagda.md      |  38 +--
 src/orthogonal-factorization-systems.lagda.md |   1 +
 .../anodyne-maps.lagda.md                     | 209 ++++++++++++++
 .../orthogonal-maps.lagda.md                  | 259 ++++++++++++++++--
 .../cocartesian-morphisms-arrows.lagda.md     |  44 +++
 .../pushouts.lagda.md                         |  22 ++
 7 files changed, 544 insertions(+), 38 deletions(-)
 create mode 100644 src/orthogonal-factorization-systems/anodyne-maps.lagda.md

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/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/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index a167d57d4a..a05161db66 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -9,6 +9,7 @@
 ```agda
 module orthogonal-factorization-systems where
 
+open import orthogonal-factorization-systems.anodyne-maps public
 open import orthogonal-factorization-systems.cd-structures public
 open import orthogonal-factorization-systems.cellular-maps public
 open import orthogonal-factorization-systems.closed-modalities public
diff --git a/src/orthogonal-factorization-systems/anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md
new file mode 100644
index 0000000000..62718f0af7
--- /dev/null
+++ b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md
@@ -0,0 +1,209 @@
+# Anodyne maps
+
+```agda
+module orthogonal-factorization-systems.anodyne-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-morphisms-arrows
+open import foundation.cartesian-product-types
+open import foundation.composition-algebra
+open import foundation.contractible-maps
+open import foundation.contractible-types
+open import foundation.coproduct-types
+open import foundation.coproducts-pullbacks
+open import foundation.dependent-pair-types
+open import foundation.dependent-products-pullbacks
+open import foundation.dependent-sums-pullbacks
+open import foundation.equivalences
+open import foundation.equivalences-arrows
+open import foundation.fibered-maps
+open import foundation.fibers-of-maps
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-cartesian-product-types
+open import foundation.functoriality-coproduct-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.functoriality-fibers-of-maps
+open import foundation.homotopies
+open import foundation.morphisms-arrows
+open import foundation.postcomposition-functions
+open import foundation.postcomposition-pullbacks
+open import foundation.precomposition-dependent-functions
+open import foundation.precomposition-functions
+open import foundation.products-pullbacks
+open import foundation.propositions
+open import foundation.pullbacks
+open import foundation.retracts-of-maps
+open import foundation.type-arithmetic-dependent-function-types
+open import foundation.type-theoretic-principle-of-choice
+open import foundation.unit-type
+open import foundation.universal-property-cartesian-product-types
+open import foundation.universal-property-coproduct-types
+open import foundation.universal-property-dependent-pair-types
+open import foundation.universal-property-equivalences
+open import foundation.universal-property-pullbacks
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import orthogonal-factorization-systems.lifting-structures-on-squares
+open import orthogonal-factorization-systems.orthogonal-maps
+open import orthogonal-factorization-systems.pullback-hom
+open import orthogonal-factorization-systems.types-local-at-maps
+
+open import synthetic-homotopy-theory.cocartesian-morphisms-arrows
+```
+
+</details>
+
+## Idea
+
+A map $j : C → D$ is said to be
+{{#concept "anodyne" Disambiguation="map of types" Agda=is-anodyne}} with
+respect to a map $f : A → B$, or **$f$-anodyne** if every map that is orthogonal
+to $f$ is also orthogonal to $j$.
+
+## Definitions
+
+### The predicate of being anodyne with respect to a map
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  (f : A → B) (j : C → D)
+  where
+
+  is-anodyne-Level :
+    (l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6)
+  is-anodyne-Level l5 l6 =
+    {X : UU l5} {Y : UU l6} (g : X → Y) → is-orthogonal f g → is-orthogonal j g
+
+  is-anodyne : UUω
+  is-anodyne = {l5 l6 : Level} → is-anodyne-Level l5 l6
+```
+
+## Properties
+
+### Anodyne maps are closed under homotopies
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  (f : A → B) {j i : C → D}
+  where
+
+  is-anodyne-htpy : j ~ i → is-anodyne f j → is-anodyne f i
+  is-anodyne-htpy K J g H = is-orthogonal-htpy-left j g K (J g H)
+```
+
+### Anodyne maps are closed under equivalences of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {C' : UU l5} {D' : UU l6}
+  (f : A → B) {j : C → D} {j' : C' → D'}
+  where
+
+  is-anodyne-equiv-arrow : equiv-arrow j j' → is-anodyne f j → is-anodyne f j'
+  is-anodyne-equiv-arrow α J g H = is-orthogonal-left-equiv-arrow α g (J g H)
+```
+
+### Anodyne maps are closed under retracts of maps
+
+> This remains to be formalized.
+
+### Anodyne maps compose
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5}
+  (f : A → B) (j : C → D) (i : D → E)
+  where
+
+  is-anodyne-comp : is-anodyne f j → is-anodyne f i → is-anodyne f (i ∘ j)
+  is-anodyne-comp J I g H = is-orthogonal-left-comp j i g (J g H) (I g H)
+```
+
+### Cancellation property for anodyne maps
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5}
+  (f : A → B) (j : C → D) (i : D → E)
+  where
+
+  is-anodyne-left-factor :
+    is-anodyne f j → is-anodyne f (i ∘ j) → is-anodyne f i
+  is-anodyne-left-factor J IJ g H =
+    is-orthogonal-left-left-factor j i g (J g H) (IJ g H)
+```
+
+### Anodyne maps are closed under dependent sums
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {A : UU l1} {B : UU l2} {I : UU l3} {C : I → UU l4} {D : I → UU l5}
+  (f : A → B) (j : (i : I) → C i → D i)
+  where
+
+  is-anodyne-tot : ((i : I) → is-anodyne f (j i)) → is-anodyne f (tot j)
+  is-anodyne-tot J g H = is-orthogonal-left-tot j g (λ i → J i g H)
+```
+
+### Anodyne maps are closed under products
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6}
+  (f : A → B) (j : C → D) (i : E → F)
+  where
+
+  is-anodyne-map-product :
+    is-anodyne f j → is-anodyne f i → is-anodyne f (map-product j i)
+  is-anodyne-map-product J I g H =
+    is-orthogonal-left-product j i g (J g H) (I g H)
+```
+
+### Anodyne maps are closed under coproducts
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6}
+  (f : A → B) (j : C → D) (i : E → F)
+  where
+
+  is-anodyne-map-coproduct :
+    is-anodyne f j → is-anodyne f i → is-anodyne f (map-coproduct j i)
+  is-anodyne-map-coproduct J I g H =
+    is-orthogonal-left-coproduct j i g (J g H) (I g H)
+```
+
+### Anodyne maps are closed under cobase change
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6}
+  (f : A → B) (j : C → D) (i : E → F)
+  where
+
+  is-anodyne-cobase-change :
+    cocartesian-hom-arrow j i → is-anodyne f j → is-anodyne f i
+  is-anodyne-cobase-change α J g H =
+    is-orthogonal-left-cobase-change j i g α (J g H)
+```
+
+### Anodyne maps are closed under pushout-products
+
+> This remains to be formalized.
diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
index ec37ad84de..8a3d9bdcfe 100644
--- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
@@ -29,6 +29,7 @@ open import foundation.functoriality-coproduct-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.postcomposition-functions
 open import foundation.postcomposition-pullbacks
@@ -37,6 +38,7 @@ open import foundation.precomposition-functions
 open import foundation.products-pullbacks
 open import foundation.propositions
 open import foundation.pullbacks
+open import foundation.type-arithmetic-cartesian-product-types
 open import foundation.type-arithmetic-dependent-function-types
 open import foundation.type-theoretic-principle-of-choice
 open import foundation.unit-type
@@ -51,6 +53,10 @@ open import foundation.whiskering-homotopies-composition
 open import orthogonal-factorization-systems.lifting-structures-on-squares
 open import orthogonal-factorization-systems.pullback-hom
 open import orthogonal-factorization-systems.types-local-at-maps
+
+open import synthetic-homotopy-theory.cocartesian-morphisms-arrows
+open import synthetic-homotopy-theory.pullback-property-pushouts
+open import synthetic-homotopy-theory.pushouts
 ```
 
 </details>
@@ -426,19 +432,40 @@ module _
         ( ( commutative-htpy-postcomp-htpy-precomp F G) ∙h
           ( inv-htpy-right-unit-htpy)))
 
-  is-orthogonal-pullback-condition-htpy-left :
-    {f' : A → B} → f ~ f' →
-    is-orthogonal-pullback-condition f g →
-    is-orthogonal-pullback-condition f' g
-  is-orthogonal-pullback-condition-htpy-left F =
-    is-orthogonal-pullback-condition-htpy F refl-htpy
-
-  is-orthogonal-pullback-condition-htpy-right :
-    {g' : X → Y} → g ~ g' →
-    is-orthogonal-pullback-condition f g →
-    is-orthogonal-pullback-condition f g'
-  is-orthogonal-pullback-condition-htpy-right =
-    is-orthogonal-pullback-condition-htpy refl-htpy
+  abstract
+    is-orthogonal-pullback-condition-htpy-left :
+      {f' : A → B} → f ~ f' →
+      is-orthogonal-pullback-condition f g →
+      is-orthogonal-pullback-condition f' g
+    is-orthogonal-pullback-condition-htpy-left F =
+      is-orthogonal-pullback-condition-htpy F refl-htpy
+
+  abstract
+    is-orthogonal-pullback-condition-htpy-right :
+      {g' : X → Y} → g ~ g' →
+      is-orthogonal-pullback-condition f g →
+      is-orthogonal-pullback-condition f g'
+    is-orthogonal-pullback-condition-htpy-right =
+      is-orthogonal-pullback-condition-htpy refl-htpy
+
+  abstract
+    is-orthogonal-htpy :
+      {f' : A → B} {g' : X → Y} → f ~ f' → g ~ g' →
+      is-orthogonal f g → is-orthogonal f' g'
+    is-orthogonal-htpy {f'} {g'} F G H =
+      is-orthogonal-is-orthogonal-pullback-condition f' g'
+        ( is-orthogonal-pullback-condition-htpy F G
+          ( is-orthogonal-pullback-condition-is-orthogonal f g H))
+
+  abstract
+    is-orthogonal-htpy-left :
+      {f' : A → B} → f ~ f' → is-orthogonal f g → is-orthogonal f' g
+    is-orthogonal-htpy-left F = is-orthogonal-htpy F refl-htpy
+
+  abstract
+    is-orthogonal-htpy-right :
+      {g' : X → Y} → g ~ g' → is-orthogonal f g → is-orthogonal f g'
+    is-orthogonal-htpy-right = is-orthogonal-htpy refl-htpy
 ```
 
 ### Equivalences are orthogonal to every map
@@ -698,6 +725,70 @@ module _
         ( is-orthogonal-pullback-condition-is-orthogonal (h ∘ f) g HF))
 ```
 
+### Orthogonality is preserved by equivalences of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {A' : UU l3} {B' : UU l4} {X : UU l5} {Y : UU l6}
+  {f : A → B} {f' : A' → B'}
+  where
+
+  abstract
+    is-orthogonal-left-equiv-arrow :
+      equiv-arrow f f' → (g : X → Y) → is-orthogonal f g → is-orthogonal f' g
+    is-orthogonal-left-equiv-arrow α g F =
+      is-orthogonal-htpy-left
+        ( map-codomain-equiv-arrow f f' α ∘
+          f ∘
+          map-inv-domain-equiv-arrow f f' α)
+        ( g)
+        ( ( coh-equiv-arrow f f' α ·r map-inv-domain-equiv-arrow f f' α) ∙h
+          ( f' ·l is-section-map-inv-equiv (equiv-domain-equiv-arrow f f' α)))
+        ( is-orthogonal-left-comp
+          ( f ∘ map-inv-domain-equiv-arrow f f' α)
+          ( map-codomain-equiv-arrow f f' α)
+          ( g)
+          ( is-orthogonal-left-comp
+            ( map-inv-domain-equiv-arrow f f' α)
+            ( f)
+            ( g)
+            ( is-orthogonal-equiv-left (equiv-domain-inv-equiv-arrow f f' α) g)
+            ( F))
+          ( is-orthogonal-equiv-left (equiv-codomain-equiv-arrow f f' α) g))
+
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {X' : UU l5} {Y' : UU l6}
+  (f : A → B) {g : X → Y} {g' : X' → Y'}
+  where
+
+  abstract
+    is-orthogonal-right-equiv-arrow :
+      equiv-arrow g g' → is-orthogonal f g → is-orthogonal f g'
+    is-orthogonal-right-equiv-arrow α G =
+      is-orthogonal-htpy-right
+        ( f)
+        ( map-codomain-equiv-arrow g g' α ∘
+          g ∘
+          map-inv-domain-equiv-arrow g g' α)
+        ( ( coh-equiv-arrow g g' α ·r map-inv-domain-equiv-arrow g g' α) ∙h
+          ( g' ·l is-section-map-inv-equiv (equiv-domain-equiv-arrow g g' α)))
+        ( is-orthogonal-right-comp
+          ( f)
+          ( g ∘ map-inv-domain-equiv-arrow g g' α)
+          ( map-codomain-equiv-arrow g g' α)
+          ( is-orthogonal-equiv-right f (equiv-codomain-equiv-arrow g g' α))
+          ( is-orthogonal-right-comp
+            ( f)
+            ( map-inv-domain-equiv-arrow g g' α)
+            ( g)
+            ( G)
+            ( is-orthogonal-equiv-right
+              ( f)
+              ( equiv-domain-inv-equiv-arrow g g' α))))
+```
+
 ### Right orthogonality is preserved by dependent products
 
 If `f ⊥ gᵢ`, for each `i : I`, then `f ⊥ (map-Π g)`.
@@ -912,10 +1003,10 @@ module _
   (f : (i : I) → A i → B i) (g : X → Y)
   where
 
-  is-orthogonal-pullback-condition-left-Σ :
+  is-orthogonal-pullback-condition-left-tot :
     ((i : I) → is-orthogonal-pullback-condition (f i) g) →
     is-orthogonal-pullback-condition (tot f) g
-  is-orthogonal-pullback-condition-left-Σ F =
+  is-orthogonal-pullback-condition-left-tot F =
     is-pullback-top-is-pullback-bottom-cube-is-equiv
       ( map-Π (λ i → postcomp (B i) g))
       ( map-Π (λ i → precomp (f i) X))
@@ -951,14 +1042,56 @@ module _
         ( λ i → cone-pullback-hom (f i) g)
         ( F))
 
-  is-orthogonal-left-Σ :
+  is-orthogonal-left-tot :
     ((i : I) → is-orthogonal (f i) g) → is-orthogonal (tot f) g
-  is-orthogonal-left-Σ F =
+  is-orthogonal-left-tot F =
     is-orthogonal-is-orthogonal-pullback-condition (tot f) g
-      ( is-orthogonal-pullback-condition-left-Σ
+      ( is-orthogonal-pullback-condition-left-tot
         ( λ i → is-orthogonal-pullback-condition-is-orthogonal (f i) g (F i)))
 ```
 
+### Left orthogonality is preserved by products
+
+If `f ⊥ g` and `f' ⊥ g`, then `(f × f') ⊥ g`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y)
+  where
+
+  is-orthogonal-left-map-right-product :
+    {l5 : Level} (C : UU l5) →
+    is-orthogonal f g → is-orthogonal (map-product (id' C) f) g
+  is-orthogonal-left-map-right-product C F =
+    is-orthogonal-left-tot (λ _ → f) g (λ _ → F)
+
+  is-orthogonal-left-map-left-product :
+    {l5 : Level} (C : UU l5) →
+    is-orthogonal f g → is-orthogonal (map-product f (id' C)) g
+  is-orthogonal-left-map-left-product C F =
+    is-orthogonal-left-equiv-arrow
+      ( commutative-product , commutative-product , refl-htpy)
+      ( g)
+      ( is-orthogonal-left-map-right-product C F)
+
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {A' : UU l3} {B' : UU l4} {X : UU l5} {Y : UU l6}
+  (f : A → B) (f' : A' → B') (g : X → Y)
+  where
+
+  is-orthogonal-left-product :
+    is-orthogonal f g → is-orthogonal f' g → is-orthogonal (map-product f f') g
+  is-orthogonal-left-product F F' =
+    is-orthogonal-left-comp
+      ( map-product f id)
+      ( map-product id f')
+      ( g)
+      ( is-orthogonal-left-map-left-product f g A' F)
+      ( is-orthogonal-left-map-right-product f' g B F')
+```
+
 ### Left orthogonality is preserved by coproducts
 
 If `f ⊥ g` and `f' ⊥ g`, then `(f + f') ⊥ g`.
@@ -966,7 +1099,7 @@ If `f ⊥ g` and `f' ⊥ g`, then `(f + f') ⊥ g`.
 **Proof:** We need to show that the square
 
 ```text
-                     - ∘ (f + f')
+                   - ∘ (f + f')
   ((B + B') → X) ---------------> ((A + A') → X)
         |                               |
         |                               |
@@ -1114,6 +1247,94 @@ module _
         ( is-orthogonal-pullback-condition-is-orthogonal f g G))
 ```
 
+### Left orthogonality is preserved under cobase change
+
+Given a pushout square
+
+```text
+    A ------> A'
+    |         |
+  f'|         | f'
+    ∨       ⌜ ∨
+    B ------> B',
+```
+
+if `f ⊥ g`, then `f' ⊥ g`.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {A' : UU l5} {B' : UU l6}
+  (f : A → B) (f' : A' → B') (g : X → Y) (α : cocartesian-hom-arrow f f')
+  where
+
+  abstract
+    is-orthogonal-pullback-condition-left-cobase-change :
+      is-orthogonal-pullback-condition f g →
+      is-orthogonal-pullback-condition f' g
+    is-orthogonal-pullback-condition-left-cobase-change F =
+      is-pullback-swap-cone
+        ( postcomp A' g)
+        ( precomp f' Y)
+        ( precomp f' X , postcomp B' g , refl-htpy)
+        ( is-pullback-back-left-is-pullback-back-right-cube
+          ( refl-htpy)
+          ( refl-htpy)
+          ( inv-htpy (htpy-precomp (coh-cocartesian-hom-arrow f f' α) X))
+          ( inv-htpy (htpy-precomp (coh-cocartesian-hom-arrow f f' α) Y))
+          ( refl-htpy)
+          ( refl-htpy)
+          ( right-unit-htpy ∙h
+            ( inv ·l
+              commutative-postcomp-htpy-precomp g
+                ( coh-cocartesian-hom-arrow f f' α)) ∙h
+            ( inv-htpy
+              ( left-whisker-inv-htpy
+                ( postcomp A g)
+                ( htpy-precomp (coh-cocartesian-hom-arrow f f' α) X))) ∙h
+            ( inv-htpy-right-unit-htpy))
+          ( is-pullback-swap-cone
+            ( precomp f Y)
+            ( precomp (map-domain-cocartesian-hom-arrow f f' α) Y)
+            ( cone-hom-arrow
+              ( precomp (map-codomain-cocartesian-hom-arrow f f' α) Y)
+              ( precomp (map-domain-cocartesian-hom-arrow f f' α) Y)
+              ( transpose-precomp-hom-arrow f f'
+                ( hom-arrow-cocartesian-hom-arrow f f' α)
+                ( Y)))
+            ( pullback-property-pushout-is-pushout
+              ( f)
+              ( map-domain-cocartesian-hom-arrow f f' α)
+              ( cocone-cocartesian-hom-arrow f f' α)
+              ( is-cocartesian-cocartesian-hom-arrow f f' α)
+              ( Y)))
+          ( is-pullback-swap-cone
+            ( precomp f Y)
+            ( postcomp A g)
+            ( cone-pullback-hom f g)
+            ( F))
+          ( is-pullback-swap-cone
+            ( precomp f X)
+            ( precomp (map-domain-cocartesian-hom-arrow f f' α) X)
+            ( cone-hom-arrow
+              ( precomp (map-codomain-cocartesian-hom-arrow f f' α) X)
+              ( precomp (map-domain-cocartesian-hom-arrow f f' α) X)
+              ( transpose-precomp-hom-arrow f f'
+                ( hom-arrow-cocartesian-hom-arrow f f' α)
+                ( X)))
+            ( pullback-property-pushout-is-pushout f
+              ( map-domain-cocartesian-hom-arrow f f' α)
+              ( cocone-cocartesian-hom-arrow f f' α)
+              ( is-cocartesian-cocartesian-hom-arrow f f' α) X)))
+
+    is-orthogonal-left-cobase-change :
+      is-orthogonal f g → is-orthogonal f' g
+    is-orthogonal-left-cobase-change F =
+      is-orthogonal-is-orthogonal-pullback-condition f' g
+        ( is-orthogonal-pullback-condition-left-cobase-change
+          ( is-orthogonal-pullback-condition-is-orthogonal f g F))
+```
+
 ### A type is `f`-local if and only if its terminal map is `f`-orthogonal
 
 **Proof (forward direction):** If the terminal map is right orthogonal to `f`,
diff --git a/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md b/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md
index 9e34713e9c..e1188a0d13 100644
--- a/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md
+++ b/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md
@@ -7,13 +7,17 @@ module synthetic-homotopy-theory.cocartesian-morphisms-arrows where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.cartesian-morphisms-arrows
 open import foundation.commuting-squares-of-maps
 open import foundation.dependent-pair-types
 open import foundation.morphisms-arrows
+open import foundation.precomposition-functions
 open import foundation.propositions
+open import foundation.pullbacks
 open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.pullback-property-pushouts
 open import synthetic-homotopy-theory.pushouts
 open import synthetic-homotopy-theory.universal-property-pushouts
 ```
@@ -121,6 +125,46 @@ module _
       ( is-cocartesian-cocartesian-hom-arrow)
 ```
 
+### The cartesian morphism on precomposition maps
+
+```agda
+module _
+  {l1 l2 l3 l4 l : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y) (α : cocartesian-hom-arrow f g) (S : UU l)
+  where
+
+  precomp-cocartesian-hom-arrow : hom-arrow (precomp g S) (precomp f S)
+  precomp-cocartesian-hom-arrow =
+    precomp-hom-arrow f g (hom-arrow-cocartesian-hom-arrow f g α) S
+
+  is-cartesian-precomp-cocartesian-hom-arrow :
+    is-cartesian-hom-arrow
+      ( precomp g S)
+      ( precomp f S)
+      ( precomp-cocartesian-hom-arrow)
+  is-cartesian-precomp-cocartesian-hom-arrow =
+    is-pullback-swap-cone
+      ( precomp f S)
+      ( precomp (map-domain-cocartesian-hom-arrow f g α) S)
+      ( cone-hom-arrow
+        ( precomp (map-codomain-cocartesian-hom-arrow f g α) S)
+        ( precomp (map-domain-cocartesian-hom-arrow f g α) S)
+        ( transpose-precomp-hom-arrow f g
+          ( hom-arrow-cocartesian-hom-arrow f g α)
+          ( S)))
+      ( pullback-property-pushout-is-pushout
+        ( f)
+        ( map-domain-cocartesian-hom-arrow f g α)
+        ( cocone-cocartesian-hom-arrow f g α)
+        ( is-cocartesian-cocartesian-hom-arrow f g α) S)
+
+  precomp-cartesian-hom-arrow-cocartesian-hom-arrow :
+    cartesian-hom-arrow (precomp g S) (precomp f S)
+  precomp-cartesian-hom-arrow-cocartesian-hom-arrow =
+    ( precomp-cocartesian-hom-arrow ,
+      is-cartesian-precomp-cocartesian-hom-arrow)
+```
+
 ## See also
 
 - [Cartesian morphisms of arrows](foundation.cartesian-morphisms-arrows.md) for
diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index 1b5112681f..2141345004 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

From 610e58f8168560c77662d628cfdffb01b6e39aac Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 10 Mar 2025 18:18:17 +0000
Subject: [PATCH 02/13] optimize imports

---
 .../anodyne-maps.lagda.md                     | 41 +------------------
 1 file changed, 2 insertions(+), 39 deletions(-)

diff --git a/src/orthogonal-factorization-systems/anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md
index 62718f0af7..9a53d0201b 100644
--- a/src/orthogonal-factorization-systems/anodyne-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md
@@ -7,52 +7,15 @@ module orthogonal-factorization-systems.anodyne-maps where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.action-on-identifications-functions
-open import foundation.cartesian-morphisms-arrows
-open import foundation.cartesian-product-types
-open import foundation.composition-algebra
-open import foundation.contractible-maps
-open import foundation.contractible-types
-open import foundation.coproduct-types
-open import foundation.coproducts-pullbacks
-open import foundation.dependent-pair-types
-open import foundation.dependent-products-pullbacks
-open import foundation.dependent-sums-pullbacks
-open import foundation.equivalences
 open import foundation.equivalences-arrows
-open import foundation.fibered-maps
-open import foundation.fibers-of-maps
-open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-coproduct-types
 open import foundation.functoriality-dependent-pair-types
-open import foundation.functoriality-fibers-of-maps
 open import foundation.homotopies
-open import foundation.morphisms-arrows
-open import foundation.postcomposition-functions
-open import foundation.postcomposition-pullbacks
-open import foundation.precomposition-dependent-functions
-open import foundation.precomposition-functions
-open import foundation.products-pullbacks
-open import foundation.propositions
-open import foundation.pullbacks
-open import foundation.retracts-of-maps
-open import foundation.type-arithmetic-dependent-function-types
-open import foundation.type-theoretic-principle-of-choice
-open import foundation.unit-type
-open import foundation.universal-property-cartesian-product-types
-open import foundation.universal-property-coproduct-types
-open import foundation.universal-property-dependent-pair-types
-open import foundation.universal-property-equivalences
-open import foundation.universal-property-pullbacks
 open import foundation.universe-levels
-open import foundation.whiskering-homotopies-composition
 
-open import orthogonal-factorization-systems.lifting-structures-on-squares
 open import orthogonal-factorization-systems.orthogonal-maps
-open import orthogonal-factorization-systems.pullback-hom
-open import orthogonal-factorization-systems.types-local-at-maps
 
 open import synthetic-homotopy-theory.cocartesian-morphisms-arrows
 ```
@@ -63,8 +26,8 @@ open import synthetic-homotopy-theory.cocartesian-morphisms-arrows
 
 A map $j : C → D$ is said to be
 {{#concept "anodyne" Disambiguation="map of types" Agda=is-anodyne}} with
-respect to a map $f : A → B$, or **$f$-anodyne** if every map that is orthogonal
-to $f$ is also orthogonal to $j$.
+respect to a map $f : A → B$, or **$f$-anodyne**, if every map that is
+orthogonal to $f$ is also orthogonal to $j$.
 
 ## Definitions
 

From 122d55a9ff2ea864bfc54ca39894097ec39da7b6 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 11 Mar 2025 20:43:57 +0000
Subject: [PATCH 03/13] more universe polymorphism `descent-data-pushout`

---
 ...a-equivalence-types-over-pushouts.lagda.md | 25 +++----
 ...data-function-types-over-pushouts.lagda.md | 28 ++++----
 ...data-identity-types-over-pushouts.lagda.md |  4 +-
 .../descent-data-pushouts.lagda.md            | 16 ++---
 .../descent-property-pushouts.lagda.md        | 12 ++--
 ...quivalences-descent-data-pushouts.lagda.md | 47 ++++++------
 .../families-descent-data-pushouts.lagda.md   | 30 ++++----
 .../flattening-lemma-coequalizers.lagda.md    | 31 +++-----
 .../flattening-lemma-pushouts.lagda.md        | 37 +++++-----
 ...ity-systems-descent-data-pushouts.lagda.md | 43 +++++------
 .../morphisms-descent-data-pushouts.lagda.md  | 40 +++++------
 .../sections-descent-data-pushouts.lagda.md   | 28 ++++----
 .../universal-property-coequalizers.lagda.md  | 19 ++---
 .../universal-property-pushouts.lagda.md      | 71 +++++++++++++++++++
 14 files changed, 240 insertions(+), 191 deletions(-)

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 ac284b320a..122a5609cf 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..6390f307a1 100644
--- a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
@@ -69,11 +69,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 +83,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 :
@@ -140,7 +140,7 @@ module _
   where
 
   descent-data-family-cocone-span-diagram :
-    {l5 : Level} → (X → UU l5) → descent-data-pushout 𝒮 l5
+    {l5 : Level} → (X → UU l5) → descent-data-pushout 𝒮 l5 l5
   pr1 (descent-data-family-cocone-span-diagram P) =
     P ∘ horizontal-map-cocone _ _ c
   pr1 (pr2 (descent-data-family-cocone-span-diagram P)) =
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/equivalences-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
index a95a4a12a1..432be6953f 100644
--- a/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
@@ -76,12 +76,12 @@ 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 ≃
@@ -176,8 +176,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-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/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..829dc84267 100644
--- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md
@@ -154,8 +154,8 @@ 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 :
@@ -178,17 +178,18 @@ module _
       ( λ s → map-equiv (pr2 (pr2 P) s))
 
   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
@@ -354,10 +355,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
@@ -408,7 +410,7 @@ module _
     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,10 +419,10 @@ 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 (pr1 e ∘ f))
+        ( equiv-tot (pr1 e))
+        ( equiv-tot (pr1 (pr2 e)))
+        ( id-equiv)
         ( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e)
         ( refl-htpy)
         ( htpy-map-Σ
@@ -433,12 +435,5 @@ module _
         ( 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)
 ```
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..2924d7cd5e 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,16 @@ 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 +176,17 @@ 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}
+    {l : Level}
     (R :
       descent-data-pushout
-        ( span-diagram-flattening-descent-data-pushout P)
-        ( l5)) →
+        ( span-diagram-flattening-descent-data-pushout P) l l) →
     section (ev-refl-section-descent-data-pushout P p₀ R)
 ```
 
@@ -232,9 +232,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 +252,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 +260,7 @@ 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 +307,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 +340,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
@@ -348,7 +348,7 @@ assumption, so the right map has a section.
               ( family-cocone-family-with-descent-data-pushout P)
               ( inv-equiv-descent-data-family-with-descent-data-pushout P)
               ( up-c))
-            ( R)
+            (  R)
 ```
 
 ### The canonical descent data for families of identity types is an identity system
@@ -404,7 +404,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 +446,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,18 +481,19 @@ 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
 
   abstract
     is-identity-system-descent-data-pushout-ind-singleton :
       (H :
-        {l6 : Level}
+        {l7 : Level}
         (R :
           descent-data-pushout
             ( span-diagram-flattening-descent-data-pushout P)
-            ( l6))
+            l7
+            l7)
         (r₀ : left-family-descent-data-pushout R (a₀ , p₀)) →
         section-descent-data-pushout R) →
       is-identity-system-descent-data-pushout P p₀
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/sections-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/sections-descent-data-pushouts.lagda.md
index 583235db13..7b668de571 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)
 ```

From 124d929b31e3a8541498e1711a55d5cb2b6c7d8c Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 11 Mar 2025 20:44:21 +0000
Subject: [PATCH 04/13] more universe polymorphism `descent-data-pushout`

---
 .../identity-systems-descent-data-pushouts.lagda.md             | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 2924d7cd5e..c10b3c533a 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
@@ -348,7 +348,7 @@ assumption, so the right map has a section.
               ( family-cocone-family-with-descent-data-pushout P)
               ( inv-equiv-descent-data-family-with-descent-data-pushout P)
               ( up-c))
-            (  R)
+            ( R)
 ```
 
 ### The canonical descent data for families of identity types is an identity system

From 48e7ca8a644702ae7d06e27948de0cb0140e46b1 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 11 Mar 2025 20:44:58 +0000
Subject: [PATCH 05/13] lemmas `fiber'`

---
 src/foundation-core/fibers-of-maps.lagda.md   | 56 +++++++++++-
 src/foundation-core/pullbacks.lagda.md        | 89 +++++++++++++++++++
 src/foundation/fibers-of-maps.lagda.md        | 39 ++++++++
 .../functoriality-fibers-of-maps.lagda.md     | 53 +++++++++++
 4 files changed, 234 insertions(+), 3 deletions(-)

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/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 5beb6de9e9..b27b46aa09 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'`

From 05b822709b16079d1b27fa56fc42213ea31f08ce Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 11 Mar 2025 22:16:56 +0000
Subject: [PATCH 06/13] weakly anodyne maps

---
 src/orthogonal-factorization-systems.lagda.md |  1 +
 .../maps-local-at-maps.lagda.md               | 13 +++
 .../weakly-anodyne-maps.lagda.md              | 89 +++++++++++++++++++
 3 files changed, 103 insertions(+)
 create mode 100644 src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md

diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index a05161db66..e2a8bf7286 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -72,6 +72,7 @@ open import orthogonal-factorization-systems.types-local-at-maps public
 open import orthogonal-factorization-systems.types-separated-at-maps public
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities public
 open import orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses public
+open import orthogonal-factorization-systems.weakly-anodyne-maps public
 open import orthogonal-factorization-systems.wide-function-classes public
 open import orthogonal-factorization-systems.wide-global-function-classes public
 open import orthogonal-factorization-systems.zero-modality public
diff --git a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md
index ac69503101..921e0c45d7 100644
--- a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md
@@ -147,6 +147,19 @@ module _
       ( G (map-codomain-inclusion-retract-map g' g R d))
 ```
 
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6}
+  {f : A → B} {g : C → D} {f' : E → F}
+  where
+
+  is-local-retract-map' :
+    is-local-map f g → f' retract-of-map f → is-local-map f' g
+  is-local-retract-map' F R d =
+    is-local-retract-map-is-local f' f R (fiber g d) (F d)
+```
+
 ## See also
 
 - [Localizations with respect to maps](orthogonal-factorization-systems.localizations-at-maps.md)
diff --git a/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md
new file mode 100644
index 0000000000..c057f9195d
--- /dev/null
+++ b/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md
@@ -0,0 +1,89 @@
+# Weakly anodyne maps
+
+```agda
+module orthogonal-factorization-systems.weakly-anodyne-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.equivalences-arrows
+open import foundation.fibers-of-maps
+open import foundation.function-types
+open import foundation.functoriality-cartesian-product-types
+open import foundation.functoriality-coproduct-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.retracts-of-maps
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import orthogonal-factorization-systems.anodyne-maps
+open import orthogonal-factorization-systems.maps-local-at-maps
+open import orthogonal-factorization-systems.orthogonal-maps
+open import orthogonal-factorization-systems.types-local-at-maps
+
+open import synthetic-homotopy-theory.cocartesian-morphisms-arrows
+```
+
+</details>
+
+## Idea
+
+A map $j : C → D$ is said to be
+{{#concept "weakly anodyne" Disambiguation="map of types" Agda=is-weakly-anodyne}}
+with respect to a map $f : A → B$, or **weakly $f$-anodyne**, if every map that
+is local at $f$ is also local at $j$.
+
+## Definitions
+
+### The predicate of being weakly anodyne with respect to a map
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  (f : A → B) (j : C → D)
+  where
+
+  is-weakly-anodyne-Level :
+    (l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6)
+  is-weakly-anodyne-Level l5 l6 =
+    {X : UU l5} {Y : UU l6} (g : X → Y) → is-local-map f g → is-local-map j g
+
+  is-weakly-anodyne : UUω
+  is-weakly-anodyne = {l5 l6 : Level} → is-weakly-anodyne-Level l5 l6
+```
+
+## Properties
+
+### Anodyne maps are weakly anodyne
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  (f : A → B) {j : C → D}
+  where
+
+  is-weakly-anodyne-is-anodyne : is-anodyne f j → is-weakly-anodyne f j
+  is-weakly-anodyne-is-anodyne J g G x =
+    is-local-is-orthogonal-terminal-map j
+      ( J ( terminal-map (fiber g x))
+          ( is-orthogonal-terminal-map-is-local f (G x)))
+```
+
+### Weakly anodyne maps are closed under retracts of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {C' : UU l5} {D' : UU l6}
+  (f : A → B) {j : C → D} {j' : C' → D'}
+  where
+
+  is-weakly-anodyne-retract-map :
+    retract-map j j' → is-weakly-anodyne f j → is-weakly-anodyne f j'
+  is-weakly-anodyne-retract-map α J g G x =
+    is-local-retract-map-is-local j' j α (fiber g x) (J g G x)
+```

From 67d0c275387608e446f652909ad50a8c80d9493d Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 12 Mar 2025 12:16:17 +0000
Subject: [PATCH 07/13] edits Postcomposition of pullbacks

---
 .../postcomposition-pullbacks.lagda.md        | 68 +++++++++----------
 ...ype-arithmetic-standard-pullbacks.lagda.md |  6 +-
 2 files changed, 36 insertions(+), 38 deletions(-)

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 _

From beb79248b24a056b7da03eb8d7e318a63f14851e Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 12 Mar 2025 13:58:28 +0000
Subject: [PATCH 08/13] "symmetric" descent data pushouts

---
 .../descent-data-pushouts.lagda.md            | 154 +++++++++++-
 ...quivalences-descent-data-pushouts.lagda.md | 220 +++++++++++++++++-
 2 files changed, 361 insertions(+), 13 deletions(-)

diff --git a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
index 6390f307a1..5df9f42d62 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
@@ -113,6 +114,140 @@ module _
     is-equiv-map-equiv (equiv-family-descent-data-pushout s)
 ```
 
+### Symmetric descent data for pushouts
+
+We give another equivalent definition of descent data for pushouts, that records
+an additional type family `PS` over the spanning type `S` and equivalences
+`PS s ≃ PA (f s)` and `PS s ≃ PB (g s)` for all `s`.
+
+```agda
+module _
+  {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3)
+  where
+
+  symmetric-descent-data-pushout :
+    (l4 l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4 ⊔ lsuc l5 ⊔ lsuc l6)
+  symmetric-descent-data-pushout 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 symmetric descent data for pushouts
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : symmetric-descent-data-pushout 𝒮 l4 l5 l6)
+  where
+
+  left-family-symmetric-descent-data-pushout : domain-span-diagram 𝒮 → UU l4
+  left-family-symmetric-descent-data-pushout = pr1 P
+
+  right-family-symmetric-descent-data-pushout : codomain-span-diagram 𝒮 → UU l5
+  right-family-symmetric-descent-data-pushout = pr1 (pr2 P)
+
+  spanning-type-family-symmetric-descent-data-pushout :
+    spanning-type-span-diagram 𝒮 → UU l6
+  spanning-type-family-symmetric-descent-data-pushout = pr1 (pr2 (pr2 P))
+
+  equiv-left-family-symmetric-descent-data-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    spanning-type-family-symmetric-descent-data-pushout s ≃
+    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s)
+  equiv-left-family-symmetric-descent-data-pushout = pr1 (pr2 (pr2 (pr2 P)))
+
+  equiv-right-family-symmetric-descent-data-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    spanning-type-family-symmetric-descent-data-pushout s ≃
+    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s)
+  equiv-right-family-symmetric-descent-data-pushout = pr2 (pr2 (pr2 (pr2 P)))
+
+  map-left-family-symmetric-descent-data-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    spanning-type-family-symmetric-descent-data-pushout s →
+    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s)
+  map-left-family-symmetric-descent-data-pushout =
+    map-equiv ∘ equiv-left-family-symmetric-descent-data-pushout
+
+  map-right-family-symmetric-descent-data-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    spanning-type-family-symmetric-descent-data-pushout s →
+    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s)
+  map-right-family-symmetric-descent-data-pushout =
+    map-equiv ∘ equiv-right-family-symmetric-descent-data-pushout
+
+  map-inv-left-family-symmetric-descent-data-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) →
+    spanning-type-family-symmetric-descent-data-pushout s
+  map-inv-left-family-symmetric-descent-data-pushout =
+    map-inv-equiv ∘ equiv-left-family-symmetric-descent-data-pushout
+
+  map-inv-right-family-symmetric-descent-data-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) →
+    spanning-type-family-symmetric-descent-data-pushout s
+  map-inv-right-family-symmetric-descent-data-pushout =
+    map-inv-equiv ∘ equiv-right-family-symmetric-descent-data-pushout
+
+  is-equiv-map-left-family-symmetric-descent-data-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    is-equiv (map-left-family-symmetric-descent-data-pushout s)
+  is-equiv-map-left-family-symmetric-descent-data-pushout s =
+    is-equiv-map-equiv (equiv-left-family-symmetric-descent-data-pushout s)
+
+  is-equiv-map-right-family-symmetric-descent-data-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    is-equiv (map-right-family-symmetric-descent-data-pushout s)
+  is-equiv-map-right-family-symmetric-descent-data-pushout s =
+    is-equiv-map-equiv (equiv-right-family-symmetric-descent-data-pushout s)
+
+  equiv-left-right-family-symmetric-descent-data-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) ≃
+    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s)
+  equiv-left-right-family-symmetric-descent-data-pushout s =
+    equiv-right-family-symmetric-descent-data-pushout s ∘e
+    inv-equiv (equiv-left-family-symmetric-descent-data-pushout s)
+
+  map-left-right-family-symmetric-descent-data-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) →
+    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s)
+  map-left-right-family-symmetric-descent-data-pushout =
+    map-equiv ∘ equiv-left-right-family-symmetric-descent-data-pushout
+
+  equiv-right-left-family-symmetric-descent-data-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) ≃
+    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s)
+  equiv-right-left-family-symmetric-descent-data-pushout s =
+    equiv-left-family-symmetric-descent-data-pushout s ∘e
+    inv-equiv (equiv-right-family-symmetric-descent-data-pushout s)
+
+  map-right-left-family-symmetric-descent-data-pushout :
+    (s : spanning-type-span-diagram 𝒮) →
+    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) →
+    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s)
+  map-right-left-family-symmetric-descent-data-pushout =
+    map-equiv ∘ equiv-right-left-family-symmetric-descent-data-pushout
+
+  descent-data-pushout-symmetric-descent-data-pushout :
+    descent-data-pushout 𝒮 l4 l5
+  descent-data-pushout-symmetric-descent-data-pushout =
+    ( left-family-symmetric-descent-data-pushout ,
+      right-family-symmetric-descent-data-pushout ,
+      equiv-left-right-family-symmetric-descent-data-pushout)
+```
+
 ### Descent data induced by families over cocones
 
 Given a [cocone](synthetic-homotopy-theory.cocones-under-spans.md)
@@ -141,10 +276,17 @@ module _
 
   descent-data-family-cocone-span-diagram :
     {l5 : Level} → (X → UU l5) → descent-data-pushout 𝒮 l5 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)
+  descent-data-family-cocone-span-diagram P =
+    ( P ∘ horizontal-map-cocone _ _ c) ,
+    ( P ∘ vertical-map-cocone _ _ c) ,
+    ( equiv-tr P ∘ coherence-square-cocone _ _ c)
+
+  symmetric-descent-data-family-cocone-span-diagram :
+    {l5 : Level} → (X → UU l5) → symmetric-descent-data-pushout 𝒮 l5 l5 l5
+  symmetric-descent-data-family-cocone-span-diagram P =
+    ( P ∘ horizontal-map-cocone _ _ c) ,
+    ( P ∘ vertical-map-cocone _ _ c) ,
+    ( P ∘ horizontal-map-cocone _ _ c ∘ left-map-span-diagram 𝒮) ,
+    ( λ _ → id-equiv) ,
+    ( equiv-tr P ∘ coherence-square-cocone _ _ c)
 ```
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 432be6953f..2b126bbbb2 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,7 +77,8 @@ the proofs of `is-equiv` of their gluing maps.
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {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
@@ -164,12 +166,216 @@ 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)
+```
+
+### Equivalences of symmetric descent data for pushouts
+
+Note that the descent data arguments cannot be inferred when calling
+`left-equiv-equiv-descent-data-pushout` and the like, since Agda cannot infer
+the proofs of `is-equiv` of their gluing maps.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level}
+  {𝒮 : span-diagram l1 l2 l3}
+  (P : symmetric-descent-data-pushout 𝒮 l4 l5 l6)
+  (Q : symmetric-descent-data-pushout 𝒮 l7 l8 l9)
+  where
+
+  equiv-symmetric-descent-data-pushout :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7 ⊔ l8 ⊔ l9)
+  equiv-symmetric-descent-data-pushout =
+    Σ ( (a : domain-span-diagram 𝒮) →
+        left-family-symmetric-descent-data-pushout P a ≃
+        left-family-symmetric-descent-data-pushout Q a)
+      ( λ eA →
+        Σ ( (b : codomain-span-diagram 𝒮) →
+            right-family-symmetric-descent-data-pushout P b ≃
+            right-family-symmetric-descent-data-pushout Q b)
+          ( λ eB →
+            Σ ( (s : spanning-type-span-diagram 𝒮) →
+                spanning-type-family-symmetric-descent-data-pushout P s ≃
+                spanning-type-family-symmetric-descent-data-pushout Q s)
+              ( λ eS →
+                ( (s : spanning-type-span-diagram 𝒮) →
+                  coherence-square-maps
+                    ( map-equiv (eS s))
+                    ( map-left-family-symmetric-descent-data-pushout P s)
+                    ( map-left-family-symmetric-descent-data-pushout 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-symmetric-descent-data-pushout P s)
+                    ( map-right-family-symmetric-descent-data-pushout Q s)
+                    ( map-equiv (eB (right-map-span-diagram 𝒮 s)))))))
+
+  module _
+    (e : equiv-symmetric-descent-data-pushout)
+    where
+
+    left-equiv-equiv-symmetric-descent-data-pushout :
+      (a : domain-span-diagram 𝒮) →
+      left-family-symmetric-descent-data-pushout P a ≃
+      left-family-symmetric-descent-data-pushout Q a
+    left-equiv-equiv-symmetric-descent-data-pushout = pr1 e
+
+    left-map-equiv-symmetric-descent-data-pushout :
+      (a : domain-span-diagram 𝒮) →
+      left-family-symmetric-descent-data-pushout P a →
+      left-family-symmetric-descent-data-pushout Q a
+    left-map-equiv-symmetric-descent-data-pushout a =
+      map-equiv (left-equiv-equiv-symmetric-descent-data-pushout a)
+
+    is-equiv-left-map-equiv-symmetric-descent-data-pushout :
+      (a : domain-span-diagram 𝒮) →
+      is-equiv (left-map-equiv-symmetric-descent-data-pushout a)
+    is-equiv-left-map-equiv-symmetric-descent-data-pushout a =
+      is-equiv-map-equiv (left-equiv-equiv-symmetric-descent-data-pushout a)
+
+    inv-left-map-equiv-symmetric-descent-data-pushout :
+      (a : domain-span-diagram 𝒮) →
+      left-family-symmetric-descent-data-pushout Q a →
+      left-family-symmetric-descent-data-pushout P a
+    inv-left-map-equiv-symmetric-descent-data-pushout a =
+      map-inv-equiv (left-equiv-equiv-symmetric-descent-data-pushout a)
+
+    right-equiv-equiv-symmetric-descent-data-pushout :
+      (b : codomain-span-diagram 𝒮) →
+      right-family-symmetric-descent-data-pushout P b ≃
+      right-family-symmetric-descent-data-pushout Q b
+    right-equiv-equiv-symmetric-descent-data-pushout = pr1 (pr2 e)
+
+    right-map-equiv-symmetric-descent-data-pushout :
+      (b : codomain-span-diagram 𝒮) →
+      right-family-symmetric-descent-data-pushout P b →
+      right-family-symmetric-descent-data-pushout Q b
+    right-map-equiv-symmetric-descent-data-pushout b =
+      map-equiv (right-equiv-equiv-symmetric-descent-data-pushout b)
+
+    is-equiv-right-map-equiv-symmetric-descent-data-pushout :
+      (b : codomain-span-diagram 𝒮) →
+      is-equiv (right-map-equiv-symmetric-descent-data-pushout b)
+    is-equiv-right-map-equiv-symmetric-descent-data-pushout b =
+      is-equiv-map-equiv (right-equiv-equiv-symmetric-descent-data-pushout b)
+
+    inv-right-map-equiv-symmetric-descent-data-pushout :
+      (b : codomain-span-diagram 𝒮) →
+      right-family-symmetric-descent-data-pushout Q b →
+      right-family-symmetric-descent-data-pushout P b
+    inv-right-map-equiv-symmetric-descent-data-pushout b =
+      map-inv-equiv (right-equiv-equiv-symmetric-descent-data-pushout b)
+
+    spanning-type-equiv-equiv-symmetric-descent-data-pushout :
+      (b : spanning-type-span-diagram 𝒮) →
+      spanning-type-family-symmetric-descent-data-pushout P b ≃
+      spanning-type-family-symmetric-descent-data-pushout Q b
+    spanning-type-equiv-equiv-symmetric-descent-data-pushout = pr1 (pr2 (pr2 e))
+
+    spanning-type-map-equiv-symmetric-descent-data-pushout :
+      (b : spanning-type-span-diagram 𝒮) →
+      spanning-type-family-symmetric-descent-data-pushout P b →
+      spanning-type-family-symmetric-descent-data-pushout Q b
+    spanning-type-map-equiv-symmetric-descent-data-pushout b =
+      map-equiv (spanning-type-equiv-equiv-symmetric-descent-data-pushout b)
+
+    is-equiv-spanning-type-map-equiv-symmetric-descent-data-pushout :
+      (b : spanning-type-span-diagram 𝒮) →
+      is-equiv (spanning-type-map-equiv-symmetric-descent-data-pushout b)
+    is-equiv-spanning-type-map-equiv-symmetric-descent-data-pushout b =
+      is-equiv-map-equiv
+        ( spanning-type-equiv-equiv-symmetric-descent-data-pushout b)
+
+    inv-spanning-type-map-equiv-symmetric-descent-data-pushout :
+      (b : spanning-type-span-diagram 𝒮) →
+      spanning-type-family-symmetric-descent-data-pushout Q b →
+      spanning-type-family-symmetric-descent-data-pushout P b
+    inv-spanning-type-map-equiv-symmetric-descent-data-pushout b =
+      map-inv-equiv (spanning-type-equiv-equiv-symmetric-descent-data-pushout b)
+
+    coherence-left-equiv-symmetric-descent-data-pushout :
+      (s : spanning-type-span-diagram 𝒮) →
+      coherence-square-maps
+        ( spanning-type-map-equiv-symmetric-descent-data-pushout s)
+        ( map-left-family-symmetric-descent-data-pushout P s)
+        ( map-left-family-symmetric-descent-data-pushout Q s)
+        ( left-map-equiv-symmetric-descent-data-pushout
+          ( left-map-span-diagram 𝒮 s))
+    coherence-left-equiv-symmetric-descent-data-pushout =
+      pr1 (pr2 (pr2 (pr2 e)))
+
+    coherence-right-equiv-symmetric-descent-data-pushout :
+      (s : spanning-type-span-diagram 𝒮) →
+      coherence-square-maps
+        ( spanning-type-map-equiv-symmetric-descent-data-pushout s)
+        ( map-right-family-symmetric-descent-data-pushout P s)
+        ( map-right-family-symmetric-descent-data-pushout Q s)
+        ( right-map-equiv-symmetric-descent-data-pushout
+          ( right-map-span-diagram 𝒮 s))
+    coherence-right-equiv-symmetric-descent-data-pushout =
+      pr2 (pr2 (pr2 (pr2 e)))
+
+    coherence-left-right-equiv-symmetric-descent-data-pushout :
+      (s : spanning-type-span-diagram 𝒮) →
+      coherence-square-maps
+        ( left-map-equiv-symmetric-descent-data-pushout
+          ( left-map-span-diagram 𝒮 s))
+        ( map-left-right-family-symmetric-descent-data-pushout P s)
+        ( map-left-right-family-symmetric-descent-data-pushout Q s)
+        ( right-map-equiv-symmetric-descent-data-pushout
+          ( right-map-span-diagram 𝒮 s))
+    coherence-left-right-equiv-symmetric-descent-data-pushout s =
+      pasting-vertical-coherence-square-maps
+        ( left-map-equiv-symmetric-descent-data-pushout
+          ( left-map-span-diagram 𝒮 s))
+        ( map-inv-left-family-symmetric-descent-data-pushout P s)
+        ( map-inv-left-family-symmetric-descent-data-pushout Q s)
+        ( spanning-type-map-equiv-symmetric-descent-data-pushout s)
+        ( map-right-family-symmetric-descent-data-pushout P s)
+        ( map-right-family-symmetric-descent-data-pushout Q s)
+        ( right-map-equiv-symmetric-descent-data-pushout
+          ( right-map-span-diagram 𝒮 s))
+        (vertical-inv-equiv-coherence-square-maps
+          ( spanning-type-map-equiv-symmetric-descent-data-pushout s)
+          ( equiv-left-family-symmetric-descent-data-pushout P s)
+          ( equiv-left-family-symmetric-descent-data-pushout Q s)
+          ( left-map-equiv-symmetric-descent-data-pushout
+            ( left-map-span-diagram 𝒮 s))
+          ( coherence-left-equiv-symmetric-descent-data-pushout s))
+        ( coherence-right-equiv-symmetric-descent-data-pushout s)
+
+    coherence-right-left-equiv-symmetric-descent-data-pushout :
+      (s : spanning-type-span-diagram 𝒮) →
+      coherence-square-maps
+        ( right-map-equiv-symmetric-descent-data-pushout
+          ( right-map-span-diagram 𝒮 s))
+        ( map-right-left-family-symmetric-descent-data-pushout P s)
+        ( map-right-left-family-symmetric-descent-data-pushout Q s)
+        ( left-map-equiv-symmetric-descent-data-pushout
+          ( left-map-span-diagram 𝒮 s))
+    coherence-right-left-equiv-symmetric-descent-data-pushout s =
+      pasting-vertical-coherence-square-maps
+        ( right-map-equiv-symmetric-descent-data-pushout
+          ( right-map-span-diagram 𝒮 s))
+        ( map-inv-right-family-symmetric-descent-data-pushout P s)
+        ( map-inv-right-family-symmetric-descent-data-pushout Q s)
+        ( spanning-type-map-equiv-symmetric-descent-data-pushout s)
+        ( map-left-family-symmetric-descent-data-pushout P s)
+        ( map-left-family-symmetric-descent-data-pushout Q s)
+        ( left-map-equiv-symmetric-descent-data-pushout
+          ( left-map-span-diagram 𝒮 s))
+        (vertical-inv-equiv-coherence-square-maps
+          ( spanning-type-map-equiv-symmetric-descent-data-pushout s)
+          ( equiv-right-family-symmetric-descent-data-pushout P s)
+          ( equiv-right-family-symmetric-descent-data-pushout Q s)
+          ( right-map-equiv-symmetric-descent-data-pushout
+            ( right-map-span-diagram 𝒮 s))
+          ( coherence-right-equiv-symmetric-descent-data-pushout s))
+        ( coherence-left-equiv-symmetric-descent-data-pushout s)
 ```
 
 ### The identity equivalence of descent data for pushouts

From 05396ddf1784c910adbabe6570ab71efc6e1c4a5 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 12 Mar 2025 14:08:15 +0000
Subject: [PATCH 09/13] Revert "lemmas `fiber'`"

This reverts commit 48e7ca8a644702ae7d06e27948de0cb0140e46b1.
---
 src/foundation-core/fibers-of-maps.lagda.md   | 56 +-----------
 src/foundation-core/pullbacks.lagda.md        | 89 -------------------
 src/foundation/fibers-of-maps.lagda.md        | 39 --------
 .../functoriality-fibers-of-maps.lagda.md     | 53 -----------
 4 files changed, 3 insertions(+), 234 deletions(-)

diff --git a/src/foundation-core/fibers-of-maps.lagda.md b/src/foundation-core/fibers-of-maps.lagda.md
index 0376de9e04..12a441cd2d 100644
--- a/src/foundation-core/fibers-of-maps.lagda.md
+++ b/src/foundation-core/fibers-of-maps.lagda.md
@@ -52,13 +52,6 @@ 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
@@ -287,7 +280,9 @@ module _
   triangle-map-equiv-total-fiber t = inv (pr2 (pr2 t))
 
   map-inv-equiv-total-fiber : A → Σ B (fiber f)
-  map-inv-equiv-total-fiber x = (f x , x , refl)
+  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
 
   is-retraction-map-inv-equiv-total-fiber :
     is-retraction map-equiv-total-fiber map-inv-equiv-total-fiber
@@ -321,51 +316,6 @@ 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 0170c208fc..332e6e96e2 100644
--- a/src/foundation-core/pullbacks.lagda.md
+++ b/src/foundation-core/pullbacks.lagda.md
@@ -309,86 +309,6 @@ 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}
@@ -436,15 +356,6 @@ 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/fibers-of-maps.lagda.md b/src/foundation/fibers-of-maps.lagda.md
index c6205c190d..01e4a3f77b 100644
--- a/src/foundation/fibers-of-maps.lagda.md
+++ b/src/foundation/fibers-of-maps.lagda.md
@@ -141,45 +141,6 @@ 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 b27b46aa09..5beb6de9e9 100644
--- a/src/foundation/functoriality-fibers-of-maps.lagda.md
+++ b/src/foundation/functoriality-fibers-of-maps.lagda.md
@@ -103,41 +103,6 @@ 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
@@ -156,15 +121,6 @@ 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
@@ -183,15 +139,6 @@ 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'`

From 5f66950a08b88a371ef74ec61c9ea465cf8c4a64 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 12 Mar 2025 14:08:21 +0000
Subject: [PATCH 10/13] Revert "more universe polymorphism
 `descent-data-pushout`"

This reverts commit 124d929b31e3a8541498e1711a55d5cb2b6c7d8c.
---
 .../identity-systems-descent-data-pushouts.lagda.md             | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 c10b3c533a..2924d7cd5e 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
@@ -348,7 +348,7 @@ assumption, so the right map has a section.
               ( family-cocone-family-with-descent-data-pushout P)
               ( inv-equiv-descent-data-family-with-descent-data-pushout P)
               ( up-c))
-            ( R)
+            (  R)
 ```
 
 ### The canonical descent data for families of identity types is an identity system

From 7eb32578178a7176aff882cff45ea7dde4b59599 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 12 Mar 2025 14:08:58 +0000
Subject: [PATCH 11/13] Revert "more universe polymorphism
 `descent-data-pushout`"

This reverts commit 122d55a9ff2ea864bfc54ca39894097ec39da7b6.
---
 ...a-equivalence-types-over-pushouts.lagda.md | 25 ++++---
 ...data-function-types-over-pushouts.lagda.md | 28 ++++----
 ...data-identity-types-over-pushouts.lagda.md |  4 +-
 .../descent-data-pushouts.lagda.md            | 35 ++++-----
 .../descent-property-pushouts.lagda.md        | 12 ++--
 ...quivalences-descent-data-pushouts.lagda.md | 48 ++++++-------
 .../families-descent-data-pushouts.lagda.md   | 30 ++++----
 .../flattening-lemma-coequalizers.lagda.md    | 31 +++++---
 .../flattening-lemma-pushouts.lagda.md        | 37 +++++-----
 ...ity-systems-descent-data-pushouts.lagda.md | 43 ++++++-----
 .../morphisms-descent-data-pushouts.lagda.md  | 40 +++++------
 .../sections-descent-data-pushouts.lagda.md   | 28 ++++----
 .../universal-property-coequalizers.lagda.md  | 19 +++--
 .../universal-property-pushouts.lagda.md      | 71 -------------------
 14 files changed, 197 insertions(+), 254 deletions(-)

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 ebea5fa249..7095433e23 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,19 +60,18 @@ for [pushouts](synthetic-homotopy-theory.pushouts.md) `P ≈ (PA, PB, PS)` and
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
-  (P : family-with-descent-data-pushout c l5 l6 l7)
-  (R : family-with-descent-data-pushout c l8 l9 l10)
+  (P : family-with-descent-data-pushout c l5)
+  (R : family-with-descent-data-pushout c l6)
   where
 
-  family-cocone-equivalence-type-pushout : X → UU (l7 ⊔ l10)
+  family-cocone-equivalence-type-pushout : X → UU (l5 ⊔ l6)
   family-cocone-equivalence-type-pushout x =
     family-cocone-family-with-descent-data-pushout P x ≃
     family-cocone-family-with-descent-data-pushout R x
 
-  descent-data-equivalence-type-pushout :
-    descent-data-pushout 𝒮 (l5 ⊔ l8) (l6 ⊔ l9)
+  descent-data-equivalence-type-pushout : descent-data-pushout 𝒮 (l5 ⊔ l6)
   pr1 descent-data-equivalence-type-pushout a =
     left-family-family-with-descent-data-pushout P a ≃
     left-family-family-with-descent-data-pushout R a
@@ -170,7 +169,7 @@ module _
     coherence-equiv-descent-data-equivalence-type-pushout
 
   family-with-descent-data-equivalence-type-pushout :
-    family-with-descent-data-pushout c (l5 ⊔ l8) (l6 ⊔ l9) (l7 ⊔ l10)
+    family-with-descent-data-pushout c (l5 ⊔ l6)
   pr1 family-with-descent-data-equivalence-type-pushout =
     family-cocone-equivalence-type-pushout
   pr1 (pr2 family-with-descent-data-equivalence-type-pushout) =
@@ -185,10 +184,10 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
-  (P : family-with-descent-data-pushout c l5 l6 l7)
-  (R : family-with-descent-data-pushout c l8 l9 l10)
+  (P : family-with-descent-data-pushout c l5)
+  (R : family-with-descent-data-pushout c l6)
   where
 
   equiv-section-descent-data-equivalence-type-pushout :
@@ -289,11 +288,11 @@ by inverting the inverted equivalences.
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
   (up-c : universal-property-pushout _ _ c)
-  (P : family-with-descent-data-pushout c l5 l6 l7)
-  (R : family-with-descent-data-pushout c l8 l9 l10)
+  (P : family-with-descent-data-pushout c l5)
+  (R : family-with-descent-data-pushout c l6)
   (e :
     equiv-descent-data-pushout
       ( descent-data-family-with-descent-data-pushout P)
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 122a5609cf..ac284b320a 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,19 +102,18 @@ which we can massage into a coherence of the morphism as
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
-  (P : family-with-descent-data-pushout c l5 l6 l7)
-  (R : family-with-descent-data-pushout c l8 l9 l10)
+  (P : family-with-descent-data-pushout c l5)
+  (R : family-with-descent-data-pushout c l6)
   where
 
-  family-cocone-function-type-pushout : X → UU (l7 ⊔ l10)
+  family-cocone-function-type-pushout : X → UU (l5 ⊔ l6)
   family-cocone-function-type-pushout x =
     family-cocone-family-with-descent-data-pushout P x →
     family-cocone-family-with-descent-data-pushout R x
 
-  descent-data-function-type-pushout :
-    descent-data-pushout 𝒮 (l5 ⊔ l8) (l6 ⊔ l9)
+  descent-data-function-type-pushout : descent-data-pushout 𝒮 (l5 ⊔ l6)
   pr1 descent-data-function-type-pushout a =
     left-family-family-with-descent-data-pushout P a →
     left-family-family-with-descent-data-pushout R a
@@ -209,7 +208,7 @@ module _
     coherence-equiv-descent-data-function-type-pushout
 
   family-with-descent-data-function-type-pushout :
-    family-with-descent-data-pushout c (l5 ⊔ l8) (l6 ⊔ l9) (l7 ⊔ l10)
+    family-with-descent-data-pushout c (l5 ⊔ l6)
   pr1 family-with-descent-data-function-type-pushout =
     family-cocone-function-type-pushout
   pr1 (pr2 family-with-descent-data-function-type-pushout) =
@@ -224,10 +223,10 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
-  (P : family-with-descent-data-pushout c l5 l6 l7)
-  (R : family-with-descent-data-pushout c l8 l9 l10)
+  (P : family-with-descent-data-pushout c l5)
+  (R : family-with-descent-data-pushout c l6)
   where
 
   hom-section-descent-data-function-type-pushout :
@@ -251,7 +250,8 @@ 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 l7 l8 l9 l10 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
   (up-c : universal-property-pushout _ _ c)
-  (P : family-with-descent-data-pushout c l5 l6 l7)
-  (R : family-with-descent-data-pushout c l8 l9 l10)
+  (P : family-with-descent-data-pushout c l5)
+  (R : family-with-descent-data-pushout c l6)
   (m :
     hom-descent-data-pushout
       ( descent-data-family-with-descent-data-pushout P)
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 89d5e10cc6..6244d587ce 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 l4
+  descent-data-identity-type-pushout : descent-data-pushout 𝒮 l4
   pr1 descent-data-identity-type-pushout a =
     x₀ ＝ horizontal-map-cocone _ _ c a
   pr1 (pr2 descent-data-identity-type-pushout) b =
@@ -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 l4 l4
+    family-with-descent-data-pushout c l4
   pr1 family-with-descent-data-identity-type-pushout =
     family-cocone-identity-type-pushout
   pr1 (pr2 family-with-descent-data-identity-type-pushout) =
diff --git a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
index 5df9f42d62..ab3abf2750 100644
--- a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
@@ -70,11 +70,11 @@ module _
   {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3)
   where
 
-  descent-data-pushout : (l4 l5 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4 ⊔ lsuc l5)
-  descent-data-pushout l4 l5 =
-    Σ ( domain-span-diagram 𝒮 → UU l4)
+  descent-data-pushout : (l4 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4)
+  descent-data-pushout l =
+    Σ ( domain-span-diagram 𝒮 → UU l)
       ( λ PA →
-        Σ ( codomain-span-diagram 𝒮 → UU l5)
+        Σ ( codomain-span-diagram 𝒮 → UU l)
           ( λ PB →
             (s : spanning-type-span-diagram 𝒮) →
             PA (left-map-span-diagram 𝒮 s) ≃ PB (right-map-span-diagram 𝒮 s)))
@@ -84,14 +84,14 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5)
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
   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 l5
+  right-family-descent-data-pushout : codomain-span-diagram 𝒮 → UU l4
   right-family-descent-data-pushout = pr1 (pr2 P)
 
   equiv-family-descent-data-pushout :
@@ -275,18 +275,11 @@ module _
   where
 
   descent-data-family-cocone-span-diagram :
-    {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)
-
-  symmetric-descent-data-family-cocone-span-diagram :
-    {l5 : Level} → (X → UU l5) → symmetric-descent-data-pushout 𝒮 l5 l5 l5
-  symmetric-descent-data-family-cocone-span-diagram P =
-    ( P ∘ horizontal-map-cocone _ _ c) ,
-    ( P ∘ vertical-map-cocone _ _ c) ,
-    ( P ∘ horizontal-map-cocone _ _ c ∘ left-map-span-diagram 𝒮) ,
-    ( λ _ → id-equiv) ,
-    ( equiv-tr P ∘ coherence-square-cocone _ _ c)
+    {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)
 ```
diff --git a/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
index 5d8b09bc77..6d1f56638f 100644
--- a/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
@@ -120,16 +120,18 @@ module _
   equiv-descent-data-cocone-span-diagram-UU :
     (l4 : Level) →
     cocone-span-diagram 𝒮 (UU l4) ≃
-    descent-data-pushout 𝒮 l4 l4
+    descent-data-pushout 𝒮 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 l4
+    descent-data-pushout 𝒮 l4
   descent-data-cocone-span-diagram-UU {l4} =
     map-equiv (equiv-descent-data-cocone-span-diagram-UU l4)
 
@@ -174,7 +176,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 l5)
+  (P : descent-data-pushout 𝒮 l5)
   where
 
   abstract
@@ -291,7 +293,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 l5 l5
+    family-with-descent-data-pushout c 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/equivalences-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
index 2b126bbbb2..efcb51aae6 100644
--- a/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
@@ -77,13 +77,12 @@ the proofs of `is-equiv` of their gluing maps.
 
 ```agda
 module _
-  {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)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
+  (Q : descent-data-pushout 𝒮 l5)
   where
 
-  equiv-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7)
+  equiv-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
   equiv-descent-data-pushout =
     Σ ( (a : domain-span-diagram 𝒮) →
         left-family-descent-data-pushout P a ≃
@@ -382,8 +381,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5)
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
   where
 
   id-equiv-descent-data-pushout : equiv-descent-data-pushout P P
@@ -417,9 +416,9 @@ and mirroring the coherence squares vertically to get
 
 ```agda
 module _
-  {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)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
+  (Q : descent-data-pushout 𝒮 l5)
   where
 
   inv-equiv-descent-data-pushout :
@@ -442,14 +441,13 @@ module _
 
 ```agda
 module _
-  {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)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
+  (Q : descent-data-pushout 𝒮 l5)
   where
 
   htpy-equiv-descent-data-pushout :
-    (e f : equiv-descent-data-pushout P Q) →
-    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7)
+    (e f : equiv-descent-data-pushout P Q) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
   htpy-equiv-descent-data-pushout e f =
     htpy-hom-descent-data-pushout P Q
       ( hom-equiv-descent-data-pushout P Q e)
@@ -462,18 +460,18 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5)
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
   where
 
   equiv-eq-descent-data-pushout :
-    (Q : descent-data-pushout 𝒮 l4 l5) →
+    (Q : descent-data-pushout 𝒮 l4) →
     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 {l6 = l4} {l7 = l5} P)
+      is-torsorial (equiv-descent-data-pushout {l5 = l4} P)
     is-torsorial-equiv-descent-data-pushout =
       is-torsorial-Eq-structure
         ( is-torsorial-Eq-Π
@@ -488,7 +486,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 l5) →
+      (Q : descent-data-pushout 𝒮 l4) →
       is-equiv (equiv-eq-descent-data-pushout Q)
     is-equiv-equiv-eq-descent-data-pushout =
       fundamental-theorem-id
@@ -496,7 +494,7 @@ module _
         ( equiv-eq-descent-data-pushout)
 
   extensionality-descent-data-pushout :
-    (Q : descent-data-pushout 𝒮 l4 l5) →
+    (Q : descent-data-pushout 𝒮 l4) →
     (P ＝ Q) ≃ equiv-descent-data-pushout P Q
   pr1 (extensionality-descent-data-pushout Q) =
     equiv-eq-descent-data-pushout Q
@@ -504,7 +502,7 @@ module _
     is-equiv-equiv-eq-descent-data-pushout Q
 
   eq-equiv-descent-data-pushout :
-    (Q : descent-data-pushout 𝒮 l4 l5) →
+    (Q : descent-data-pushout 𝒮 l4) →
     equiv-descent-data-pushout P Q → P ＝ Q
   eq-equiv-descent-data-pushout Q =
     map-inv-equiv (extensionality-descent-data-pushout Q)
@@ -514,9 +512,9 @@ module _
 
 ```agda
 module _
-  {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}
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {P : descent-data-pushout 𝒮 l4}
+  {Q : descent-data-pushout 𝒮 l5}
   (e : equiv-descent-data-pushout P Q)
   where
 
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 62d678d3b2..0a68a9200c 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 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)
+    (l5 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5)
+  family-with-descent-data-pushout l5 =
+    Σ ( X → UU l5)
       ( λ P →
-        Σ ( descent-data-pushout 𝒮 l5 l6)
+        Σ ( descent-data-pushout 𝒮 l5)
           ( λ 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 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
-  (P : family-with-descent-data-pushout c l5 l6 l7)
+  (P : family-with-descent-data-pushout c l5)
   where
 
-  family-cocone-family-with-descent-data-pushout : X → UU l7
+  family-cocone-family-with-descent-data-pushout : X → UU l5
   family-cocone-family-with-descent-data-pushout = pr1 P
 
-  descent-data-family-with-descent-data-pushout : descent-data-pushout 𝒮 l5 l6
+  descent-data-family-with-descent-data-pushout : descent-data-pushout 𝒮 l5
   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 l6
+    codomain-span-diagram 𝒮 → UU l5
   right-family-family-with-descent-data-pushout =
     right-family-descent-data-pushout
       ( descent-data-family-with-descent-data-pushout)
@@ -224,7 +224,8 @@ 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
@@ -242,11 +243,12 @@ module _
   where
 
   family-with-descent-data-pushout-family-cocone :
-    {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
+    {l5 : Level} (P : X → UU l5) →
+    family-with-descent-data-pushout c l5
+  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 abddcc385a..552c91b146 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-equiv
+        ( universal-property-pushout-bottom-universal-property-pushout-top-cube-is-equiv
           ( vertical-map-span-cocone-cofork
             ( double-arrow-flattening-lemma-coequalizer a P e))
           ( horizontal-map-span-cocone-cofork
@@ -166,15 +166,16 @@ module _
             ( vertical-map-span-cocone-cofork a)
             ( horizontal-map-span-cocone-cofork a)
             ( cocone-codiagonal-cofork a e))
-          ( 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)
+          ( 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)
           ( coherence-square-cocone-flattening-pushout P
             ( vertical-map-span-cocone-cofork a)
             ( horizontal-map-span-cocone-cofork a)
@@ -190,6 +191,16 @@ 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 829dc84267..a5842aaa89 100644
--- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md
@@ -154,8 +154,8 @@ data for the pushout.
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5)
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
   where
 
   vertical-map-span-flattening-descent-data-pushout :
@@ -178,18 +178,17 @@ module _
       ( λ s → map-equiv (pr2 (pr2 P) s))
 
   span-diagram-flattening-descent-data-pushout :
-    span-diagram (l1 ⊔ l4) (l2 ⊔ l5) (l3 ⊔ l4)
+    span-diagram (l1 ⊔ l4) (l2 ⊔ l4) (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 l6 l7 : Level}
-  {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
+  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   ( f : S → A) (g : S → B) (c : cocone f g X)
-  ( P : descent-data-pushout (make-span-diagram f g) l5 l6)
-  ( Q : X → UU l7)
+  ( P : descent-data-pushout (make-span-diagram f g) l5)
+  ( Q : X → UU l5)
   ( e :
     equiv-descent-data-pushout P (descent-data-family-cocone-span-diagram c Q))
   where
@@ -355,11 +354,10 @@ descent data.
 
 ```agda
 module _
-  { l1 l2 l3 l4 l5 l6 l7 : Level}
-  { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
+  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
   ( f : S → A) (g : S → B) (c : cocone f g X)
-  ( P : descent-data-pushout (make-span-diagram f g) l5 l6)
-  ( Q : X → UU l7)
+  ( P : descent-data-pushout (make-span-diagram f g) l5)
+  ( Q : X → UU l5)
   ( e :
     equiv-descent-data-pushout P (descent-data-family-cocone-span-diagram c Q))
   where
@@ -410,7 +408,7 @@ module _
     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-equiv
+      universal-property-pushout-top-universal-property-pushout-bottom-cube-is-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)
@@ -419,10 +417,10 @@ 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)
-        ( equiv-tot (pr1 e ∘ f))
-        ( equiv-tot (pr1 e))
-        ( equiv-tot (pr1 (pr2 e)))
-        ( id-equiv)
+        ( tot (λ s → map-equiv (pr1 e (f s))))
+        ( tot (λ a → map-equiv (pr1 e a)))
+        ( tot (λ b → map-equiv (pr1 (pr2 e) b)))
+        ( id)
         ( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e)
         ( refl-htpy)
         ( htpy-map-Σ
@@ -435,5 +433,12 @@ module _
         ( 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)
 ```
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 2924d7cd5e..ed4ca2232d 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,16 +156,15 @@ section of `(RΣA, RΣB, RΣS)`, respectively.
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5) {a₀ : domain-span-diagram 𝒮}
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4) {a₀ : domain-span-diagram 𝒮}
   (p₀ : left-family-descent-data-pushout P a₀)
   where
 
   ev-refl-section-descent-data-pushout :
-    {l6 l7 : Level}
+    {l5 : Level}
     (R :
-      descent-data-pushout
-        ( span-diagram-flattening-descent-data-pushout P) l6 l7)
+      descent-data-pushout (span-diagram-flattening-descent-data-pushout P) l5)
     (t : section-descent-data-pushout R) →
     left-family-descent-data-pushout R (a₀ , p₀)
   ev-refl-section-descent-data-pushout R t =
@@ -176,17 +175,18 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5) {a₀ : domain-span-diagram 𝒮}
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4) {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 =
-    {l : Level}
+    {l5 : Level}
     (R :
       descent-data-pushout
-        ( span-diagram-flattening-descent-data-pushout P) l l) →
+        ( span-diagram-flattening-descent-data-pushout P)
+        ( l5)) →
     section (ev-refl-section-descent-data-pushout P p₀ R)
 ```
 
@@ -232,9 +232,9 @@ section if and only if the right map has a section.
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
-  (P : family-with-descent-data-pushout c l5 l6 l7)
+  (P : family-with-descent-data-pushout c l5)
   {a₀ : domain-span-diagram 𝒮}
   (p₀ : left-family-family-with-descent-data-pushout P a₀)
   where
@@ -252,7 +252,7 @@ module _
         ( inv-equiv-descent-data-family-with-descent-data-pushout P)
 
   square-ev-refl-section-descent-data-pushout :
-    {l5 l6 l7 : Level}
+    {l5 : Level}
     (R :
       family-with-descent-data-pushout
         ( cocone-flattening-descent-data-pushout _ _ c
@@ -260,7 +260,7 @@ module _
           ( family-cocone-family-with-descent-data-pushout P)
           ( inv-equiv-descent-data-pushout _ _
             ( equiv-descent-data-family-with-descent-data-pushout P)))
-        l5 l6 l7) →
+        ( l5)) →
     coherence-square-maps
       ( section-descent-data-section-family-cocone-span-diagram R ∘ ind-Σ)
       ( ev-refl-identity-system
@@ -307,7 +307,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 l l
+        fam-R : family-with-descent-data-pushout cocone-flattening l
         fam-R =
           family-with-descent-data-pushout-family-cocone
             ( cocone-flattening)
@@ -340,7 +340,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 l l
+        fam-R : family-with-descent-data-pushout cocone-flattening l
         fam-R =
           family-with-descent-data-pushout-descent-data-pushout
             ( flattening-lemma-descent-data-pushout _ _ c
@@ -348,7 +348,7 @@ assumption, so the right map has a section.
               ( family-cocone-family-with-descent-data-pushout P)
               ( inv-equiv-descent-data-family-with-descent-data-pushout P)
               ( up-c))
-            (  R)
+            ( R)
 ```
 
 ### The canonical descent data for families of identity types is an identity system
@@ -404,7 +404,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 l5) {a₀ : domain-span-diagram 𝒮}
+  (P : descent-data-pushout 𝒮 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 +446,7 @@ module _
               ( up-c)
               ( id-system-P))))
       where
-      fam-P : family-with-descent-data-pushout c l5 l5 l5
+      fam-P : family-with-descent-data-pushout c l5
       fam-P = family-with-descent-data-pushout-descent-data-pushout up-c P
       p₀' :
         family-cocone-family-with-descent-data-pushout
@@ -481,19 +481,18 @@ 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 l5) {a₀ : domain-span-diagram 𝒮}
+  (P : descent-data-pushout 𝒮 l5) {a₀ : domain-span-diagram 𝒮}
   (p₀ : left-family-descent-data-pushout P a₀)
   where
 
   abstract
     is-identity-system-descent-data-pushout-ind-singleton :
       (H :
-        {l7 : Level}
+        {l6 : Level}
         (R :
           descent-data-pushout
             ( span-diagram-flattening-descent-data-pushout P)
-            l7
-            l7)
+            ( l6))
         (r₀ : left-family-descent-data-pushout R (a₀ , p₀)) →
         section-descent-data-pushout R) →
       is-identity-system-descent-data-pushout P p₀
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 317bf3a29e..27f747d90f 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 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5)
-  (Q : descent-data-pushout 𝒮 l6 l7)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
+  (Q : descent-data-pushout 𝒮 l5)
   where
 
-  hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7)
+  hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
   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 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5)
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
   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 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)
+  {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)
   (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 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5)
-  (Q : descent-data-pushout 𝒮 l6 l7)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
+  (Q : descent-data-pushout 𝒮 l5)
   (f g : hom-descent-data-pushout P Q)
   where
 
-  htpy-hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7)
+  htpy-hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
   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 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5)
-  (Q : descent-data-pushout 𝒮 l6 l7)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
+  (Q : descent-data-pushout 𝒮 l5)
   (f : hom-descent-data-pushout P Q)
   where
 
@@ -271,9 +271,9 @@ module _
 
 ```agda
 module _
-  {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)
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
+  (Q : descent-data-pushout 𝒮 l5)
   (f : hom-descent-data-pushout P Q)
   where
 
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 7b668de571..583235db13 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 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5)
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
   where
 
-  section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
+  section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   section-descent-data-pushout =
     Σ ( (a : domain-span-diagram 𝒮) → left-family-descent-data-pushout P a)
       ( λ tA →
@@ -147,12 +147,12 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5)
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
   (r t : section-descent-data-pushout P)
   where
 
-  htpy-section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
+  htpy-section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   htpy-section-descent-data-pushout =
     Σ ( left-map-section-descent-data-pushout P r ~
         left-map-section-descent-data-pushout P t)
@@ -174,8 +174,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5)
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
   (r : section-descent-data-pushout P)
   where
 
@@ -192,8 +192,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : descent-data-pushout 𝒮 l4 l5)
+  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
+  (P : descent-data-pushout 𝒮 l4)
   (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 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
-  (P : family-with-descent-data-pushout c l5 l6 l7)
+  (P : family-with-descent-data-pushout c l5)
   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 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3}
+  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
   {X : UU l4} {c : cocone-span-diagram 𝒮 X}
   (up-c : universal-property-pushout _ _ c)
-  (P : family-with-descent-data-pushout c l5 l6 l7)
+  (P : family-with-descent-data-pushout c l5)
   (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 31d4fe2ff3..14abaccfc2 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-equiv
+      ( universal-property-pushout-top-universal-property-pushout-bottom-cube-is-equiv
         ( vertical-map-span-cocone-cofork a')
         ( horizontal-map-span-cocone-cofork a')
         ( horizontal-map-cocone-cofork a' c')
@@ -204,12 +204,11 @@ module _
         ( horizontal-map-span-cocone-cofork a)
         ( horizontal-map-cocone-cofork a c)
         ( vertical-map-cocone-cofork a c)
-        ( 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')
+        ( 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')
         ( coherence-square-cocone-cofork a c)
         ( inv-htpy
           ( left-square-hom-span-diagram-cofork-hom-double-arrow a a'
@@ -265,6 +264,12 @@ 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 2191989aef..06f4082d85 100644
--- a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md
@@ -998,75 +998,4 @@ 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)
 ```

From 5f2fcbde0bbbd411dc9eedfd1ff869d8c0a2c26a Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 12 Mar 2025 14:09:57 +0000
Subject: [PATCH 12/13] Revert ""symmetric" descent data pushouts"

This reverts commit beb79248b24a056b7da03eb8d7e318a63f14851e.
---
 .../descent-data-pushouts.lagda.md            | 135 -----------
 ...quivalences-descent-data-pushouts.lagda.md | 217 +-----------------
 2 files changed, 6 insertions(+), 346 deletions(-)

diff --git a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
index ab3abf2750..020d2dcefb 100644
--- a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
@@ -7,7 +7,6 @@ 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
@@ -114,140 +113,6 @@ module _
     is-equiv-map-equiv (equiv-family-descent-data-pushout s)
 ```
 
-### Symmetric descent data for pushouts
-
-We give another equivalent definition of descent data for pushouts, that records
-an additional type family `PS` over the spanning type `S` and equivalences
-`PS s ≃ PA (f s)` and `PS s ≃ PB (g s)` for all `s`.
-
-```agda
-module _
-  {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3)
-  where
-
-  symmetric-descent-data-pushout :
-    (l4 l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4 ⊔ lsuc l5 ⊔ lsuc l6)
-  symmetric-descent-data-pushout 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 symmetric descent data for pushouts
-
-```agda
-module _
-  {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
-  (P : symmetric-descent-data-pushout 𝒮 l4 l5 l6)
-  where
-
-  left-family-symmetric-descent-data-pushout : domain-span-diagram 𝒮 → UU l4
-  left-family-symmetric-descent-data-pushout = pr1 P
-
-  right-family-symmetric-descent-data-pushout : codomain-span-diagram 𝒮 → UU l5
-  right-family-symmetric-descent-data-pushout = pr1 (pr2 P)
-
-  spanning-type-family-symmetric-descent-data-pushout :
-    spanning-type-span-diagram 𝒮 → UU l6
-  spanning-type-family-symmetric-descent-data-pushout = pr1 (pr2 (pr2 P))
-
-  equiv-left-family-symmetric-descent-data-pushout :
-    (s : spanning-type-span-diagram 𝒮) →
-    spanning-type-family-symmetric-descent-data-pushout s ≃
-    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s)
-  equiv-left-family-symmetric-descent-data-pushout = pr1 (pr2 (pr2 (pr2 P)))
-
-  equiv-right-family-symmetric-descent-data-pushout :
-    (s : spanning-type-span-diagram 𝒮) →
-    spanning-type-family-symmetric-descent-data-pushout s ≃
-    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s)
-  equiv-right-family-symmetric-descent-data-pushout = pr2 (pr2 (pr2 (pr2 P)))
-
-  map-left-family-symmetric-descent-data-pushout :
-    (s : spanning-type-span-diagram 𝒮) →
-    spanning-type-family-symmetric-descent-data-pushout s →
-    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s)
-  map-left-family-symmetric-descent-data-pushout =
-    map-equiv ∘ equiv-left-family-symmetric-descent-data-pushout
-
-  map-right-family-symmetric-descent-data-pushout :
-    (s : spanning-type-span-diagram 𝒮) →
-    spanning-type-family-symmetric-descent-data-pushout s →
-    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s)
-  map-right-family-symmetric-descent-data-pushout =
-    map-equiv ∘ equiv-right-family-symmetric-descent-data-pushout
-
-  map-inv-left-family-symmetric-descent-data-pushout :
-    (s : spanning-type-span-diagram 𝒮) →
-    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) →
-    spanning-type-family-symmetric-descent-data-pushout s
-  map-inv-left-family-symmetric-descent-data-pushout =
-    map-inv-equiv ∘ equiv-left-family-symmetric-descent-data-pushout
-
-  map-inv-right-family-symmetric-descent-data-pushout :
-    (s : spanning-type-span-diagram 𝒮) →
-    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) →
-    spanning-type-family-symmetric-descent-data-pushout s
-  map-inv-right-family-symmetric-descent-data-pushout =
-    map-inv-equiv ∘ equiv-right-family-symmetric-descent-data-pushout
-
-  is-equiv-map-left-family-symmetric-descent-data-pushout :
-    (s : spanning-type-span-diagram 𝒮) →
-    is-equiv (map-left-family-symmetric-descent-data-pushout s)
-  is-equiv-map-left-family-symmetric-descent-data-pushout s =
-    is-equiv-map-equiv (equiv-left-family-symmetric-descent-data-pushout s)
-
-  is-equiv-map-right-family-symmetric-descent-data-pushout :
-    (s : spanning-type-span-diagram 𝒮) →
-    is-equiv (map-right-family-symmetric-descent-data-pushout s)
-  is-equiv-map-right-family-symmetric-descent-data-pushout s =
-    is-equiv-map-equiv (equiv-right-family-symmetric-descent-data-pushout s)
-
-  equiv-left-right-family-symmetric-descent-data-pushout :
-    (s : spanning-type-span-diagram 𝒮) →
-    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) ≃
-    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s)
-  equiv-left-right-family-symmetric-descent-data-pushout s =
-    equiv-right-family-symmetric-descent-data-pushout s ∘e
-    inv-equiv (equiv-left-family-symmetric-descent-data-pushout s)
-
-  map-left-right-family-symmetric-descent-data-pushout :
-    (s : spanning-type-span-diagram 𝒮) →
-    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) →
-    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s)
-  map-left-right-family-symmetric-descent-data-pushout =
-    map-equiv ∘ equiv-left-right-family-symmetric-descent-data-pushout
-
-  equiv-right-left-family-symmetric-descent-data-pushout :
-    (s : spanning-type-span-diagram 𝒮) →
-    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) ≃
-    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s)
-  equiv-right-left-family-symmetric-descent-data-pushout s =
-    equiv-left-family-symmetric-descent-data-pushout s ∘e
-    inv-equiv (equiv-right-family-symmetric-descent-data-pushout s)
-
-  map-right-left-family-symmetric-descent-data-pushout :
-    (s : spanning-type-span-diagram 𝒮) →
-    right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) →
-    left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s)
-  map-right-left-family-symmetric-descent-data-pushout =
-    map-equiv ∘ equiv-right-left-family-symmetric-descent-data-pushout
-
-  descent-data-pushout-symmetric-descent-data-pushout :
-    descent-data-pushout 𝒮 l4 l5
-  descent-data-pushout-symmetric-descent-data-pushout =
-    ( left-family-symmetric-descent-data-pushout ,
-      right-family-symmetric-descent-data-pushout ,
-      equiv-left-right-family-symmetric-descent-data-pushout)
-```
-
 ### Descent data induced by families over cocones
 
 Given a [cocone](synthetic-homotopy-theory.cocones-under-spans.md)
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 efcb51aae6..a95a4a12a1 100644
--- a/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md
@@ -7,7 +7,6 @@ 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
@@ -165,216 +164,12 @@ module _
     coherence-equiv-descent-data-pushout = pr2 (pr2 e)
 
     hom-equiv-descent-data-pushout : hom-descent-data-pushout P Q
-    hom-equiv-descent-data-pushout =
-      ( left-map-equiv-descent-data-pushout ,
-        right-map-equiv-descent-data-pushout ,
-        coherence-equiv-descent-data-pushout)
-```
-
-### Equivalences of symmetric descent data for pushouts
-
-Note that the descent data arguments cannot be inferred when calling
-`left-equiv-equiv-descent-data-pushout` and the like, since Agda cannot infer
-the proofs of `is-equiv` of their gluing maps.
-
-```agda
-module _
-  {l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level}
-  {𝒮 : span-diagram l1 l2 l3}
-  (P : symmetric-descent-data-pushout 𝒮 l4 l5 l6)
-  (Q : symmetric-descent-data-pushout 𝒮 l7 l8 l9)
-  where
-
-  equiv-symmetric-descent-data-pushout :
-    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7 ⊔ l8 ⊔ l9)
-  equiv-symmetric-descent-data-pushout =
-    Σ ( (a : domain-span-diagram 𝒮) →
-        left-family-symmetric-descent-data-pushout P a ≃
-        left-family-symmetric-descent-data-pushout Q a)
-      ( λ eA →
-        Σ ( (b : codomain-span-diagram 𝒮) →
-            right-family-symmetric-descent-data-pushout P b ≃
-            right-family-symmetric-descent-data-pushout Q b)
-          ( λ eB →
-            Σ ( (s : spanning-type-span-diagram 𝒮) →
-                spanning-type-family-symmetric-descent-data-pushout P s ≃
-                spanning-type-family-symmetric-descent-data-pushout Q s)
-              ( λ eS →
-                ( (s : spanning-type-span-diagram 𝒮) →
-                  coherence-square-maps
-                    ( map-equiv (eS s))
-                    ( map-left-family-symmetric-descent-data-pushout P s)
-                    ( map-left-family-symmetric-descent-data-pushout 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-symmetric-descent-data-pushout P s)
-                    ( map-right-family-symmetric-descent-data-pushout Q s)
-                    ( map-equiv (eB (right-map-span-diagram 𝒮 s)))))))
-
-  module _
-    (e : equiv-symmetric-descent-data-pushout)
-    where
-
-    left-equiv-equiv-symmetric-descent-data-pushout :
-      (a : domain-span-diagram 𝒮) →
-      left-family-symmetric-descent-data-pushout P a ≃
-      left-family-symmetric-descent-data-pushout Q a
-    left-equiv-equiv-symmetric-descent-data-pushout = pr1 e
-
-    left-map-equiv-symmetric-descent-data-pushout :
-      (a : domain-span-diagram 𝒮) →
-      left-family-symmetric-descent-data-pushout P a →
-      left-family-symmetric-descent-data-pushout Q a
-    left-map-equiv-symmetric-descent-data-pushout a =
-      map-equiv (left-equiv-equiv-symmetric-descent-data-pushout a)
-
-    is-equiv-left-map-equiv-symmetric-descent-data-pushout :
-      (a : domain-span-diagram 𝒮) →
-      is-equiv (left-map-equiv-symmetric-descent-data-pushout a)
-    is-equiv-left-map-equiv-symmetric-descent-data-pushout a =
-      is-equiv-map-equiv (left-equiv-equiv-symmetric-descent-data-pushout a)
-
-    inv-left-map-equiv-symmetric-descent-data-pushout :
-      (a : domain-span-diagram 𝒮) →
-      left-family-symmetric-descent-data-pushout Q a →
-      left-family-symmetric-descent-data-pushout P a
-    inv-left-map-equiv-symmetric-descent-data-pushout a =
-      map-inv-equiv (left-equiv-equiv-symmetric-descent-data-pushout a)
-
-    right-equiv-equiv-symmetric-descent-data-pushout :
-      (b : codomain-span-diagram 𝒮) →
-      right-family-symmetric-descent-data-pushout P b ≃
-      right-family-symmetric-descent-data-pushout Q b
-    right-equiv-equiv-symmetric-descent-data-pushout = pr1 (pr2 e)
-
-    right-map-equiv-symmetric-descent-data-pushout :
-      (b : codomain-span-diagram 𝒮) →
-      right-family-symmetric-descent-data-pushout P b →
-      right-family-symmetric-descent-data-pushout Q b
-    right-map-equiv-symmetric-descent-data-pushout b =
-      map-equiv (right-equiv-equiv-symmetric-descent-data-pushout b)
-
-    is-equiv-right-map-equiv-symmetric-descent-data-pushout :
-      (b : codomain-span-diagram 𝒮) →
-      is-equiv (right-map-equiv-symmetric-descent-data-pushout b)
-    is-equiv-right-map-equiv-symmetric-descent-data-pushout b =
-      is-equiv-map-equiv (right-equiv-equiv-symmetric-descent-data-pushout b)
-
-    inv-right-map-equiv-symmetric-descent-data-pushout :
-      (b : codomain-span-diagram 𝒮) →
-      right-family-symmetric-descent-data-pushout Q b →
-      right-family-symmetric-descent-data-pushout P b
-    inv-right-map-equiv-symmetric-descent-data-pushout b =
-      map-inv-equiv (right-equiv-equiv-symmetric-descent-data-pushout b)
-
-    spanning-type-equiv-equiv-symmetric-descent-data-pushout :
-      (b : spanning-type-span-diagram 𝒮) →
-      spanning-type-family-symmetric-descent-data-pushout P b ≃
-      spanning-type-family-symmetric-descent-data-pushout Q b
-    spanning-type-equiv-equiv-symmetric-descent-data-pushout = pr1 (pr2 (pr2 e))
-
-    spanning-type-map-equiv-symmetric-descent-data-pushout :
-      (b : spanning-type-span-diagram 𝒮) →
-      spanning-type-family-symmetric-descent-data-pushout P b →
-      spanning-type-family-symmetric-descent-data-pushout Q b
-    spanning-type-map-equiv-symmetric-descent-data-pushout b =
-      map-equiv (spanning-type-equiv-equiv-symmetric-descent-data-pushout b)
-
-    is-equiv-spanning-type-map-equiv-symmetric-descent-data-pushout :
-      (b : spanning-type-span-diagram 𝒮) →
-      is-equiv (spanning-type-map-equiv-symmetric-descent-data-pushout b)
-    is-equiv-spanning-type-map-equiv-symmetric-descent-data-pushout b =
-      is-equiv-map-equiv
-        ( spanning-type-equiv-equiv-symmetric-descent-data-pushout b)
-
-    inv-spanning-type-map-equiv-symmetric-descent-data-pushout :
-      (b : spanning-type-span-diagram 𝒮) →
-      spanning-type-family-symmetric-descent-data-pushout Q b →
-      spanning-type-family-symmetric-descent-data-pushout P b
-    inv-spanning-type-map-equiv-symmetric-descent-data-pushout b =
-      map-inv-equiv (spanning-type-equiv-equiv-symmetric-descent-data-pushout b)
-
-    coherence-left-equiv-symmetric-descent-data-pushout :
-      (s : spanning-type-span-diagram 𝒮) →
-      coherence-square-maps
-        ( spanning-type-map-equiv-symmetric-descent-data-pushout s)
-        ( map-left-family-symmetric-descent-data-pushout P s)
-        ( map-left-family-symmetric-descent-data-pushout Q s)
-        ( left-map-equiv-symmetric-descent-data-pushout
-          ( left-map-span-diagram 𝒮 s))
-    coherence-left-equiv-symmetric-descent-data-pushout =
-      pr1 (pr2 (pr2 (pr2 e)))
-
-    coherence-right-equiv-symmetric-descent-data-pushout :
-      (s : spanning-type-span-diagram 𝒮) →
-      coherence-square-maps
-        ( spanning-type-map-equiv-symmetric-descent-data-pushout s)
-        ( map-right-family-symmetric-descent-data-pushout P s)
-        ( map-right-family-symmetric-descent-data-pushout Q s)
-        ( right-map-equiv-symmetric-descent-data-pushout
-          ( right-map-span-diagram 𝒮 s))
-    coherence-right-equiv-symmetric-descent-data-pushout =
-      pr2 (pr2 (pr2 (pr2 e)))
-
-    coherence-left-right-equiv-symmetric-descent-data-pushout :
-      (s : spanning-type-span-diagram 𝒮) →
-      coherence-square-maps
-        ( left-map-equiv-symmetric-descent-data-pushout
-          ( left-map-span-diagram 𝒮 s))
-        ( map-left-right-family-symmetric-descent-data-pushout P s)
-        ( map-left-right-family-symmetric-descent-data-pushout Q s)
-        ( right-map-equiv-symmetric-descent-data-pushout
-          ( right-map-span-diagram 𝒮 s))
-    coherence-left-right-equiv-symmetric-descent-data-pushout s =
-      pasting-vertical-coherence-square-maps
-        ( left-map-equiv-symmetric-descent-data-pushout
-          ( left-map-span-diagram 𝒮 s))
-        ( map-inv-left-family-symmetric-descent-data-pushout P s)
-        ( map-inv-left-family-symmetric-descent-data-pushout Q s)
-        ( spanning-type-map-equiv-symmetric-descent-data-pushout s)
-        ( map-right-family-symmetric-descent-data-pushout P s)
-        ( map-right-family-symmetric-descent-data-pushout Q s)
-        ( right-map-equiv-symmetric-descent-data-pushout
-          ( right-map-span-diagram 𝒮 s))
-        (vertical-inv-equiv-coherence-square-maps
-          ( spanning-type-map-equiv-symmetric-descent-data-pushout s)
-          ( equiv-left-family-symmetric-descent-data-pushout P s)
-          ( equiv-left-family-symmetric-descent-data-pushout Q s)
-          ( left-map-equiv-symmetric-descent-data-pushout
-            ( left-map-span-diagram 𝒮 s))
-          ( coherence-left-equiv-symmetric-descent-data-pushout s))
-        ( coherence-right-equiv-symmetric-descent-data-pushout s)
-
-    coherence-right-left-equiv-symmetric-descent-data-pushout :
-      (s : spanning-type-span-diagram 𝒮) →
-      coherence-square-maps
-        ( right-map-equiv-symmetric-descent-data-pushout
-          ( right-map-span-diagram 𝒮 s))
-        ( map-right-left-family-symmetric-descent-data-pushout P s)
-        ( map-right-left-family-symmetric-descent-data-pushout Q s)
-        ( left-map-equiv-symmetric-descent-data-pushout
-          ( left-map-span-diagram 𝒮 s))
-    coherence-right-left-equiv-symmetric-descent-data-pushout s =
-      pasting-vertical-coherence-square-maps
-        ( right-map-equiv-symmetric-descent-data-pushout
-          ( right-map-span-diagram 𝒮 s))
-        ( map-inv-right-family-symmetric-descent-data-pushout P s)
-        ( map-inv-right-family-symmetric-descent-data-pushout Q s)
-        ( spanning-type-map-equiv-symmetric-descent-data-pushout s)
-        ( map-left-family-symmetric-descent-data-pushout P s)
-        ( map-left-family-symmetric-descent-data-pushout Q s)
-        ( left-map-equiv-symmetric-descent-data-pushout
-          ( left-map-span-diagram 𝒮 s))
-        (vertical-inv-equiv-coherence-square-maps
-          ( spanning-type-map-equiv-symmetric-descent-data-pushout s)
-          ( equiv-right-family-symmetric-descent-data-pushout P s)
-          ( equiv-right-family-symmetric-descent-data-pushout Q s)
-          ( right-map-equiv-symmetric-descent-data-pushout
-            ( right-map-span-diagram 𝒮 s))
-          ( coherence-right-equiv-symmetric-descent-data-pushout s))
-        ( coherence-left-equiv-symmetric-descent-data-pushout s)
+    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
 ```
 
 ### The identity equivalence of descent data for pushouts

From 6f26a15ad671040a730c0f19cf6c7c6271bec32f Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 15 Jul 2025 15:28:26 +0200
Subject: [PATCH 13/13] review <3

---
 .../postcomposition-pullbacks.lagda.md        |  4 +-
 .../anodyne-maps.lagda.md                     | 59 +++++++++++--------
 .../weakly-anodyne-maps.lagda.md              | 21 +++----
 .../cocartesian-morphisms-arrows.lagda.md     | 39 ++++++------
 .../pushouts.lagda.md                         | 24 ++++----
 5 files changed, 79 insertions(+), 68 deletions(-)

diff --git a/src/foundation/postcomposition-pullbacks.lagda.md b/src/foundation/postcomposition-pullbacks.lagda.md
index f5f0528db2..f2f61bf6b5 100644
--- a/src/foundation/postcomposition-pullbacks.lagda.md
+++ b/src/foundation/postcomposition-pullbacks.lagda.md
@@ -123,13 +123,13 @@ triangle-map-standard-pullback-postcomp T f g c h =
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
+  {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)
   where
 
   abstract
     is-pullback-postcomp-is-pullback :
-      is-pullback f g c → (T : UU l5) →
+      is-pullback f g c → {l5 : Level} (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 _ _ _
diff --git a/src/orthogonal-factorization-systems/anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md
index 9a53d0201b..8f86a1c09d 100644
--- a/src/orthogonal-factorization-systems/anodyne-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md
@@ -25,9 +25,10 @@ open import synthetic-homotopy-theory.cocartesian-morphisms-arrows
 ## Idea
 
 A map $j : C → D$ is said to be
-{{#concept "anodyne" Disambiguation="map of types" Agda=is-anodyne}} with
+{{#concept "anodyne" Disambiguation="map of types" Agda=is-anodyne-map}} with
 respect to a map $f : A → B$, or **$f$-anodyne**, if every map that is
-orthogonal to $f$ is also orthogonal to $j$.
+[orthogonal](orthogonal-factorization-systems.orthogonal-maps.md) to $f$ is also
+orthogonal to $j$.
 
 ## Definitions
 
@@ -40,13 +41,13 @@ module _
   (f : A → B) (j : C → D)
   where
 
-  is-anodyne-Level :
+  is-anodyne-map-Level :
     (l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6)
-  is-anodyne-Level l5 l6 =
+  is-anodyne-map-Level l5 l6 =
     {X : UU l5} {Y : UU l6} (g : X → Y) → is-orthogonal f g → is-orthogonal j g
 
-  is-anodyne : UUω
-  is-anodyne = {l5 l6 : Level} → is-anodyne-Level l5 l6
+  is-anodyne-map : UUω
+  is-anodyne-map = {l5 l6 : Level} → is-anodyne-map-Level l5 l6
 ```
 
 ## Properties
@@ -60,8 +61,8 @@ module _
   (f : A → B) {j i : C → D}
   where
 
-  is-anodyne-htpy : j ~ i → is-anodyne f j → is-anodyne f i
-  is-anodyne-htpy K J g H = is-orthogonal-htpy-left j g K (J g H)
+  is-anodyne-map-htpy : j ~ i → is-anodyne-map f j → is-anodyne-map f i
+  is-anodyne-map-htpy K J g H = is-orthogonal-htpy-left j g K (J g H)
 ```
 
 ### Anodyne maps are closed under equivalences of maps
@@ -73,8 +74,10 @@ module _
   (f : A → B) {j : C → D} {j' : C' → D'}
   where
 
-  is-anodyne-equiv-arrow : equiv-arrow j j' → is-anodyne f j → is-anodyne f j'
-  is-anodyne-equiv-arrow α J g H = is-orthogonal-left-equiv-arrow α g (J g H)
+  is-anodyne-map-equiv-arrow :
+    equiv-arrow j j' → is-anodyne-map f j → is-anodyne-map f j'
+  is-anodyne-map-equiv-arrow α J g H =
+    is-orthogonal-left-equiv-arrow α g (J g H)
 ```
 
 ### Anodyne maps are closed under retracts of maps
@@ -90,8 +93,9 @@ module _
   (f : A → B) (j : C → D) (i : D → E)
   where
 
-  is-anodyne-comp : is-anodyne f j → is-anodyne f i → is-anodyne f (i ∘ j)
-  is-anodyne-comp J I g H = is-orthogonal-left-comp j i g (J g H) (I g H)
+  is-anodyne-map-comp :
+    is-anodyne-map f j → is-anodyne-map f i → is-anodyne-map f (i ∘ j)
+  is-anodyne-map-comp J I g H = is-orthogonal-left-comp j i g (J g H) (I g H)
 ```
 
 ### Cancellation property for anodyne maps
@@ -103,9 +107,9 @@ module _
   (f : A → B) (j : C → D) (i : D → E)
   where
 
-  is-anodyne-left-factor :
-    is-anodyne f j → is-anodyne f (i ∘ j) → is-anodyne f i
-  is-anodyne-left-factor J IJ g H =
+  is-anodyne-map-left-factor :
+    is-anodyne-map f j → is-anodyne-map f (i ∘ j) → is-anodyne-map f i
+  is-anodyne-map-left-factor J IJ g H =
     is-orthogonal-left-left-factor j i g (J g H) (IJ g H)
 ```
 
@@ -118,8 +122,9 @@ module _
   (f : A → B) (j : (i : I) → C i → D i)
   where
 
-  is-anodyne-tot : ((i : I) → is-anodyne f (j i)) → is-anodyne f (tot j)
-  is-anodyne-tot J g H = is-orthogonal-left-tot j g (λ i → J i g H)
+  is-anodyne-map-tot :
+    ((i : I) → is-anodyne-map f (j i)) → is-anodyne-map f (tot j)
+  is-anodyne-map-tot J g H = is-orthogonal-left-tot j g (λ i → J i g H)
 ```
 
 ### Anodyne maps are closed under products
@@ -131,9 +136,9 @@ module _
   (f : A → B) (j : C → D) (i : E → F)
   where
 
-  is-anodyne-map-product :
-    is-anodyne f j → is-anodyne f i → is-anodyne f (map-product j i)
-  is-anodyne-map-product J I g H =
+  is-anodyne-map-map-product :
+    is-anodyne-map f j → is-anodyne-map f i → is-anodyne-map f (map-product j i)
+  is-anodyne-map-map-product J I g H =
     is-orthogonal-left-product j i g (J g H) (I g H)
 ```
 
@@ -146,9 +151,11 @@ module _
   (f : A → B) (j : C → D) (i : E → F)
   where
 
-  is-anodyne-map-coproduct :
-    is-anodyne f j → is-anodyne f i → is-anodyne f (map-coproduct j i)
-  is-anodyne-map-coproduct J I g H =
+  is-anodyne-map-map-coproduct :
+    is-anodyne-map f j →
+    is-anodyne-map f i →
+    is-anodyne-map f (map-coproduct j i)
+  is-anodyne-map-map-coproduct J I g H =
     is-orthogonal-left-coproduct j i g (J g H) (I g H)
 ```
 
@@ -161,9 +168,9 @@ module _
   (f : A → B) (j : C → D) (i : E → F)
   where
 
-  is-anodyne-cobase-change :
-    cocartesian-hom-arrow j i → is-anodyne f j → is-anodyne f i
-  is-anodyne-cobase-change α J g H =
+  is-anodyne-map-cobase-change :
+    cocartesian-hom-arrow j i → is-anodyne-map f j → is-anodyne-map f i
+  is-anodyne-map-cobase-change α J g H =
     is-orthogonal-left-cobase-change j i g α (J g H)
 ```
 
diff --git a/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md
index c057f9195d..a2a1cdbe49 100644
--- a/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md
@@ -31,7 +31,7 @@ open import synthetic-homotopy-theory.cocartesian-morphisms-arrows
 ## Idea
 
 A map $j : C → D$ is said to be
-{{#concept "weakly anodyne" Disambiguation="map of types" Agda=is-weakly-anodyne}}
+{{#concept "weakly anodyne" Disambiguation="map of types" Agda=is-weakly-anodyne-map}}
 with respect to a map $f : A → B$, or **weakly $f$-anodyne**, if every map that
 is local at $f$ is also local at $j$.
 
@@ -46,13 +46,13 @@ module _
   (f : A → B) (j : C → D)
   where
 
-  is-weakly-anodyne-Level :
+  is-weakly-anodyne-map-Level :
     (l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6)
-  is-weakly-anodyne-Level l5 l6 =
+  is-weakly-anodyne-map-Level l5 l6 =
     {X : UU l5} {Y : UU l6} (g : X → Y) → is-local-map f g → is-local-map j g
 
-  is-weakly-anodyne : UUω
-  is-weakly-anodyne = {l5 l6 : Level} → is-weakly-anodyne-Level l5 l6
+  is-weakly-anodyne-map : UUω
+  is-weakly-anodyne-map = {l5 l6 : Level} → is-weakly-anodyne-map-Level l5 l6
 ```
 
 ## Properties
@@ -66,8 +66,9 @@ module _
   (f : A → B) {j : C → D}
   where
 
-  is-weakly-anodyne-is-anodyne : is-anodyne f j → is-weakly-anodyne f j
-  is-weakly-anodyne-is-anodyne J g G x =
+  is-weakly-anodyne-map-is-anodyne-map :
+    is-anodyne-map f j → is-weakly-anodyne-map f j
+  is-weakly-anodyne-map-is-anodyne-map J g G x =
     is-local-is-orthogonal-terminal-map j
       ( J ( terminal-map (fiber g x))
           ( is-orthogonal-terminal-map-is-local f (G x)))
@@ -82,8 +83,8 @@ module _
   (f : A → B) {j : C → D} {j' : C' → D'}
   where
 
-  is-weakly-anodyne-retract-map :
-    retract-map j j' → is-weakly-anodyne f j → is-weakly-anodyne f j'
-  is-weakly-anodyne-retract-map α J g G x =
+  is-weakly-anodyne-map-retract-map :
+    retract-map j j' → is-weakly-anodyne-map f j → is-weakly-anodyne-map f j'
+  is-weakly-anodyne-map-retract-map α J g G x =
     is-local-retract-map-is-local j' j α (fiber g x) (J g G x)
 ```
diff --git a/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md b/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md
index e1188a0d13..634145c719 100644
--- a/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md
+++ b/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md
@@ -137,26 +137,27 @@ module _
   precomp-cocartesian-hom-arrow =
     precomp-hom-arrow f g (hom-arrow-cocartesian-hom-arrow f g α) S
 
-  is-cartesian-precomp-cocartesian-hom-arrow :
-    is-cartesian-hom-arrow
-      ( precomp g S)
-      ( precomp f S)
-      ( precomp-cocartesian-hom-arrow)
-  is-cartesian-precomp-cocartesian-hom-arrow =
-    is-pullback-swap-cone
-      ( precomp f S)
-      ( precomp (map-domain-cocartesian-hom-arrow f g α) S)
-      ( cone-hom-arrow
-        ( precomp (map-codomain-cocartesian-hom-arrow f g α) S)
+  abstract
+    is-cartesian-precomp-cocartesian-hom-arrow :
+      is-cartesian-hom-arrow
+        ( precomp g S)
+        ( precomp f S)
+        ( precomp-cocartesian-hom-arrow)
+    is-cartesian-precomp-cocartesian-hom-arrow =
+      is-pullback-swap-cone
+        ( precomp f S)
         ( precomp (map-domain-cocartesian-hom-arrow f g α) S)
-        ( transpose-precomp-hom-arrow f g
-          ( hom-arrow-cocartesian-hom-arrow f g α)
-          ( S)))
-      ( pullback-property-pushout-is-pushout
-        ( f)
-        ( map-domain-cocartesian-hom-arrow f g α)
-        ( cocone-cocartesian-hom-arrow f g α)
-        ( is-cocartesian-cocartesian-hom-arrow f g α) S)
+        ( cone-hom-arrow
+          ( precomp (map-codomain-cocartesian-hom-arrow f g α) S)
+          ( precomp (map-domain-cocartesian-hom-arrow f g α) S)
+          ( transpose-precomp-hom-arrow f g
+            ( hom-arrow-cocartesian-hom-arrow f g α)
+            ( S)))
+        ( pullback-property-pushout-is-pushout
+          ( f)
+          ( map-domain-cocartesian-hom-arrow f g α)
+          ( cocone-cocartesian-hom-arrow f g α)
+          ( is-cocartesian-cocartesian-hom-arrow f g α) S)
 
   precomp-cartesian-hom-arrow-cocartesian-hom-arrow :
     cartesian-hom-arrow (precomp g S) (precomp f S)
diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index e2737409b4..5242c08e65 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -468,17 +468,19 @@ module _
   (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)
+  abstract
+    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)
+
+  abstract
+    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