diff --git a/Makefile b/Makefile
index 003f3341e6..74df635d51 100644
--- a/Makefile
+++ b/Makefile
@@ -4,7 +4,7 @@
 # files, and if these options are pervasive (i.e. they need to be enabled in all
 # modules that include the modules that have them enabled), then they need to be
 # added to the everything file as well.
-everythingOpts := --guardedness --cohesion --flat-split
+everythingOpts := --guardedness --cohesion --flat-split --rewriting
 # use "$ export AGDAVERBOSE=-v20" if you want to see all
 AGDAVERBOSE ?= -v1
 
diff --git a/agda-unimath.agda-lib b/agda-unimath.agda-lib
index b7557d82bd..d57349cb40 100644
--- a/agda-unimath.agda-lib
+++ b/agda-unimath.agda-lib
@@ -1,3 +1,3 @@
 name: agda-unimath
 include: src
-flags: --without-K --exact-split --no-import-sorts --auto-inline
+flags: --without-K --exact-split --no-import-sorts --auto-inline -WnoWithoutKFlagPrimEraseEquality
diff --git a/src/foundation/constant-type-families.lagda.md b/src/foundation/constant-type-families.lagda.md
index c3daca83ba..58fd987d4a 100644
--- a/src/foundation/constant-type-families.lagda.md
+++ b/src/foundation/constant-type-families.lagda.md
@@ -10,8 +10,10 @@ module foundation.constant-type-families where
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
+open import foundation-core.commuting-squares-of-identifications
 open import foundation-core.dependent-identifications
 open import foundation-core.equivalences
 open import foundation-core.identity-types
@@ -79,6 +81,45 @@ tr-constant-type-family refl b = refl
 ```agda
 apd-constant-type-family :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y : A} (p : x ＝ y) →
-  apd f p ＝ (tr-constant-type-family p (f x) ∙ ap f p)
+  apd f p ＝ tr-constant-type-family p (f x) ∙ ap f p
 apd-constant-type-family f refl = refl
 ```
+
+### Naturality of transport in constant type families
+
+For every equality `p : x ＝ x'` in `A` and `q : y ＝ y'` in `B` we have a
+commuting square of identifications
+
+```text
+                    ap (tr (λ _ → B) p) q
+          tr (λ _ → B) p y ------> tr (λ _ → B) p y'
+                         |         |
+  tr-constant-family p y |         | tr-constant-family p y'
+                         ∨         ∨
+                         y ------> y'.
+                              q
+```
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  naturality-tr-constant-type-family :
+    {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
+    coherence-square-identifications
+      ( ap (tr (λ _ → B) p) q)
+      ( tr-constant-type-family p y)
+      ( tr-constant-type-family p y')
+      ( q)
+  naturality-tr-constant-type-family p refl = right-unit
+
+  naturality-inv-tr-constant-type-family :
+    {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
+    coherence-square-identifications
+      ( q)
+      ( inv (tr-constant-type-family p y))
+      ( inv (tr-constant-type-family p y'))
+      ( ap (tr (λ _ → B) p) q)
+  naturality-inv-tr-constant-type-family p refl = right-unit
+```
diff --git a/src/foundation/dependent-identifications.lagda.md b/src/foundation/dependent-identifications.lagda.md
index 80539b1d9c..fc4b128c5d 100644
--- a/src/foundation/dependent-identifications.lagda.md
+++ b/src/foundation/dependent-identifications.lagda.md
@@ -43,7 +43,7 @@ module _
     {x' : B x} {y' : B y}
     (p' : dependent-identification B p x' y')
     (q' : dependent-identification B q x' y') →
-    p' ＝ ((tr² B α _) ∙ q') → dependent-identification² B α p' q'
+    p' ＝ tr² B α x' ∙ q' → dependent-identification² B α p' q'
   map-compute-dependent-identification² refl ._ refl refl =
     refl
 
@@ -52,7 +52,7 @@ module _
     {x' : B x} {y' : B y}
     (p' : dependent-identification B p x' y')
     (q' : dependent-identification B q x' y') →
-    dependent-identification² B α p' q' → p' ＝ ((tr² B α _) ∙ q')
+    dependent-identification² B α p' q' → p' ＝ tr² B α x' ∙ q'
   map-inv-compute-dependent-identification² refl refl ._ refl =
     refl
 
@@ -93,7 +93,7 @@ module _
     {x' : B x} {y' : B y}
     (p' : dependent-identification B p x' y')
     (q' : dependent-identification B q x' y') →
-    (p' ＝ ((tr² B α _) ∙ q')) ≃ dependent-identification² B α p' q'
+    (p' ＝ tr² B α x' ∙ q') ≃ dependent-identification² B α p' q'
   pr1 (compute-dependent-identification² α p' q') =
     map-compute-dependent-identification² α p' q'
   pr2 (compute-dependent-identification² α p' q') =
diff --git a/src/foundation/transport-along-identifications.lagda.md b/src/foundation/transport-along-identifications.lagda.md
index 61ae11003c..10987aecc0 100644
--- a/src/foundation/transport-along-identifications.lagda.md
+++ b/src/foundation/transport-along-identifications.lagda.md
@@ -75,7 +75,7 @@ equiv-tr-refl B = refl
 
 ```agda
 tr-loop :
-  {l1 : Level} {A : UU l1} {a0 a1 : A} (p : a0 ＝ a1) (l : a0 ＝ a0) →
-  (tr (λ y → y ＝ y) p l) ＝ ((inv p ∙ l) ∙ p)
-tr-loop refl l = inv right-unit
+  {l1 : Level} {A : UU l1} {a0 a1 : A} (p : a0 ＝ a1) (q : a0 ＝ a0) →
+  tr (λ y → y ＝ y) p q ＝ (inv p ∙ q) ∙ p
+tr-loop refl q = inv right-unit
 ```
diff --git a/src/reflection.lagda.md b/src/reflection.lagda.md
index b391840a82..f0d2255e66 100644
--- a/src/reflection.lagda.md
+++ b/src/reflection.lagda.md
@@ -1,5 +1,9 @@
 # Reflection
 
+```agda
+{-# OPTIONS --rewriting #-}
+```
+
 ## Files in the reflection folder
 
 ```agda
@@ -9,12 +13,14 @@ open import reflection.abstractions public
 open import reflection.arguments public
 open import reflection.boolean-reflection public
 open import reflection.definitions public
+open import reflection.erasing-equality public
 open import reflection.fixity public
 open import reflection.group-solver public
 open import reflection.literals public
 open import reflection.metavariables public
 open import reflection.names public
 open import reflection.precategory-solver public
+open import reflection.rewriting public
 open import reflection.terms public
 open import reflection.type-checking-monad public
 ```
diff --git a/src/reflection/erasing-equality.lagda.md b/src/reflection/erasing-equality.lagda.md
new file mode 100644
index 0000000000..3f3a0bec8a
--- /dev/null
+++ b/src/reflection/erasing-equality.lagda.md
@@ -0,0 +1,47 @@
+# Erasing equality
+
+```agda
+module reflection.erasing-equality where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+Agda's builtin primitive `primEraseEquality` is a special construct on
+[identifications](foundation-core.identity-types.md) that for every
+identification `x ＝ y` gives an identification `x ＝ y` with the following
+reduction behaviour:
+
+- If the two end points `x ＝ y` normalize to the same term, `primEraseEquality`
+  reduces to `refl`.
+
+For example, `primEraseEquality` applied to the loop of the
+[circle](synthetic-homotopy-theory.circle.md) will compute to `refl`, while
+`primEraseEquality` applied to the nontrivial identification in the
+[interval](synthetic-homotopy-theory.interval-type.md) will not reduce.
+
+This primitive is useful for [rewrite rules](reflection.rewriting.md), as it
+ensures that the identification used in defining the rewrite rule also computes
+to `refl`. Concretely, if the identification `β` defines a rewrite rule, and `β`
+is defined via `primEraseEqaulity`, then we have the strict equality `β ≐ refl`.
+
+## Primitives
+
+```agda
+primitive
+  primEraseEquality : {l : Level} {A : UU l} {x y : A} → x ＝ y → x ＝ y
+```
+
+## External links
+
+- [Built-ins#Equality](https://agda.readthedocs.io/en/latest/language/built-ins.html#equality)
+  at Agda's documentation pages
diff --git a/src/reflection/rewriting.lagda.md b/src/reflection/rewriting.lagda.md
new file mode 100644
index 0000000000..159ba1e1ed
--- /dev/null
+++ b/src/reflection/rewriting.lagda.md
@@ -0,0 +1,49 @@
+# Rewriting
+
+```agda
+{-# OPTIONS --rewriting #-}
+
+module reflection.rewriting where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+Agda's rewriting functionality allows us to add new strict equalities to our
+type theory. Given an [identification](foundation-core.identity-types.md)
+`β : x ＝ y`, then adding a rewrite rule for `β` with
+
+```text
+{-# REWRITE β #-}
+```
+
+will make it so `x` rewrites to `y`, i.e., `x ≐ y`.
+
+**Warning.** Rewriting is by nature a very unsafe tool so we advice exercising
+abundant caution when defining such rules.
+
+## Definitions
+
+We declare to Agda that the
+[standard identity relation](foundation.identity-types.md) may be used to define
+rewrite rules.
+
+```agda
+{-# BUILTIN REWRITE _＝_ #-}
+```
+
+## See also
+
+- [Erasing equality](reflection.erasing-equality.md)
+
+## External links
+
+- [Rewriting](https://agda.readthedocs.io/en/latest/language/rewriting.html) at
+  Agda's documentation pages
diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index d1663a7fd1..dbe44b253b 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -1,5 +1,9 @@
 # Synthetic homotopy theory
 
+```agda
+{-# OPTIONS --rewriting #-}
+```
+
 ## Files in the synthetic homotopy theory folder
 
 ```agda
@@ -90,7 +94,9 @@ open import synthetic-homotopy-theory.pullback-property-pushouts public
 open import synthetic-homotopy-theory.pushout-products public
 open import synthetic-homotopy-theory.pushouts public
 open import synthetic-homotopy-theory.pushouts-of-pointed-types public
+open import synthetic-homotopy-theory.recursion-principle-pushouts public
 open import synthetic-homotopy-theory.retracts-of-sequential-diagrams public
+open import synthetic-homotopy-theory.rewriting-pushouts public
 open import synthetic-homotopy-theory.sections-descent-circle public
 open import synthetic-homotopy-theory.sequential-colimits public
 open import synthetic-homotopy-theory.sequential-diagrams public
diff --git a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
index ee937b06f0..daaa5bd191 100644
--- a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
@@ -117,15 +117,39 @@ module _
         ( vertical-htpy-cocone)
     coherence-htpy-cocone = pr2 (pr2 H)
 
-  reflexive-htpy-cocone :
+  refl-htpy-cocone :
     (c : cocone f g X) → htpy-cocone c c
-  pr1 (reflexive-htpy-cocone (i , j , H)) = refl-htpy
-  pr1 (pr2 (reflexive-htpy-cocone (i , j , H))) = refl-htpy
-  pr2 (pr2 (reflexive-htpy-cocone (i , j , H))) = right-unit-htpy
+  pr1 (refl-htpy-cocone (i , j , H)) = refl-htpy
+  pr1 (pr2 (refl-htpy-cocone (i , j , H))) = refl-htpy
+  pr2 (pr2 (refl-htpy-cocone (i , j , H))) = right-unit-htpy
 
   htpy-eq-cocone :
     (c c' : cocone f g X) → c ＝ c' → htpy-cocone c c'
-  htpy-eq-cocone c .c refl = reflexive-htpy-cocone c
+  htpy-eq-cocone c .c refl = refl-htpy-cocone c
+
+  module _
+    (c c' : cocone f g X)
+    (p : c ＝ c')
+    where
+
+    horizontal-htpy-eq-cocone :
+      horizontal-map-cocone f g c ~
+      horizontal-map-cocone f g c'
+    horizontal-htpy-eq-cocone =
+      horizontal-htpy-cocone c c' (htpy-eq-cocone c c' p)
+
+    vertical-htpy-eq-cocone :
+      vertical-map-cocone f g c ~
+      vertical-map-cocone f g c'
+    vertical-htpy-eq-cocone =
+      vertical-htpy-cocone c c' (htpy-eq-cocone c c' p)
+
+    coherence-square-htpy-eq-cocone :
+      statement-coherence-htpy-cocone c c'
+        ( horizontal-htpy-eq-cocone)
+        ( vertical-htpy-eq-cocone)
+    coherence-square-htpy-eq-cocone =
+      coherence-htpy-cocone c c' (htpy-eq-cocone c c' p)
 
   is-torsorial-htpy-cocone :
     (c : cocone f g X) → is-torsorial (htpy-cocone c)
diff --git a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
index 9d8e684cbb..f3b33ac51b 100644
--- a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
@@ -9,20 +9,32 @@ module synthetic-homotopy-theory.dependent-cocones-under-spans where
 ```agda
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-identifications
+open import foundation.commuting-squares-of-maps
+open import foundation.constant-type-families
 open import foundation.contractible-types
+open import foundation.dependent-homotopies
 open import foundation.dependent-identifications
 open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
 open import foundation.equivalences
+open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopies
 open import foundation.homotopy-induction
 open import foundation.identity-types
+open import foundation.retractions
+open import foundation.sections
 open import foundation.structure-identity-principle
 open import foundation.torsorial-type-families
+open import foundation.transport-along-higher-identifications
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import foundation-core.injective-maps
 
 open import synthetic-homotopy-theory.cocones-under-spans
 ```
@@ -94,6 +106,75 @@ module _
     coherence-square-dependent-cocone = pr2 (pr2 d)
 ```
 
+### Cocones equipped with dependent cocones
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
+  (f : S → A) (g : S → B) (P : X → UU l5)
+  where
+
+  cocone-with-dependent-cocone : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
+  cocone-with-dependent-cocone =
+    Σ (cocone f g X) (λ c → dependent-cocone f g c P)
+
+module _
+  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
+  (f : S → A) (g : S → B) (P : X → UU l5)
+  (c : cocone-with-dependent-cocone f g P)
+  where
+
+  cocone-cocone-with-dependent-cocone : cocone f g X
+  cocone-cocone-with-dependent-cocone = pr1 c
+
+  horizontal-map-cocone-with-dependent-cocone : A → X
+  horizontal-map-cocone-with-dependent-cocone =
+    horizontal-map-cocone f g cocone-cocone-with-dependent-cocone
+
+  vertical-map-cocone-with-dependent-cocone : B → X
+  vertical-map-cocone-with-dependent-cocone =
+    vertical-map-cocone f g cocone-cocone-with-dependent-cocone
+
+  coherence-square-cocone-with-dependent-cocone :
+    coherence-square-maps g f
+      ( vertical-map-cocone-with-dependent-cocone)
+      ( horizontal-map-cocone-with-dependent-cocone)
+  coherence-square-cocone-with-dependent-cocone =
+    coherence-square-cocone f g cocone-cocone-with-dependent-cocone
+
+  dependent-cocone-cocone-with-dependent-cocone :
+    dependent-cocone f g cocone-cocone-with-dependent-cocone P
+  dependent-cocone-cocone-with-dependent-cocone = pr2 c
+
+  horizontal-map-dependent-cocone-with-dependent-cocone :
+    (a : A) → P (horizontal-map-cocone-with-dependent-cocone a)
+  horizontal-map-dependent-cocone-with-dependent-cocone =
+    horizontal-map-dependent-cocone f g
+      ( cocone-cocone-with-dependent-cocone)
+      ( P)
+      ( dependent-cocone-cocone-with-dependent-cocone)
+
+  vertical-map-dependent-cocone-with-dependent-cocone :
+    (b : B) → P (vertical-map-cocone-with-dependent-cocone b)
+  vertical-map-dependent-cocone-with-dependent-cocone =
+    vertical-map-dependent-cocone f g
+      ( cocone-cocone-with-dependent-cocone)
+      ( P)
+      ( dependent-cocone-cocone-with-dependent-cocone)
+
+  coherence-square-dependent-cocone-with-dependent-cocone :
+    (s : S) →
+    dependent-identification P
+      ( coherence-square-cocone-with-dependent-cocone s)
+      ( horizontal-map-dependent-cocone-with-dependent-cocone (f s))
+      ( vertical-map-dependent-cocone-with-dependent-cocone (g s))
+  coherence-square-dependent-cocone-with-dependent-cocone =
+    coherence-square-dependent-cocone f g
+      ( cocone-cocone-with-dependent-cocone)
+      ( P)
+      ( dependent-cocone-cocone-with-dependent-cocone)
+```
+
 ### Postcomposing dependent cocones with maps
 
 ```agda
@@ -111,7 +192,7 @@ pr2 (pr2 (dependent-cocone-map f g c P h)) s =
 
 ## Properties
 
-### Characterization of identifications of dependent cocones
+### Characterization of identifications of dependent cocones over a fixed cocone
 
 ```agda
 module _
@@ -122,12 +203,10 @@ module _
   where
 
   coherence-htpy-dependent-cocone :
-    ( d' : dependent-cocone f g c P)
-    ( K :
-      horizontal-map-dependent-cocone f g c P d ~
-      horizontal-map-dependent-cocone f g c P d')
-    ( L :
-      vertical-map-dependent-cocone f g c P d ~
+    ( d' : dependent-cocone f g c P) →
+    ( horizontal-map-dependent-cocone f g c P d ~
+      horizontal-map-dependent-cocone f g c P d') →
+    ( vertical-map-dependent-cocone f g c P d ~
       vertical-map-dependent-cocone f g c P d') →
     UU (l1 ⊔ l5)
   coherence-htpy-dependent-cocone d' K L =
@@ -226,3 +305,427 @@ module _
     is-retraction-eq-htpy-dependent-cocone d' =
       is-retraction-map-inv-is-equiv (is-equiv-htpy-eq-dependent-cocone d')
 ```
+
+### Dependent homotopies of dependent cocones over homotopies of cocones
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B)
+  {X : UU l4}
+  where
+
+  coherence-dependent-htpy-dependent-cocone :
+    ( c c' : cocone f g X) (H : htpy-cocone f g c c') (P : X → UU l5)
+    ( d : dependent-cocone f g c P)
+    ( d' : dependent-cocone f g c' P) →
+    dependent-homotopy (λ _ → P)
+      ( horizontal-htpy-cocone f g c c' H)
+      ( horizontal-map-dependent-cocone f g c P d)
+      ( horizontal-map-dependent-cocone f g c' P d') →
+    dependent-homotopy (λ _ → P)
+      ( vertical-htpy-cocone f g c c' H)
+      ( vertical-map-dependent-cocone f g c P d)
+      ( vertical-map-dependent-cocone f g c' P d') →
+    UU (l1 ⊔ l5)
+  coherence-dependent-htpy-dependent-cocone c c' H P d d' K L =
+    (s : S) →
+    dependent-identification² P
+      ( coherence-htpy-cocone f g c c' H s)
+      ( concat-dependent-identification P
+        ( coherence-square-cocone f g c s)
+        ( vertical-htpy-cocone f g c c' H (g s))
+        ( coherence-square-dependent-cocone f g c P d s)
+        ( L (g s)))
+      ( concat-dependent-identification P
+        ( horizontal-htpy-cocone f g c c' H (f s))
+        ( coherence-square-cocone f g c' s)
+        ( K (f s))
+        ( coherence-square-dependent-cocone f g c' P d' s))
+
+  dependent-htpy-dependent-cocone :
+    ( c c' : cocone f g X) (H : htpy-cocone f g c c') (P : X → UU l5)
+    ( d : dependent-cocone f g c P) (d' : dependent-cocone f g c' P) →
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l5)
+  dependent-htpy-dependent-cocone c c' H P d d' =
+    Σ ( dependent-homotopy (λ _ → P)
+        ( horizontal-htpy-cocone f g c c' H)
+        ( horizontal-map-dependent-cocone f g c P d)
+        ( horizontal-map-dependent-cocone f g c' P d'))
+      ( λ K →
+        Σ ( dependent-homotopy (λ _ → P)
+            ( vertical-htpy-cocone f g c c' H)
+            ( vertical-map-dependent-cocone f g c P d)
+            ( vertical-map-dependent-cocone f g c' P d'))
+          ( coherence-dependent-htpy-dependent-cocone c c' H P d d' K))
+
+  refl-dependent-htpy-dependent-cocone :
+    ( c : cocone f g X) (P : X → UU l5) (d : dependent-cocone f g c P) →
+    dependent-htpy-dependent-cocone c c (refl-htpy-cocone f g c) P d d
+  pr1 (refl-dependent-htpy-dependent-cocone c P d) = refl-htpy
+  pr1 (pr2 (refl-dependent-htpy-dependent-cocone c P d)) = refl-htpy
+  pr2 (pr2 (refl-dependent-htpy-dependent-cocone c P d)) s =
+    right-unit-dependent-identification P
+      ( coherence-square-cocone f g c s)
+      ( coherence-square-dependent-cocone f g c P d s)
+
+  dependent-htpy-dependent-eq-dependent-cocone :
+    (c c' : cocone f g X) (p : c ＝ c') (P : X → UU l5)
+    (d : dependent-cocone f g c P) (d' : dependent-cocone f g c' P) →
+    dependent-identification (λ c'' → dependent-cocone f g c'' P) p d d' →
+    dependent-htpy-dependent-cocone c c' (htpy-eq-cocone f g c c' p) P d d'
+  dependent-htpy-dependent-eq-dependent-cocone c .c refl P d ._ refl =
+    refl-dependent-htpy-dependent-cocone c P d
+
+  abstract
+    is-torsorial-dependent-htpy-over-refl-dependent-cocone :
+      (c : cocone f g X) (P : X → UU l5) (d : dependent-cocone f g c P) →
+      is-torsorial
+        ( dependent-htpy-dependent-cocone c c (refl-htpy-cocone f g c) P d)
+    is-torsorial-dependent-htpy-over-refl-dependent-cocone c P d =
+      is-torsorial-Eq-structure
+        ( is-torsorial-htpy _)
+        ( horizontal-map-dependent-cocone f g c P d , refl-htpy)
+        ( is-torsorial-Eq-structure
+          ( is-torsorial-htpy _)
+          ( vertical-map-dependent-cocone f g c P d , refl-htpy)
+          ( is-torsorial-htpy _))
+```
+
+#### Characterizing equality of cocones equipped with dependent cocones
+
+We now move to characterize equality of cocones equipped with dependent cocones,
+from which it follows that dependent homotopies of dependent cocones
+characterize dependent identifications of them.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B)
+  {X : UU l4} (P : X → UU l5)
+  where
+
+  htpy-cocone-with-dependent-cocone :
+    (c c' : cocone-with-dependent-cocone f g P) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
+  htpy-cocone-with-dependent-cocone c c' =
+    Σ ( htpy-cocone f g
+        ( cocone-cocone-with-dependent-cocone f g P c)
+        ( cocone-cocone-with-dependent-cocone f g P c'))
+      ( λ H →
+        dependent-htpy-dependent-cocone f g
+          ( cocone-cocone-with-dependent-cocone f g P c)
+          ( cocone-cocone-with-dependent-cocone f g P c')
+          ( H)
+          ( P)
+          ( dependent-cocone-cocone-with-dependent-cocone f g P c)
+          ( dependent-cocone-cocone-with-dependent-cocone f g P c'))
+
+  refl-htpy-cocone-with-dependent-cocone :
+    (c : cocone-with-dependent-cocone f g P) →
+    htpy-cocone-with-dependent-cocone c c
+  pr1 (refl-htpy-cocone-with-dependent-cocone c) =
+    refl-htpy-cocone f g (cocone-cocone-with-dependent-cocone f g P c)
+  pr2 (refl-htpy-cocone-with-dependent-cocone c) =
+    refl-dependent-htpy-dependent-cocone f g
+      ( cocone-cocone-with-dependent-cocone f g P c)
+      ( P)
+      ( dependent-cocone-cocone-with-dependent-cocone f g P c)
+
+  htpy-eq-cocone-with-dependent-cocone :
+    (c c' : cocone-with-dependent-cocone f g P) →
+    c ＝ c' →
+    htpy-cocone-with-dependent-cocone c c'
+  htpy-eq-cocone-with-dependent-cocone c .c refl =
+    refl-htpy-cocone-with-dependent-cocone c
+
+  abstract
+    is-torsorial-htpy-cocone-with-dependent-cocone :
+      (c : cocone-with-dependent-cocone f g P) →
+      is-torsorial (htpy-cocone-with-dependent-cocone c)
+    is-torsorial-htpy-cocone-with-dependent-cocone c =
+      is-torsorial-Eq-structure
+        ( is-torsorial-htpy-cocone f g
+          ( cocone-cocone-with-dependent-cocone f g P c))
+        ( cocone-cocone-with-dependent-cocone f g P c ,
+          refl-htpy-cocone f g (cocone-cocone-with-dependent-cocone f g P c))
+        ( is-torsorial-dependent-htpy-over-refl-dependent-cocone f g
+          ( cocone-cocone-with-dependent-cocone f g P c)
+          ( P)
+          ( dependent-cocone-cocone-with-dependent-cocone f g P c))
+
+  abstract
+    is-equiv-htpy-eq-cocone-with-dependent-cocone :
+      (c c' : cocone-with-dependent-cocone f g P) →
+      is-equiv (htpy-eq-cocone-with-dependent-cocone c c')
+    is-equiv-htpy-eq-cocone-with-dependent-cocone c =
+      fundamental-theorem-id
+        ( is-torsorial-htpy-cocone-with-dependent-cocone c)
+        ( htpy-eq-cocone-with-dependent-cocone c)
+
+  eq-htpy-cocone-with-dependent-cocone :
+    (c c' : cocone-with-dependent-cocone f g P) →
+    htpy-cocone-with-dependent-cocone c c' → c ＝ c'
+  eq-htpy-cocone-with-dependent-cocone c c' =
+    map-inv-is-equiv (is-equiv-htpy-eq-cocone-with-dependent-cocone c c')
+
+  extensionality-cocone-with-dependent-cocone :
+    (c c' : cocone-with-dependent-cocone f g P) →
+    (c ＝ c') ≃ htpy-cocone-with-dependent-cocone c c'
+  extensionality-cocone-with-dependent-cocone c c' =
+    ( htpy-eq-cocone-with-dependent-cocone c c' ,
+      is-equiv-htpy-eq-cocone-with-dependent-cocone c c')
+```
+
+### Dependent cocones on constant type families are equivalent to nondependent cocones
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
+  (f : S → A) (g : S → B) (c : cocone f g X) {Y : UU l5}
+  where
+
+  dependent-cocone-constant-type-family-cocone :
+    cocone f g Y → dependent-cocone f g c (λ _ → Y)
+  pr1 (dependent-cocone-constant-type-family-cocone (f' , g' , H)) = f'
+  pr1 (pr2 (dependent-cocone-constant-type-family-cocone (f' , g' , H))) = g'
+  pr2 (pr2 (dependent-cocone-constant-type-family-cocone (f' , g' , H))) s =
+    tr-constant-type-family (coherence-square-cocone f g c s) (f' (f s)) ∙ H s
+
+  cocone-dependent-cocone-constant-type-family :
+    dependent-cocone f g c (λ _ → Y) → cocone f g Y
+  pr1 (cocone-dependent-cocone-constant-type-family (f' , g' , H)) = f'
+  pr1 (pr2 (cocone-dependent-cocone-constant-type-family (f' , g' , H))) = g'
+  pr2 (pr2 (cocone-dependent-cocone-constant-type-family (f' , g' , H))) s =
+    ( inv
+      ( tr-constant-type-family (coherence-square-cocone f g c s) (f' (f s)))) ∙
+    ( H s)
+
+  is-section-cocone-dependent-cocone-constant-type-family :
+    is-section
+      ( dependent-cocone-constant-type-family-cocone)
+      ( cocone-dependent-cocone-constant-type-family)
+  is-section-cocone-dependent-cocone-constant-type-family (f' , g' , H) =
+    eq-pair-eq-fiber
+      ( eq-pair-eq-fiber
+        ( eq-htpy
+          ( λ s →
+            is-section-inv-concat
+              ( tr-constant-type-family
+                ( coherence-square-cocone f g c s)
+                ( f' (f s)))
+              ( H s))))
+
+  is-retraction-cocone-dependent-cocone-constant-type-family :
+    is-retraction
+      ( dependent-cocone-constant-type-family-cocone)
+      ( cocone-dependent-cocone-constant-type-family)
+  is-retraction-cocone-dependent-cocone-constant-type-family (f' , g' , H) =
+    eq-pair-eq-fiber
+      ( eq-pair-eq-fiber
+        ( eq-htpy
+          ( λ s →
+            is-retraction-inv-concat
+              ( tr-constant-type-family
+                ( coherence-square-cocone f g c s)
+                ( f' (f s)))
+              ( H s))))
+
+  is-equiv-dependent-cocone-constant-type-family-cocone :
+    is-equiv dependent-cocone-constant-type-family-cocone
+  is-equiv-dependent-cocone-constant-type-family-cocone =
+    is-equiv-is-invertible
+      ( cocone-dependent-cocone-constant-type-family)
+      ( is-section-cocone-dependent-cocone-constant-type-family)
+      ( is-retraction-cocone-dependent-cocone-constant-type-family)
+
+  compute-dependent-cocone-constant-type-family :
+    cocone f g Y ≃ dependent-cocone f g c (λ _ → Y)
+  compute-dependent-cocone-constant-type-family =
+    ( dependent-cocone-constant-type-family-cocone ,
+      is-equiv-dependent-cocone-constant-type-family-cocone)
+```
+
+### Computing the dependent cocone map on a constant type family
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
+  (f : S → A) (g : S → B) (c : cocone f g X) {Y : UU l5}
+  where
+
+  triangle-dependent-cocone-map-constant-type-family :
+    dependent-cocone-map f g c (λ _ → Y) ~
+    dependent-cocone-constant-type-family-cocone f g c ∘ cocone-map f g c
+  triangle-dependent-cocone-map-constant-type-family h =
+    eq-htpy-dependent-cocone f g c
+      ( λ _ → Y)
+      ( dependent-cocone-map f g c (λ _ → Y) h)
+      ( dependent-cocone-constant-type-family-cocone f g c (cocone-map f g c h))
+      ( ( refl-htpy) ,
+        ( refl-htpy) ,
+        ( λ s →
+          right-unit ∙
+          apd-constant-type-family h (coherence-square-cocone f g c s)))
+
+  triangle-dependent-cocone-map-constant-type-family' :
+    cocone-map f g c ~
+    cocone-dependent-cocone-constant-type-family f g c ∘
+    dependent-cocone-map f g c (λ _ → Y)
+  triangle-dependent-cocone-map-constant-type-family' h =
+    eq-htpy-cocone f g
+      ( cocone-map f g c h)
+      ( ( cocone-dependent-cocone-constant-type-family f g c
+          ( dependent-cocone-map f g c (λ _ → Y) h)))
+      ( ( refl-htpy) ,
+        ( refl-htpy) ,
+        ( λ s →
+          right-unit ∙
+          left-transpose-eq-concat
+            ( tr-constant-type-family
+              ( coherence-square-cocone f g c s)
+              ( pr1 (dependent-cocone-map f g c (λ _ → Y) h) (f s)))
+            ( ap h (coherence-square-cocone f g c s))
+            ( apd h (coherence-square-cocone f g c s))
+            ( inv
+              ( apd-constant-type-family h (coherence-square-cocone f g c s)))))
+```
+
+### The nondependent cocone map at `Y` is an equivalence if and only if the dependent cocone map at the constant type family `(λ _ → Y)` is
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
+  (f : S → A) (g : S → B) (c : cocone f g X) {Y : UU l5}
+  where
+
+  is-equiv-cocone-map-is-equiv-dependent-cocone-map-constant-type-family :
+    is-equiv (dependent-cocone-map f g c (λ _ → Y)) →
+    is-equiv (cocone-map f g c)
+  is-equiv-cocone-map-is-equiv-dependent-cocone-map-constant-type-family =
+    is-equiv-top-map-triangle
+      ( dependent-cocone-map f g c (λ _ → Y))
+      ( dependent-cocone-constant-type-family-cocone f g c)
+      ( cocone-map f g c)
+      ( triangle-dependent-cocone-map-constant-type-family f g c)
+      ( is-equiv-dependent-cocone-constant-type-family-cocone f g c)
+
+  is-equiv-dependent-cocone-map-constant-type-family-is-equiv-cocone-map :
+    is-equiv (cocone-map f g c) →
+    is-equiv (dependent-cocone-map f g c (λ _ → Y))
+  is-equiv-dependent-cocone-map-constant-type-family-is-equiv-cocone-map H =
+    is-equiv-left-map-triangle
+      ( dependent-cocone-map f g c (λ _ → Y))
+      ( dependent-cocone-constant-type-family-cocone f g c)
+      ( cocone-map f g c)
+      ( triangle-dependent-cocone-map-constant-type-family f g c)
+      ( H)
+      ( is-equiv-dependent-cocone-constant-type-family-cocone f g c)
+```
+
+### Computing with the characterization of identifications of dependent cocones on constant type families over a fixed cocone
+
+If two dependent cocones on a constant type family are homotopic, then so are
+their nondependent counterparts.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B)
+  {X : UU l4} (c : cocone f g X)
+  (Y : UU l5)
+  where
+
+  coherence-htpy-cocone-dependent-cocone-coherence-htpy-dependent-cocone-constant-type-family :
+    ( d d' : dependent-cocone f g c (λ _ → Y)) →
+    ( K :
+      horizontal-map-dependent-cocone f g c (λ _ → Y) d ~
+      horizontal-map-dependent-cocone f g c (λ _ → Y) d')
+    ( L :
+      vertical-map-dependent-cocone f g c (λ _ → Y) d ~
+      vertical-map-dependent-cocone f g c (λ _ → Y) d')
+    ( H : coherence-htpy-dependent-cocone f g c (λ _ → Y) d d' K L) →
+    statement-coherence-htpy-cocone f g
+      ( cocone-dependent-cocone-constant-type-family f g c d)
+      ( cocone-dependent-cocone-constant-type-family f g c d')
+      ( K)
+      ( L)
+  coherence-htpy-cocone-dependent-cocone-coherence-htpy-dependent-cocone-constant-type-family
+    d d' K L H x =
+    ( left-whisker-concat-coherence-square-identifications
+      ( inv
+        ( tr-constant-type-family
+          ( coherence-square-cocone f g c x)
+          ( horizontal-map-dependent-cocone f g c (λ _ → Y) d (f x))))
+      ( ap (tr (λ _ → Y) (coherence-square-cocone f g c x)) (K (f x)))
+      ( coherence-square-dependent-cocone f g c (λ _ → Y) d x)
+      ( coherence-square-dependent-cocone f g c (λ _ → Y) d' x)
+      ( L (g x))
+      ( H x)) ∙
+    ( ap
+      ( _∙ coherence-square-dependent-cocone f g c (λ _ → Y) d' x)
+      ( naturality-inv-tr-constant-type-family
+        ( coherence-square-cocone f g c x)
+        ( K (f x)))) ∙
+    ( assoc
+      ( K (f x))
+      ( inv
+        ( tr-constant-type-family
+          ( coherence-square-cocone f g c x)
+          ( horizontal-map-dependent-cocone f g c (λ _ → Y) d' (f x))))
+      ( coherence-square-dependent-cocone f g c (λ _ → Y) d' x))
+```
+
+If the dependent cocones on constant type families constructed from nondependent
+cocones are homotopic, then so are the nondependent cocones.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B)
+  {X : UU l4} {Y : UU l5}
+  where
+
+  coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family :
+    (c : cocone f g X)
+    (d d' : cocone f g Y) →
+    ( K : horizontal-map-cocone f g d ~ horizontal-map-cocone f g d')
+    ( L : vertical-map-cocone f g d ~ vertical-map-cocone f g d') →
+    coherence-htpy-dependent-cocone f g c (λ _ → Y)
+      ( dependent-cocone-constant-type-family-cocone f g c d)
+      ( dependent-cocone-constant-type-family-cocone f g c d')
+      ( K)
+      ( L) →
+    statement-coherence-htpy-cocone f g
+      ( d)
+      ( d')
+      ( K)
+      ( L)
+  coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family
+    c d d' K L H x =
+    is-injective-concat
+      ( tr-constant-type-family
+        ( coherence-square-cocone f g c x)
+        ( horizontal-map-cocone f g d (f x)))
+      ( ( inv
+          ( assoc
+            ( tr-constant-type-family
+              ( coherence-square-cocone f g c x)
+              ( horizontal-map-cocone f g d (f x)))
+            ( coherence-square-cocone f g d x)
+            ( L (g x)))) ∙
+        ( H x) ∙
+        ( right-whisker-concat-coherence-square-identifications
+          ( tr-constant-type-family
+            ( coherence-square-cocone f g c x)
+            ( horizontal-map-cocone f g d (f x)))
+          ( ap (tr (λ _ → Y) (coherence-square-cocone f g c x)) (K (f x)))
+          ( K (f x))
+          ( tr-constant-type-family
+            ( coherence-square-cocone f g c x)
+            ( horizontal-map-cocone f g d' (f x)))
+          ( inv
+            ( naturality-tr-constant-type-family
+              ( coherence-square-cocone f g c x)
+              ( K (f x))))
+          ( coherence-square-cocone f g d' x)))
+```
diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-pushouts.lagda.md
index 6b4ddfae4b..eb89f7ca3b 100644
--- a/src/synthetic-homotopy-theory/dependent-universal-property-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-universal-property-pushouts.lagda.md
@@ -19,6 +19,7 @@ open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.retractions
 open import foundation.standard-pullbacks
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
@@ -88,25 +89,27 @@ abstract
 #### The induction principle of pushouts implies the dependent universal property of pushouts
 
 ```agda
-htpy-eq-dependent-cocone-map :
-  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
-  ( f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
-  ( H : induction-principle-pushout l f g c)
-  { P : X → UU l} (h h' : (x : X) → P x) →
-  dependent-cocone-map f g c P h ＝ dependent-cocone-map f g c P h' → h ~ h'
-htpy-eq-dependent-cocone-map f g c ind-c {P} h h' p =
-  ind-induction-principle-pushout f g c ind-c
-    ( λ x → Id (h x) (h' x))
-    ( pair
-      ( horizontal-htpy-eq-dependent-cocone f g c P
-        ( dependent-cocone-map f g c P h)
-        ( dependent-cocone-map f g c P h')
-        ( p))
-      ( pair
+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
+
+  htpy-eq-dependent-cocone-map :
+    { l : Level} →
+    induction-principle-pushout l f g c →
+    { P : X → UU l} (h h' : (x : X) → P x) →
+    dependent-cocone-map f g c P h ＝ dependent-cocone-map f g c P h' → h ~ h'
+  htpy-eq-dependent-cocone-map ind-c {P} h h' p =
+    ind-induction-principle-pushout f g c ind-c
+      ( λ x → h x ＝ h' x)
+      ( ( horizontal-htpy-eq-dependent-cocone f g c P
+          ( dependent-cocone-map f g c P h)
+          ( dependent-cocone-map f g c P h')
+          ( p)) ,
         ( vertical-htpy-eq-dependent-cocone f g c P
           ( dependent-cocone-map f g c P h)
           ( dependent-cocone-map f g c P h')
-          ( p))
+          ( p)) ,
         ( λ s →
           map-compute-dependent-identification-eq-value h h'
             ( coherence-square-cocone f g c s)
@@ -124,28 +127,34 @@ htpy-eq-dependent-cocone-map f g c ind-c {P} h h' p =
               ( dependent-cocone-map f g c P h)
               ( dependent-cocone-map f g c P h')
               ( p)
-              ( s)))))
+              ( s))))
 
-dependent-universal-property-pushout-induction-principle-pushout :
-  {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) →
-  ({l : Level} → induction-principle-pushout l f g c) →
-  ({l : Level} → dependent-universal-property-pushout l f g c)
-dependent-universal-property-pushout-induction-principle-pushout
-  f g c ind-c P =
-  is-equiv-is-invertible
-    ( ind-induction-principle-pushout f g c ind-c P)
-    ( pr2 (ind-c P))
-    ( λ h →
-      eq-htpy
-        ( htpy-eq-dependent-cocone-map f g c
+  is-retraction-ind-induction-principle-pushout :
+    (H : {l : Level} → induction-principle-pushout l f g c) →
+    {l : Level} (P : X → UU l) →
+    is-retraction
+      ( dependent-cocone-map f g c P)
+      ( ind-induction-principle-pushout f g c H P)
+  is-retraction-ind-induction-principle-pushout ind-c P h =
+    eq-htpy
+      ( htpy-eq-dependent-cocone-map
+        ( ind-c)
+        ( ind-induction-principle-pushout f g c
           ( ind-c)
-          ( ind-induction-principle-pushout f g c
-            ( ind-c)
-            ( P)
-            ( dependent-cocone-map f g c P h))
-          ( h)
-          ( pr2 (ind-c P) (dependent-cocone-map f g c P h))))
+          ( P)
+          ( dependent-cocone-map f g c P h))
+        ( h)
+        ( eq-compute-ind-induction-principle-pushout f g c ind-c P
+          ( dependent-cocone-map f g c P h)))
+
+  dependent-universal-property-pushout-induction-principle-pushout :
+    ({l : Level} → induction-principle-pushout l f g c) →
+    ({l : Level} → dependent-universal-property-pushout l f g c)
+  dependent-universal-property-pushout-induction-principle-pushout ind-c P =
+    is-equiv-is-invertible
+      ( ind-induction-principle-pushout f g c ind-c P)
+      ( eq-compute-ind-induction-principle-pushout f g c ind-c P)
+      ( is-retraction-ind-induction-principle-pushout ind-c P)
 ```
 
 #### The dependent universal property of pushouts implies the induction principle of pushouts
diff --git a/src/synthetic-homotopy-theory/induction-principle-pushouts.lagda.md b/src/synthetic-homotopy-theory/induction-principle-pushouts.lagda.md
index 431c649a01..f32afe4414 100644
--- a/src/synthetic-homotopy-theory/induction-principle-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/induction-principle-pushouts.lagda.md
@@ -61,6 +61,11 @@ module _
   ind-induction-principle-pushout : dependent-cocone f g c P → (x : X) → P x
   ind-induction-principle-pushout = pr1 (ind-c P)
 
+  eq-compute-ind-induction-principle-pushout :
+    (h : dependent-cocone f g c P) →
+    dependent-cocone-map f g c P (ind-induction-principle-pushout h) ＝ h
+  eq-compute-ind-induction-principle-pushout = pr2 (ind-c P)
+
   compute-ind-induction-principle-pushout :
     (h : dependent-cocone f g c P) →
     htpy-dependent-cocone f g c P
@@ -70,29 +75,29 @@ module _
     htpy-eq-dependent-cocone f g c P
       ( dependent-cocone-map f g c P (ind-induction-principle-pushout h))
       ( h)
-      ( pr2 (ind-c P) h)
+      ( eq-compute-ind-induction-principle-pushout h)
 
-  left-compute-ind-induction-principle-pushout :
+  compute-horizontal-map-ind-induction-principle-pushout :
     ( h : dependent-cocone f g c P) (a : A) →
     ind-induction-principle-pushout h (horizontal-map-cocone f g c a) ＝
     horizontal-map-dependent-cocone f g c P h a
-  left-compute-ind-induction-principle-pushout h =
+  compute-horizontal-map-ind-induction-principle-pushout h =
     pr1 (compute-ind-induction-principle-pushout h)
 
-  right-compute-ind-induction-principle-pushout :
+  compute-vertical-map-ind-induction-principle-pushout :
     ( h : dependent-cocone f g c P) (b : B) →
     ind-induction-principle-pushout h (vertical-map-cocone f g c b) ＝
     vertical-map-dependent-cocone f g c P h b
-  right-compute-ind-induction-principle-pushout h =
+  compute-vertical-map-ind-induction-principle-pushout h =
     pr1 (pr2 (compute-ind-induction-principle-pushout h))
 
-  path-compute-ind-induction-principle-pushout :
+  compute-glue-ind-induction-principle-pushout :
     (h : dependent-cocone f g c P) →
     coherence-htpy-dependent-cocone f g c P
       ( dependent-cocone-map f g c P (ind-induction-principle-pushout h))
       ( h)
-      ( left-compute-ind-induction-principle-pushout h)
-      ( right-compute-ind-induction-principle-pushout h)
-  path-compute-ind-induction-principle-pushout h =
+      ( compute-horizontal-map-ind-induction-principle-pushout h)
+      ( compute-vertical-map-ind-induction-principle-pushout h)
+  compute-glue-ind-induction-principle-pushout h =
     pr2 (pr2 (compute-ind-induction-principle-pushout h))
 ```
diff --git a/src/synthetic-homotopy-theory/joins-of-types.lagda.md b/src/synthetic-homotopy-theory/joins-of-types.lagda.md
index 36a860e028..0ef22c971d 100644
--- a/src/synthetic-homotopy-theory/joins-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/joins-of-types.lagda.md
@@ -28,6 +28,7 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.dependent-cocones-under-spans
 open import synthetic-homotopy-theory.pushouts
 open import synthetic-homotopy-theory.universal-property-pushouts
 ```
@@ -36,16 +37,17 @@ open import synthetic-homotopy-theory.universal-property-pushouts
 
 ## Idea
 
-The **join** of `A` and `B` is the
+The {{#concept "join" Disambiguation="of types" Agda=_*_}} of `A` and `B` is the
 [pushout](synthetic-homotopy-theory.pushouts.md) of the
 [span](foundation.spans.md) `A ← A × B → B`.
 
-## Definition
+## Definitions
+
+### The standard join of types
 
 ```agda
-join :
-  {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2)
-join A B = pushout (pr1 {A = A} {B = λ _ → B}) pr2
+join : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2)
+join A B = pushout {A = A} {B = B} pr1 pr2
 
 infixr 15 _*_
 _*_ = join
@@ -54,45 +56,93 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2}
   where
 
-  cocone-join : cocone (pr1 {A = A} {B = λ _ → B}) pr2 (A * B)
+  cocone-join : cocone {A = A} {B = B} pr1 pr2 (A * B)
   cocone-join = cocone-pushout pr1 pr2
 
+  inl-join : A → A * B
+  inl-join = horizontal-map-cocone pr1 pr2 cocone-join
+
+  inr-join : B → A * B
+  inr-join = vertical-map-cocone pr1 pr2 cocone-join
+
+  glue-join : (t : A × B) → inl-join (pr1 t) ＝ inr-join (pr2 t)
+  glue-join = coherence-square-cocone pr1 pr2 cocone-join
+```
+
+### The universal property of the join
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
   up-join :
-    {l : Level} → universal-property-pushout l pr1 pr2 (cocone-join)
+    {l : Level} → universal-property-pushout l {A = A} {B} pr1 pr2 cocone-join
   up-join = up-pushout pr1 pr2
 
   equiv-up-join :
     {l : Level} (X : UU l) → (A * B → X) ≃ cocone pr1 pr2 X
   equiv-up-join = equiv-up-pushout pr1 pr2
+```
 
-  inl-join : A → A * B
-  inl-join = pr1 cocone-join
+### The dependent cogap map of the join
 
-  inr-join : B → A * B
-  inr-join = pr1 (pr2 cocone-join)
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {P : A * B → UU l3}
+  (c : dependent-cocone pr1 pr2 cocone-join P)
+  where
 
-  glue-join : (t : A × B) → inl-join (pr1 t) ＝ inr-join (pr2 t)
-  glue-join = pr2 (pr2 cocone-join)
+  dependent-cogap-join : (x : A * B) → P x
+  dependent-cogap-join = dependent-cogap pr1 pr2 {P = P} c
+
+  compute-inl-dependent-cogap-join :
+    dependent-cogap-join ∘ inl-join ~
+    horizontal-map-dependent-cocone pr1 pr2 cocone-join P c
+  compute-inl-dependent-cogap-join = compute-inl-dependent-cogap pr1 pr2 c
+
+  compute-inr-dependent-cogap-join :
+    dependent-cogap-join ∘ inr-join ~
+    vertical-map-dependent-cocone pr1 pr2 cocone-join P c
+  compute-inr-dependent-cogap-join = compute-inr-dependent-cogap pr1 pr2 c
+
+  compute-glue-dependent-cogap-join :
+    coherence-htpy-dependent-cocone pr1 pr2 cocone-join P
+      ( dependent-cocone-map pr1 pr2 cocone-join P dependent-cogap-join)
+      ( c)
+      ( compute-inl-dependent-cogap-join)
+      ( compute-inr-dependent-cogap-join)
+  compute-glue-dependent-cogap-join = compute-glue-dependent-cogap pr1 pr2 c
+```
+
+### The cogap map of the join
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
 
   cogap-join :
     {l3 : Level} (X : UU l3) → cocone pr1 pr2 X → A * B → X
-  cogap-join X = map-inv-is-equiv (up-join X)
+  cogap-join X = cogap pr1 pr2
 
   compute-inl-cogap-join :
     {l3 : Level} {X : UU l3} (c : cocone pr1 pr2 X) →
-    ( cogap-join X c ∘ inl-join) ~ horizontal-map-cocone pr1 pr2 c
+    cogap-join X c ∘ inl-join ~ horizontal-map-cocone pr1 pr2 c
   compute-inl-cogap-join = compute-inl-cogap pr1 pr2
 
   compute-inr-cogap-join :
     {l3 : Level} {X : UU l3} (c : cocone pr1 pr2 X) →
-    ( cogap-join X c ∘ inr-join) ~ vertical-map-cocone pr1 pr2 c
+    cogap-join X c ∘ inr-join ~ vertical-map-cocone pr1 pr2 c
   compute-inr-cogap-join = compute-inr-cogap pr1 pr2
 
   compute-glue-cogap-join :
     {l3 : Level} {X : UU l3} (c : cocone pr1 pr2 X) →
-    ( ( cogap-join X c ·l coherence-square-cocone pr1 pr2 cocone-join) ∙h
-      ( compute-inr-cogap-join c ·r pr2)) ~
-    ( compute-inl-cogap-join c ·r pr1) ∙h coherence-square-cocone pr1 pr2 c
+    statement-coherence-htpy-cocone pr1 pr2
+      ( cocone-map pr1 pr2 cocone-join (cogap-join X c))
+      ( c)
+      ( compute-inl-cogap-join c)
+      ( compute-inr-cogap-join c)
   compute-glue-cogap-join = compute-glue-cogap pr1 pr2
 ```
 
@@ -271,15 +321,15 @@ module _
     is-proof-irrelevant A → is-proof-irrelevant B → is-proof-irrelevant (A * B)
   is-proof-irrelevant-join-is-proof-irrelevant
     is-proof-irrelevant-A is-proof-irrelevant-B =
-    cogap-join (is-contr (A * B))
-      ( pair
-        ( left-zero-law-join-is-contr A B ∘ is-proof-irrelevant-A)
-        ( pair
-          ( right-zero-law-join-is-contr A B ∘ is-proof-irrelevant-B)
-          ( λ (a , b) → center
+    cogap-join
+      ( is-contr (A * B))
+      ( ( left-zero-law-join-is-contr A B ∘ is-proof-irrelevant-A) ,
+        ( right-zero-law-join-is-contr A B ∘ is-proof-irrelevant-B) ,
+        ( λ (a , b) →
+          center
             ( is-property-is-contr
               ( left-zero-law-join-is-contr A B (is-proof-irrelevant-A a))
-              ( right-zero-law-join-is-contr A B (is-proof-irrelevant-B b))))))
+              ( right-zero-law-join-is-contr A B (is-proof-irrelevant-B b)))))
 
   is-prop-join-is-prop :
     is-prop A → is-prop B → is-prop (A * B)
@@ -373,14 +423,15 @@ module _
       ( map-disjunction-join-Prop)
       ( ( λ _ → eq-is-prop (is-prop-disjunction-Prop A B)) ,
         ( λ _ → eq-is-prop (is-prop-disjunction-Prop A B)) ,
-        ( λ (a , b) → eq-is-contr
-          ( is-prop-disjunction-Prop A B
-            ( horizontal-map-cocone pr1 pr2
-              ( cocone-map pr1 pr2
-                ( cocone-join)
-                ( map-disjunction-join-Prop))
-              ( a))
-            ( vertical-map-cocone pr1 pr2 cocone-disjunction b))))
+        ( λ (a , b) →
+          eq-is-contr
+            ( is-prop-disjunction-Prop A B
+              ( horizontal-map-cocone pr1 pr2
+                ( cocone-map pr1 pr2
+                  ( cocone-join)
+                  ( map-disjunction-join-Prop))
+                ( a))
+              ( vertical-map-cocone pr1 pr2 cocone-disjunction b))))
       ( is-equiv-map-disjunction-join-Prop)
       ( up-join)
 ```
diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index bb55f0d156..9fcda8bd15 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -7,8 +7,10 @@ module synthetic-homotopy-theory.pushouts where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-squares-of-maps
+open import foundation.constant-type-families
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.fibers-of-maps
@@ -19,12 +21,18 @@ open import foundation.identity-types
 open import foundation.propositions
 open import foundation.retractions
 open import foundation.sections
+open import foundation.transport-along-homotopies
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import reflection.erasing-equality
 
 open import synthetic-homotopy-theory.cocones-under-spans
 open import synthetic-homotopy-theory.dependent-cocones-under-spans
 open import synthetic-homotopy-theory.dependent-universal-property-pushouts
 open import synthetic-homotopy-theory.flattening-lemma-pushouts
+open import synthetic-homotopy-theory.induction-principle-pushouts
 open import synthetic-homotopy-theory.universal-property-pushouts
 ```
 
@@ -77,6 +85,8 @@ Examples of pushouts include
 
 ## Postulates
 
+### The standard pushout type
+
 We will assume that for any span
 
 ```text
@@ -114,40 +124,282 @@ cocone-pushout :
 pr1 (cocone-pushout f g) = inl-pushout f g
 pr1 (pr2 (cocone-pushout f g)) = inr-pushout f g
 pr2 (pr2 (cocone-pushout f g)) = glue-pushout f g
+```
 
-postulate
-  up-pushout :
-    {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
-    (f : S → A) (g : S → B) →
-    universal-property-pushout l4 f g (cocone-pushout f g)
+### The dependent cogap map
 
-equiv-up-pushout :
+We postulate the constituents of a section of
+`dependent-cocone-map f g (cocone-pushout f g)` up to homotopy of dependent
+cocones. This is, assuming
+[function extensionality](foundation.function-extensionality.md), precisely the
+data of the induction principle of pushouts. We write out each component
+separately to accomodate
+[optional rewrite rules for the standard pushouts](synthetic-homotopy-theory.rewriting-pushouts.md).
+
+```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) → (pushout f g → X) ≃ (cocone f g X)
-pr1 (equiv-up-pushout f g X) = cocone-map f g (cocone-pushout f g)
-pr2 (equiv-up-pushout f g X) = up-pushout f g X
+  (f : S → A) (g : S → B) {P : pushout f g → UU l4}
+  (c : dependent-cocone f g (cocone-pushout f g) P)
+  where
+
+  postulate
+    dependent-cogap : (x : pushout f g) → P x
+
+  compute-inl-dependent-cogap :
+    (a : A) →
+    dependent-cogap (inl-pushout f g a) ＝
+    horizontal-map-dependent-cocone f g (cocone-pushout f g) P c a
+  compute-inl-dependent-cogap a = primEraseEquality compute-inl-dependent-cogap'
+    where postulate
+      compute-inl-dependent-cogap' :
+        dependent-cogap (inl-pushout f g a) ＝
+        horizontal-map-dependent-cocone f g (cocone-pushout f g) P c a
+
+  compute-inr-dependent-cogap :
+    (b : B) →
+    dependent-cogap (inr-pushout f g b) ＝
+    vertical-map-dependent-cocone f g (cocone-pushout f g) P c b
+  compute-inr-dependent-cogap b = primEraseEquality compute-inr-dependent-cogap'
+    where postulate
+      compute-inr-dependent-cogap' :
+        dependent-cogap (inr-pushout f g b) ＝
+        vertical-map-dependent-cocone f g (cocone-pushout f g) P c b
+
+  postulate
+    compute-glue-dependent-cogap :
+      coherence-htpy-dependent-cocone f g
+        ( cocone-pushout f g)
+        ( P)
+        ( dependent-cocone-map f g (cocone-pushout f g) P dependent-cogap)
+        ( c)
+        ( compute-inl-dependent-cogap)
+        ( compute-inr-dependent-cogap)
+
+  htpy-compute-dependent-cogap :
+    htpy-dependent-cocone f g
+      ( cocone-pushout f g)
+      ( P)
+      ( dependent-cocone-map f g (cocone-pushout f g) P dependent-cogap)
+      ( c)
+  htpy-compute-dependent-cogap =
+    ( compute-inl-dependent-cogap ,
+      compute-inr-dependent-cogap ,
+      compute-glue-dependent-cogap)
 ```
 
 ## Definitions
 
+### The induction principle of standard pushouts
+
+```agda
+module _
+  {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B)
+  where
+
+  is-section-dependent-cogap :
+    {l : Level} {P : pushout f g → UU l} →
+    is-section
+      ( dependent-cocone-map f g (cocone-pushout f g) P)
+      ( dependent-cogap f g)
+  is-section-dependent-cogap {P = P} c =
+    eq-htpy-dependent-cocone f g
+      ( cocone-pushout f g)
+      ( P)
+      ( dependent-cocone-map f g (cocone-pushout f g) P (dependent-cogap f g c))
+      ( c)
+      ( htpy-compute-dependent-cogap f g c)
+
+  induction-principle-pushout' :
+    {l : Level} → induction-principle-pushout l f g (cocone-pushout f g)
+  induction-principle-pushout' P =
+    ( dependent-cogap f g , is-section-dependent-cogap)
+
+  is-retraction-dependent-cogap :
+    {l : Level} {P : pushout f g → UU l} →
+    is-retraction
+      ( dependent-cocone-map f g (cocone-pushout f g) P)
+      ( dependent-cogap f g)
+  is-retraction-dependent-cogap {P = P} =
+    is-retraction-ind-induction-principle-pushout f g
+      ( cocone-pushout f g)
+      ( induction-principle-pushout')
+      ( P)
+```
+
+### The dependent universal property of standard pushouts
+
+```agda
+module _
+  {l1 l2 l3 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B)
+  where
+
+  dup-pushout :
+    dependent-universal-property-pushout l f g (cocone-pushout f g)
+  dup-pushout =
+    dependent-universal-property-pushout-induction-principle-pushout f g
+      ( cocone-pushout f g)
+      ( induction-principle-pushout' f g)
+
+  equiv-dup-pushout :
+    (P : pushout f g → UU l) →
+    ((x : pushout f g) → P x) ≃ dependent-cocone f g (cocone-pushout f g) P
+  pr1 (equiv-dup-pushout P) = dependent-cocone-map f g (cocone-pushout f g) P
+  pr2 (equiv-dup-pushout P) = dup-pushout P
+```
+
 ### The cogap map
 
+We define `cogap` and its computation rules in terms of `dependent-cogap` to
+ensure the proper computational behaviour when in the presence of strict
+computation laws on the point constructors of the standard pushouts.
+
 ```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}
+  (f : S → A) (g : S → B) {X : UU l4}
   where
 
   cogap : cocone f g X → pushout f g → X
-  cogap = map-inv-equiv (equiv-up-pushout f g X)
+  cogap =
+    dependent-cogap f g ∘
+    dependent-cocone-constant-type-family-cocone f g (cocone-pushout f g)
 
   is-section-cogap : is-section (cocone-map f g (cocone-pushout f g)) cogap
-  is-section-cogap = is-section-map-inv-equiv (equiv-up-pushout f g X)
+  is-section-cogap =
+    ( ( triangle-dependent-cocone-map-constant-type-family' f g
+        ( cocone-pushout f g)) ·r
+      ( cogap)) ∙h
+    ( ( cocone-dependent-cocone-constant-type-family f g
+        ( cocone-pushout f g)) ·l
+      ( is-section-dependent-cogap f g) ·r
+      ( dependent-cocone-constant-type-family-cocone f g
+        ( cocone-pushout f g))) ∙h
+    ( is-retraction-cocone-dependent-cocone-constant-type-family f g
+      ( cocone-pushout f g))
 
   is-retraction-cogap :
     is-retraction (cocone-map f g (cocone-pushout f g)) cogap
   is-retraction-cogap =
-    is-retraction-map-inv-equiv (equiv-up-pushout f g X)
+    ( ( cogap) ·l
+      ( triangle-dependent-cocone-map-constant-type-family' f g
+        ( cocone-pushout f g))) ∙h
+    ( ( dependent-cogap f g) ·l
+      ( is-section-cocone-dependent-cocone-constant-type-family f g
+        ( cocone-pushout f g)) ·r
+      ( dependent-cocone-map f g (cocone-pushout f g) (λ _ → X))) ∙h
+    ( is-retraction-dependent-cogap f g)
+```
+
+### The universal property of standard pushouts
+
+```agda
+up-pushout :
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B) →
+  universal-property-pushout l4 f g (cocone-pushout f g)
+up-pushout f g P =
+  is-equiv-is-invertible
+    ( cogap f g)
+    ( is-section-cogap f g)
+    ( is-retraction-cogap f g)
+
+equiv-up-pushout :
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B) (X : UU l4) → (pushout f g → X) ≃ (cocone f g X)
+pr1 (equiv-up-pushout f g X) = cocone-map f g (cocone-pushout f g)
+pr2 (equiv-up-pushout f g X) = up-pushout f g X
+```
+
+### Computation with the cogap map
+
+We define the computation witnesses for the cogap map in terms of the
+computation witnesses for the dependent cogap map so that when
+[rewriting is enabled for pushouts](synthetic-homotopy-theory.rewriting-pushouts.md),
+these witnesses reduce to reflexivities.
+
+```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
+
+  compute-inl-cogap :
+    cogap f g c ∘ inl-pushout f g ~ horizontal-map-cocone f g c
+  compute-inl-cogap =
+    compute-inl-dependent-cogap f g
+      ( dependent-cocone-constant-type-family-cocone f g (cocone-pushout f g) c)
+
+  compute-inr-cogap :
+    cogap f g c ∘ inr-pushout f g ~ vertical-map-cocone f g c
+  compute-inr-cogap =
+    compute-inr-dependent-cogap f g
+      ( dependent-cocone-constant-type-family-cocone f g (cocone-pushout f g) c)
+```
+
+<!-- TODO: find the right infrastructure to make the proof below just an application of a more general construction. Note that this is very almost `coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family`, but an `apd-constant-type-family` has snuck its way into the proof Issue#1120 -->
+
+```agda
+  abstract
+    compute-glue-cogap :
+      statement-coherence-htpy-cocone f g
+        ( cocone-map f g (cocone-pushout f g) (cogap f g c))
+        ( c)
+        ( compute-inl-cogap)
+        ( compute-inr-cogap)
+    compute-glue-cogap x =
+      is-injective-concat
+        ( tr-constant-type-family
+          ( glue-pushout f g x)
+          ( cogap f g c ((inl-pushout f g ∘ f) x)))
+        ( ( inv
+            ( assoc
+              ( tr-constant-type-family
+                ( glue-pushout f g x)
+                ( cogap f g c
+                  ( horizontal-map-cocone f g (cocone-pushout f g) (f x))))
+              ( ap (cogap f g c) (glue-pushout f g x))
+              ( compute-inr-cogap (g x)))) ∙
+          ( ap
+            ( _∙ compute-inr-cogap (g x))
+            ( inv
+              ( apd-constant-type-family (cogap f g c) (glue-pushout f g x)))) ∙
+          ( compute-glue-dependent-cogap f g
+            ( dependent-cocone-constant-type-family-cocone f g
+              ( cocone-pushout f g)
+              ( c))
+            ( x)) ∙
+          ( inv
+            ( assoc
+              ( ap
+                ( tr (λ _ → X) (glue-pushout f g x))
+                ( compute-inl-cogap (f x)))
+              ( tr-constant-type-family
+                ( glue-pushout f g x)
+                ( pr1 c (f x)))
+              ( coherence-square-cocone f g c x))) ∙
+          ( ap
+            ( _∙ coherence-square-cocone f g c x)
+            ( inv
+              ( naturality-tr-constant-type-family
+                ( glue-pushout f g x)
+                ( compute-inl-cogap (f x))))) ∙
+            ( assoc
+              ( tr-constant-type-family
+                ( glue-pushout f g x)
+                ( cogap f g c (inl-pushout f g (f x))))
+              ( compute-inl-cogap (f x))
+              ( coherence-square-cocone f g c x)))
+
+  htpy-compute-cogap :
+    htpy-cocone f g
+      ( cocone-map f g (cocone-pushout f g) (cogap f g c))
+      ( c)
+  htpy-compute-cogap =
+    ( compute-inl-cogap , compute-inr-cogap , compute-glue-cogap)
 ```
 
 ### The small predicate of being a pushout cocone
@@ -207,76 +459,6 @@ module _
       ( up-pushout f g)
 ```
 
-### The pushout of a span has the dependent universal property
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
-  (f : S → A) (g : S → B)
-  where
-
-  dup-pushout :
-    dependent-universal-property-pushout l4 f g (cocone-pushout f g)
-  dup-pushout =
-    dependent-universal-property-universal-property-pushout
-    ( f)
-    ( g)
-    ( cocone-pushout f g)
-    ( up-pushout f g)
-
-  equiv-dup-pushout :
-    (P : pushout f g → UU l4) →
-    ((x : pushout f g) → P x) ≃ dependent-cocone f g (cocone-pushout f g) P
-  pr1 (equiv-dup-pushout P) =
-    dependent-cocone-map f g (cocone-pushout f g) P
-  pr2 (equiv-dup-pushout P) =
-    dup-pushout P
-```
-
-### Computation with the cogap map
-
-```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
-
-  compute-inl-cogap :
-    ( a : A) → cogap f g c (inl-pushout f g a) ＝ horizontal-map-cocone f g c a
-  compute-inl-cogap =
-    horizontal-htpy-cocone-map-universal-property-pushout
-      ( f)
-      ( g)
-      ( cocone-pushout f g)
-      ( up-pushout f g)
-      ( c)
-
-  compute-inr-cogap :
-    ( b : B) → cogap f g c (inr-pushout f g b) ＝ vertical-map-cocone f g c b
-  compute-inr-cogap =
-    vertical-htpy-cocone-map-universal-property-pushout
-      ( f)
-      ( g)
-      ( cocone-pushout f g)
-      ( up-pushout f g)
-      ( c)
-
-  compute-glue-cogap :
-    statement-coherence-htpy-cocone f g
-      ( cocone-map f g (cocone-pushout f g) (cogap f g c))
-      ( c)
-      ( compute-inl-cogap)
-      ( compute-inr-cogap)
-  compute-glue-cogap =
-    coherence-htpy-cocone-map-universal-property-pushout
-      ( f)
-      ( g)
-      ( cocone-pushout f g)
-      ( up-pushout f g)
-      ( c)
-```
-
 ### Fibers of the cogap map
 
 We characterize the [fibers](foundation-core.fibers-of-maps.md) of the cogap map
diff --git a/src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md b/src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md
new file mode 100644
index 0000000000..af0fa511a5
--- /dev/null
+++ b/src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md
@@ -0,0 +1,90 @@
+# The recursion principle of pushouts
+
+```agda
+module synthetic-homotopy-theory.recursion-principle-pushouts where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.sections
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.dependent-cocones-under-spans
+```
+
+</details>
+
+## Idea
+
+The {{#concept "recursion principle of pushouts"}} asserts that for every type
+`Y` and [cocone](synthetic-homotopy-theory.cocones-under-spans.md) on a type
+`X`, the cocone map
+
+```text
+  cocone-map f g c Y : (X → Y) → cocone f g Y
+```
+
+has a [section](foundation.sections.md).
+
+## Definition
+
+### The recursion principle of pushouts
+
+```agda
+recursion-principle-pushout :
+  { l1 l2 l3 l4 : Level} →
+  { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
+  ( f : S → A) (g : S → B) (c : cocone f g X) →
+  UUω
+recursion-principle-pushout f g c =
+  {l : Level} {Y : UU l} → section (cocone-map f g {Y = Y} c)
+
+module _
+  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
+  ( f : S → A) (g : S → B) (c : cocone f g X)
+  ( rec-c : recursion-principle-pushout f g c)
+  ( Y : UU l)
+  where
+
+  rec-recursion-principle-pushout : cocone f g Y → X → Y
+  rec-recursion-principle-pushout = pr1 rec-c
+
+  compute-rec-recursion-principle-pushout :
+    (h : cocone f g Y) →
+    htpy-cocone f g
+      ( cocone-map f g c (rec-recursion-principle-pushout h))
+      ( h)
+  compute-rec-recursion-principle-pushout h =
+    htpy-eq-cocone f g
+      ( cocone-map f g c (rec-recursion-principle-pushout h))
+      ( h)
+      ( pr2 rec-c h)
+
+  compute-horizontal-map-rec-recursion-principle-pushout :
+    ( h : cocone f g Y) (a : A) →
+    rec-recursion-principle-pushout h (horizontal-map-cocone f g c a) ＝
+    horizontal-map-cocone f g h a
+  compute-horizontal-map-rec-recursion-principle-pushout h =
+    pr1 (compute-rec-recursion-principle-pushout h)
+
+  compute-vertical-map-rec-recursion-principle-pushout :
+    ( h : cocone f g Y) (b : B) →
+    rec-recursion-principle-pushout h (vertical-map-cocone f g c b) ＝
+    vertical-map-cocone f g h b
+  compute-vertical-map-rec-recursion-principle-pushout h =
+    pr1 (pr2 (compute-rec-recursion-principle-pushout h))
+
+  compute-glue-rec-recursion-principle-pushout :
+    (h : cocone f g Y) →
+    statement-coherence-htpy-cocone f g
+      ( cocone-map f g c (rec-recursion-principle-pushout h))
+      ( h)
+      ( compute-horizontal-map-rec-recursion-principle-pushout h)
+      ( compute-vertical-map-rec-recursion-principle-pushout h)
+  compute-glue-rec-recursion-principle-pushout h =
+    pr2 (pr2 (compute-rec-recursion-principle-pushout h))
+```
diff --git a/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md b/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md
new file mode 100644
index 0000000000..5b471fe9ff
--- /dev/null
+++ b/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md
@@ -0,0 +1,120 @@
+# Rewriting rules for pushouts
+
+```agda
+{-# OPTIONS --rewriting #-}
+
+module synthetic-homotopy-theory.rewriting-pushouts where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import reflection.rewriting
+
+open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.dependent-cocones-under-spans
+open import synthetic-homotopy-theory.pushouts
+```
+
+</details>
+
+## Idea
+
+This module endows the eliminator of the
+[standard pushouts](synthetic-homotopy-theory.pushouts.md) `cogap` with strict
+computation rules on the point constructors using Agda's
+[rewriting](reflection.rewriting.md) functionality. This gives the strict
+equalities
+
+```text
+  cogap (inl-pushout f g a) ≐ horizontal-map-cocone f g c a
+```
+
+and
+
+```text
+  cogap (inr-pushout f g b) ≐ vertical-map-cocone f g c b.
+```
+
+More generally, strict computation rules for the dependent eliminator are
+enabled, giving the strict equalities
+
+```text
+  dependent-cogap (inl-pushout f g a) ≐
+  horizontal-map-dependent-cocone f g (cocone-pushout f g) P c a
+```
+
+and
+
+```text
+  dependent-cogap (inr-pushout f g b) ≐
+  vertical-map-dependent-cocone f g (cocone-pushout f g) P c b.
+```
+
+In addition, the pre-existing witnesses of these equalities:
+`compute-inl-dependent-cogap`, `compute-inr-dependent-cogap`, and their
+nondependent counterparts, reduce to `refl`. This is achieved using Agda's
+[equality erasure](reflection.erasing-equality.md) functionality.
+
+To enable these computation rules in your own formalizations, set the
+`--rewriting` option and import this module. Keep in mind, however, that we
+offer no way to selectively disable these rules, so if your module depends on
+any other module that imports this one, you will automatically also have
+rewriting for pushouts enabled.
+
+By default, we abstain from using rewrite rules in agda-unimath. However, we
+recognize their usefulness in, for instance, exploratory formalizations. Since
+formalizations with and without rewrite rules can coexist, there is no harm in
+providing these tools for those that see a need to use them. We do, however,
+emphasize that formalizations without the use of rewrite rules are preferred
+over those that do use them in the library, as the former can also be applied in
+other formalizations that do not enable rewrite rules.
+
+## Rewrite rules
+
+```agda
+{-# REWRITE compute-inl-dependent-cogap #-}
+{-# REWRITE compute-inr-dependent-cogap #-}
+```
+
+## Properties
+
+### Verifying the reduction behavior of the computation rules for the eliminators of standard pushouts
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B) {P : pushout f g → UU l4}
+  (d : dependent-cocone f g (cocone-pushout f g) P)
+  where
+
+  _ : compute-inl-dependent-cogap f g d ~ refl-htpy
+  _ = refl-htpy
+
+  _ : compute-inr-dependent-cogap f g d ~ refl-htpy
+  _ = refl-htpy
+
+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
+
+  _ : compute-inl-cogap f g c ~ refl-htpy
+  _ = refl-htpy
+
+  _ : compute-inr-cogap f g c ~ refl-htpy
+  _ = refl-htpy
+```
+
+## See also
+
+- For some discussion on strict computation rules for higher inductive types,
+  see the introduction to Section 6.2 of {{#cite UF13}}.
+
+## References
+
+{{#bibliography}}