From 8347f78dc1ef1148ec688bcdf728927eecb7ad7a Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 6 Feb 2024 16:05:20 +0100
Subject: [PATCH 01/29] add `rewriting` file

---
 src/reflection.lagda.md           |  1 +
 src/reflection/rewriting.lagda.md | 26 ++++++++++++++++++++++++++
 2 files changed, 27 insertions(+)
 create mode 100644 src/reflection/rewriting.lagda.md

diff --git a/src/reflection.lagda.md b/src/reflection.lagda.md
index b391840a82..a829a466d2 100644
--- a/src/reflection.lagda.md
+++ b/src/reflection.lagda.md
@@ -15,6 +15,7 @@ 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/rewriting.lagda.md b/src/reflection/rewriting.lagda.md
new file mode 100644
index 0000000000..226c018236
--- /dev/null
+++ b/src/reflection/rewriting.lagda.md
@@ -0,0 +1,26 @@
+# Rewriting
+
+```agda
+{-# OPTIONS --rewriting #-}
+
+module reflection.rewriting where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+```agda
+{-# BUILTIN REWRITE _＝_ #-}
+```
+
+## External links
+
+- [Rewriting](https://agda.readthedocs.io/en/latest/language/rewriting.html) at
+  Agda's documentation pages

From 06950c70708ee8bb96e2593ff65da43c8743ff5d Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 6 Feb 2024 16:23:47 +0100
Subject: [PATCH 02/29] stop :(

---
 Makefile                                       |  2 +-
 .../pushouts.lagda.md                          | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index db28a1e8ae..7ec651f1ea 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
 AGDARTS := +RTS -M4.0G -RTS
diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index bb55f0d156..0d3e09fb2a 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -1,6 +1,8 @@
 # Pushouts
 
 ```agda
+{-# OPTIONS --rewriting #-}
+
 module synthetic-homotopy-theory.pushouts where
 ```
 
@@ -21,6 +23,8 @@ open import foundation.retractions
 open import foundation.sections
 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.dependent-universal-property-pushouts
@@ -277,6 +281,20 @@ module _
       ( c)
 ```
 
+### Rewrite rules
+
+```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
+
+  rewrite-inl-cogap :
+    ( a : A) → cogap f g c (inl-pushout f g a) ＝ horizontal-map-cocone f g c a
+
+```
+
 ### Fibers of the cogap map
 
 We characterize the [fibers](foundation-core.fibers-of-maps.md) of the cogap map

From 29a53f63fb1118868134ba11b18ac0f4adfef079 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 15 Apr 2024 17:28:28 +0200
Subject: [PATCH 03/29] The recursion principle of pushouts

---
 src/synthetic-homotopy-theory.lagda.md        |  1 +
 .../recursion-principle-pushouts.lagda.md     | 96 +++++++++++++++++++
 2 files changed, 97 insertions(+)
 create mode 100644 src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 47dbab16c5..a21aae0963 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -78,6 +78,7 @@ 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.sections-descent-circle public
 open import synthetic-homotopy-theory.sequential-colimits public
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..bb2d041fdf
--- /dev/null
+++ b/src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md
@@ -0,0 +1,96 @@
+# 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.dependent-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).
+
+The fact that the recursion principle of pushouts is
+[logically equivalent](foundation.logical-equivalences.md) to the
+[universal property](synthetic-homotopy-theory.universal-property-pushouts.md)
+of pushouts is shown in
+[`universal-property-pushouts`](synthetic-homotopy-theory.universal-property-pushouts.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)
+
+  left-compute-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
+  left-compute-rec-recursion-principle-pushout h =
+    pr1 (compute-rec-recursion-principle-pushout h)
+
+  right-compute-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
+  right-compute-rec-recursion-principle-pushout h =
+    pr1 (pr2 (compute-rec-recursion-principle-pushout h))
+
+  path-compute-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)
+      ( left-compute-rec-recursion-principle-pushout h)
+      ( right-compute-rec-recursion-principle-pushout h)
+  path-compute-rec-recursion-principle-pushout h =
+    pr2 (pr2 (compute-rec-recursion-principle-pushout h))
+```

From fc236bea921bdb858b16177af9567d7422db5a0d Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 15 Apr 2024 19:27:11 +0200
Subject: [PATCH 04/29] Erasing equality primitive

---
 agda-unimath.agda-lib                    |  2 +-
 src/reflection.lagda.md                  |  1 +
 src/reflection/erasing-equality.lagda.md | 51 ++++++++++++++++++++++++
 3 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 src/reflection/erasing-equality.lagda.md

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/reflection.lagda.md b/src/reflection.lagda.md
index a829a466d2..1c00828e43 100644
--- a/src/reflection.lagda.md
+++ b/src/reflection.lagda.md
@@ -9,6 +9,7 @@ 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
diff --git a/src/reflection/erasing-equality.lagda.md b/src/reflection/erasing-equality.lagda.md
new file mode 100644
index 0000000000..85d1577a4c
--- /dev/null
+++ b/src/reflection/erasing-equality.lagda.md
@@ -0,0 +1,51 @@
+# 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 of 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
+in the expected way. Concretely, if the identification `β` defines a rewrite
+rule, and `β` is defined via `primEraseEqaulity`, then we have the strict
+equality `β ≐ refl`.
+
+**Warning.** Just like rewrite rules, this is an unsafe construction and should
+be used with the utmost caution.
+
+## 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

From ca671fe06b8f8f8b1618db550e626b6d2e51652f Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 15 Apr 2024 19:32:49 +0200
Subject: [PATCH 05/29] projections for `htpy-eq-cocone`

---
 .../cocones-under-spans.lagda.md              | 24 +++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
index 7812d050c5..0fbfc13ccf 100644
--- a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
@@ -127,6 +127,30 @@ module _
     (c c' : cocone f g X) → c ＝ c' → htpy-cocone c c'
   htpy-eq-cocone c .c refl = reflexive-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 =
+      pr1 (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 =
+      pr1 (pr2 (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 =
+      pr2 (pr2 (htpy-eq-cocone c c' p))
+
   is-torsorial-htpy-cocone :
     (c : cocone f g X) → is-torsorial (htpy-cocone c)
   is-torsorial-htpy-cocone c =

From 81dfdfda823eb12b305c3351cc5657e6da868400 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 15 Apr 2024 19:40:28 +0200
Subject: [PATCH 06/29] Dependent cocones on constant type families

---
 .../dependent-cocones-under-spans.lagda.md       | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

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..b21b68ad78 100644
--- a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
@@ -9,6 +9,7 @@ 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.constant-type-families
 open import foundation.contractible-types
 open import foundation.dependent-identifications
 open import foundation.dependent-pair-types
@@ -226,3 +227,18 @@ module _
     is-retraction-eq-htpy-dependent-cocone d' =
       is-retraction-map-inv-is-equiv (is-equiv-htpy-eq-dependent-cocone d')
 ```
+
+### Dependent cocones on constant type families
+
+```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-cocone : cocone f g Y → dependent-cocone f g c (λ _ → Y)
+  pr1 (dependent-cocone-cocone (f' , g' , H)) = f'
+  pr1 (pr2 (dependent-cocone-cocone (f' , g' , H))) = g'
+  pr2 (pr2 (dependent-cocone-cocone (f' , g' , H))) s =
+    tr-constant-type-family (coherence-square-cocone f g c s) (f' (f s)) ∙ H s
+```

From aa13b237d13cc7a0f83b6c3ab46797ef804a76ed Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 15 Apr 2024 19:40:54 +0200
Subject: [PATCH 07/29] change pushout postulates

---
 .../pushouts.lagda.md                         | 246 +++++++++++-------
 1 file changed, 156 insertions(+), 90 deletions(-)

diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index 0d3e09fb2a..a56ab4ac55 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -1,8 +1,6 @@
 # Pushouts
 
 ```agda
-{-# OPTIONS --rewriting #-}
-
 module synthetic-homotopy-theory.pushouts where
 ```
 
@@ -23,12 +21,13 @@ open import foundation.retractions
 open import foundation.sections
 open import foundation.universe-levels
 
-open import reflection.rewriting
+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
 ```
 
@@ -81,6 +80,8 @@ Examples of pushouts include
 
 ## Postulates
 
+### The standard pushout type
+
 We will assume that for any span
 
 ```text
@@ -118,100 +119,83 @@ 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)
-
-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
 ```
 
-## Definitions
-
-### The cogap map
+### The dependent 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}
+  (f : S → A) (g : S → B) {P : pushout f g → UU l4}
+  (c : dependent-cocone f g (cocone-pushout f g) P)
   where
 
-  cogap : cocone f g X → pushout f g → X
-  cogap = map-inv-equiv (equiv-up-pushout f g X)
-
-  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-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)
-```
-
-### The small predicate of being a pushout cocone
-
-```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
-
-  is-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  is-pushout = is-equiv (cogap f g c)
-
-  is-prop-is-pushout : is-prop is-pushout
-  is-prop-is-pushout = is-property-is-equiv (cogap f g c)
-
-  is-pushout-Prop : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  pr1 is-pushout-Prop = is-pushout
-  pr2 is-pushout-Prop = is-prop-is-pushout
+  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)
 ```
 
-## Properties
+## Definitions
 
-### Pushout cocones satisfy the universal property of the pushout
+### The induction principle 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) {X : UU l4} (c : cocone f g X)
+  {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B)
   where
 
-  universal-property-pushout-is-pushout :
-    is-pushout f g c → {l : Level} → universal-property-pushout l f g c
-  universal-property-pushout-is-pushout po =
-    up-pushout-up-pushout-is-equiv f g
+  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)
-      ( cogap f g c)
-      ( htpy-cocone-map-universal-property-pushout f g
-        ( cocone-pushout f g)
-        ( up-pushout f g)
-        ( c))
-      ( po)
-      ( up-pushout f g)
-
-  is-pushout-universal-property-pushout :
-    ({l : Level} → universal-property-pushout l f g c) → is-pushout f g c
-  is-pushout-universal-property-pushout =
-    is-equiv-up-pushout-up-pushout f g
-      ( cocone-pushout f g)
-      ( c)
-      ( cogap f g c)
-      ( htpy-cocone-map-universal-property-pushout f g
-        ( cocone-pushout f g)
-        ( up-pushout f g)
-        ( c))
-      ( up-pushout f g)
+      ( compute-inl-dependent-cogap f g c ,
+        compute-inr-dependent-cogap f g c ,
+        compute-glue-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)
 ```
 
-### The pushout of a span has the dependent universal property
+### The dependent universal property of standard pushouts
 
 ```agda
 module _
@@ -222,11 +206,9 @@ module _
   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)
+    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 l4) →
@@ -237,6 +219,47 @@ module _
     dup-pushout P
 ```
 
+### The universal property of standard pushouts
+
+```agda
+-- TODO: Redefine. The current definition does not preserve the inverse map.
+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 =
+  universal-property-dependent-universal-property-pushout f g
+    ( cocone-pushout f g)
+    ( dup-pushout 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
+```
+
+### The cogap map
+
+<!-- TODO: redefine `cogap` in terms of `dependent-cogap`, and show it is inverse to `cocone-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}
+  where
+
+  cogap : cocone f g X → pushout f g → X
+  cogap = map-inv-equiv (equiv-up-pushout f g X)
+
+  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-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)
+```
+
 ### Computation with the cogap map
 
 ```agda
@@ -247,7 +270,7 @@ module _
   where
 
   compute-inl-cogap :
-    ( a : A) → cogap f g c (inl-pushout f g a) ＝ horizontal-map-cocone f g c a
+    cogap f g c ∘ inl-pushout f g ~ horizontal-map-cocone f g c
   compute-inl-cogap =
     horizontal-htpy-cocone-map-universal-property-pushout
       ( f)
@@ -257,7 +280,7 @@ module _
       ( c)
 
   compute-inr-cogap :
-    ( b : B) → cogap f g c (inr-pushout f g b) ＝ vertical-map-cocone f g c b
+    cogap f g c ∘ inr-pushout f g ~ vertical-map-cocone f g c
   compute-inr-cogap =
     vertical-htpy-cocone-map-universal-property-pushout
       ( f)
@@ -281,18 +304,61 @@ module _
       ( c)
 ```
 
-### Rewrite rules
+### The small predicate of being a pushout cocone
 
 ```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)
+  {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
 
-  rewrite-inl-cogap :
-    ( a : A) → cogap f g c (inl-pushout f g a) ＝ horizontal-map-cocone f g c a
+  is-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-pushout = is-equiv (cogap f g c)
 
+  is-prop-is-pushout : is-prop is-pushout
+  is-prop-is-pushout = is-property-is-equiv (cogap f g c)
+
+  is-pushout-Prop : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  pr1 is-pushout-Prop = is-pushout
+  pr2 is-pushout-Prop = is-prop-is-pushout
+```
+
+## Properties
+
+### Pushout cocones satisfy the universal 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
+
+  universal-property-pushout-is-pushout :
+    is-pushout f g c → {l : Level} → universal-property-pushout l f g c
+  universal-property-pushout-is-pushout po =
+    up-pushout-up-pushout-is-equiv f g
+      ( cocone-pushout f g)
+      ( c)
+      ( cogap f g c)
+      ( htpy-cocone-map-universal-property-pushout f g
+        ( cocone-pushout f g)
+        ( up-pushout f g)
+        ( c))
+      ( po)
+      ( up-pushout f g)
+
+  is-pushout-universal-property-pushout :
+    ({l : Level} → universal-property-pushout l f g c) → is-pushout f g c
+  is-pushout-universal-property-pushout =
+    is-equiv-up-pushout-up-pushout f g
+      ( cocone-pushout f g)
+      ( c)
+      ( cogap f g c)
+      ( htpy-cocone-map-universal-property-pushout f g
+        ( cocone-pushout f g)
+        ( up-pushout f g)
+        ( c))
+      ( up-pushout f g)
 ```
 
 ### Fibers of the cogap map

From 3e3b60b5ba60fb24712744d8cd4b4a3082a4184d Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 15 Apr 2024 19:42:02 +0200
Subject: [PATCH 08/29] add module `rewriting-pushouts`

---
 src/synthetic-homotopy-theory.lagda.md        |  1 +
 .../rewriting-pushouts.lagda.md               | 47 +++++++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index a21aae0963..6786aeb4d5 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -80,6 +80,7 @@ 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/rewriting-pushouts.lagda.md b/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md
new file mode 100644
index 0000000000..1274c2f8b7
--- /dev/null
+++ b/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md
@@ -0,0 +1,47 @@
+# Rewriting rules for pushouts
+
+```agda
+{-# OPTIONS --rewriting #-}
+
+module synthetic-homotopy-theory.rewriting-pushouts where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.fibers-of-maps
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.retractions
+open import foundation.sections
+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.dependent-universal-property-pushouts
+open import synthetic-homotopy-theory.flattening-lemma-pushouts
+open import synthetic-homotopy-theory.pushouts
+open import synthetic-homotopy-theory.universal-property-pushouts
+```
+
+</details>
+
+## Idea
+
+TODO
+
+## Rewrite rules
+
+```agda
+{-# REWRITE compute-inl-dependent-cogap #-}
+{-# REWRITE compute-inr-dependent-cogap #-}
+```

From 2eb7ed069cd35f33fbb326fcddb811a392b9f3ef Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 15 Apr 2024 22:27:31 +0200
Subject: [PATCH 09/29] computing with dependent cocones on constant type
 families

---
 .../dependent-cocones-under-spans.lagda.md    | 128 ++++++++++++++++++
 1 file changed, 128 insertions(+)

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 b21b68ad78..437e500fb2 100644
--- a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
@@ -13,17 +13,22 @@ open import foundation.constant-type-families
 open import foundation.contractible-types
 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-identifications
 open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
 
 open import synthetic-homotopy-theory.cocones-under-spans
 ```
@@ -241,4 +246,127 @@ module _
   pr1 (pr2 (dependent-cocone-cocone (f' , g' , H))) = g'
   pr2 (pr2 (dependent-cocone-cocone (f' , g' , H))) s =
     tr-constant-type-family (coherence-square-cocone f g c s) (f' (f s)) ∙ H s
+
+  map-inv-dependent-cocone-cocone :
+    dependent-cocone f g c (λ _ → Y) → cocone f g Y
+  pr1 (map-inv-dependent-cocone-cocone (f' , g' , H)) = f'
+  pr1 (pr2 (map-inv-dependent-cocone-cocone (f' , g' , H))) = g'
+  pr2 (pr2 (map-inv-dependent-cocone-cocone (f' , g' , H))) s =
+    ( inv
+      ( tr-constant-type-family (coherence-square-cocone f g c s) (f' (f s)))) ∙
+    ( H s)
+
+  is-section-map-inv-dependent-cocone-cocone :
+    is-section dependent-cocone-cocone map-inv-dependent-cocone-cocone
+  is-section-map-inv-dependent-cocone-cocone (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-map-inv-dependent-cocone-cocone :
+    is-retraction dependent-cocone-cocone map-inv-dependent-cocone-cocone
+  is-retraction-map-inv-dependent-cocone-cocone (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-cocone : is-equiv dependent-cocone-cocone
+  is-equiv-dependent-cocone-cocone =
+    is-equiv-is-invertible
+      ( map-inv-dependent-cocone-cocone)
+      ( is-section-map-inv-dependent-cocone-cocone)
+      ( is-retraction-map-inv-dependent-cocone-cocone)
+
+  compute-dependent-cocone-constant-type-family :
+    cocone f g Y ≃ dependent-cocone f g c (λ _ → Y)
+  compute-dependent-cocone-constant-type-family =
+    ( dependent-cocone-cocone , is-equiv-dependent-cocone-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-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-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 ~
+    map-inv-dependent-cocone-cocone 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)
+      ( ( map-inv-dependent-cocone-cocone 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-cocone f g c)
+      ( cocone-map f g c)
+      ( triangle-dependent-cocone-map-constant-type-family f g c)
+      ( is-equiv-dependent-cocone-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-cocone f g c)
+      ( cocone-map f g c)
+      ( triangle-dependent-cocone-map-constant-type-family f g c)
+      ( H)
+      ( is-equiv-dependent-cocone-cocone f g c)
 ```

From f59f39026f6f0d2f83fe4ea8fdca0b921758cf9a Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 15 Apr 2024 22:44:06 +0200
Subject: [PATCH 10/29] redefine `cogap` so it computes with rewrite rules

---
 .../pushouts.lagda.md                         | 69 ++++++++++++-------
 1 file changed, 45 insertions(+), 24 deletions(-)

diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index a56ab4ac55..ff4833f1d1 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -20,6 +20,7 @@ open import foundation.propositions
 open import foundation.retractions
 open import foundation.sections
 open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
 
 open import reflection.erasing-equality
 
@@ -217,32 +218,18 @@ module _
     dependent-cocone-map f g (cocone-pushout f g) P
   pr2 (equiv-dup-pushout P) =
     dup-pushout P
-```
-
-### The universal property of standard pushouts
-
-```agda
--- TODO: Redefine. The current definition does not preserve the inverse map.
-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 =
-  universal-property-dependent-universal-property-pushout f g
-    ( cocone-pushout f g)
-    ( dup-pushout 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
+  is-retraction-dependent-cogap :
+    {P : pushout f g → UU l4} →
+    is-retraction
+      ( dependent-cocone-map f g (cocone-pushout f g) P)
+      ( dependent-cogap f g)
+  is-retraction-dependent-cogap {P = P} =
+    is-retraction-map-inv-is-equiv (dup-pushout P)
 ```
 
 ### The cogap map
 
-<!-- TODO: redefine `cogap` in terms of `dependent-cogap`, and show it is inverse to `cocone-map` -->
-
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
@@ -250,14 +237,48 @@ module _
   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-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
+    ( ( map-inv-dependent-cocone-cocone f g (cocone-pushout f g)) ·l
+      ( is-section-dependent-cogap f g) ·r
+      ( dependent-cocone-cocone f g (cocone-pushout f g))) ∙h
+    ( is-retraction-map-inv-dependent-cocone-cocone 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)
+  is-retraction-cogap =
+    ( ( cogap) ·l
+      ( ( triangle-dependent-cocone-map-constant-type-family' f g
+          ( cocone-pushout f g)))) ∙h
+    ( ( dependent-cogap f g) ·l
+      ( is-section-map-inv-dependent-cocone-cocone 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

From 8662b15f233cbbc5c69f4d7834fce6a9a0871699 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 15 Apr 2024 23:42:33 +0200
Subject: [PATCH 11/29] Idea `rewriting-pushouts`

---
 .../pushouts.lagda.md                         | 53 ++++++-----
 .../rewriting-pushouts.lagda.md               | 88 +++++++++++++++----
 2 files changed, 95 insertions(+), 46 deletions(-)

diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index ff4833f1d1..e636cf6c30 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -238,7 +238,12 @@ module _
 
   cogap : cocone f g X → pushout f g → X
   cogap = dependent-cogap f g ∘ dependent-cocone-cocone f g (cocone-pushout f g)
+```
+
+We write out the section and retraction homotopy in full detail to ensure that
+the inverse of `cocone-map` computes to `cogap` judgmentally.
 
+```agda
   is-section-cogap : is-section (cocone-map f g (cocone-pushout f g)) cogap
   is-section-cogap =
     ( ( triangle-dependent-cocone-map-constant-type-family' f g
@@ -253,8 +258,8 @@ module _
     is-retraction (cocone-map f g (cocone-pushout f g)) cogap
   is-retraction-cogap =
     ( ( cogap) ·l
-      ( ( triangle-dependent-cocone-map-constant-type-family' f g
-          ( cocone-pushout f g)))) ∙h
+      ( triangle-dependent-cocone-map-constant-type-family' f g
+        ( cocone-pushout f g))) ∙h
     ( ( dependent-cogap f g) ·l
       ( is-section-map-inv-dependent-cocone-cocone f g (cocone-pushout f g)) ·r
       ( dependent-cocone-map f g (cocone-pushout f g) (λ _ → X))) ∙h
@@ -293,36 +298,28 @@ module _
   compute-inl-cogap :
     cogap f g c ∘ inl-pushout f g ~ horizontal-map-cocone f g c
   compute-inl-cogap =
-    horizontal-htpy-cocone-map-universal-property-pushout
-      ( f)
-      ( g)
-      ( cocone-pushout f g)
-      ( up-pushout f g)
-      ( c)
+    compute-inl-dependent-cogap f g
+      ( dependent-cocone-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 =
-    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)
+    compute-inr-dependent-cogap f g
+      ( dependent-cocone-cocone f g (cocone-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)
 ```
 
 ### The small predicate of being a pushout cocone
diff --git a/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md b/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md
index 1274c2f8b7..def3d52155 100644
--- a/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md
@@ -9,35 +9,61 @@ module synthetic-homotopy-theory.rewriting-pushouts where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.action-on-identifications-functions
-open import foundation.commuting-squares-of-maps
-open import foundation.dependent-pair-types
-open import foundation.equivalences
-open import foundation.fibers-of-maps
-open import foundation.function-types
-open import foundation.functoriality-dependent-pair-types
+open import reflection.rewriting
+open import foundation.universe-levels
 open import foundation.homotopies
 open import foundation.identity-types
-open import foundation.propositions
-open import foundation.retractions
-open import foundation.sections
-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.dependent-universal-property-pushouts
-open import synthetic-homotopy-theory.flattening-lemma-pushouts
 open import synthetic-homotopy-theory.pushouts
-open import synthetic-homotopy-theory.universal-property-pushouts
 ```
 
 </details>
 
 ## Idea
 
-TODO
+We endow 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 us 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, we enable strict computation rules for the dependent eliminator,
+giving us 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 such a way that the (pre-existing) witnesses of these equalities reduce to
+`refl`. This is achieved using Agda's
+[equality erasure](reflection.erasing-equality.md) functionality.
+
+**Note.** By default, we abstain from using rewrite rules in agda-unimath.
+However, we recognize their usefulness in, for example, 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 don't enable rewrite rules.
 
 ## Rewrite rules
 
@@ -45,3 +71,29 @@ TODO
 {-# REWRITE compute-inl-dependent-cogap #-}
 {-# REWRITE compute-inr-dependent-cogap #-}
 ```
+
+## Properties
+
+### Verifying the reduction behavior of the computation rules for the nondependent eliminator 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) {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}} {{#reference UF13}}

From 72dc2e30b3602b0a836645dc197a4d3480913a6b Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 15 Apr 2024 23:42:42 +0200
Subject: [PATCH 12/29] pre-commit

---
 src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md b/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md
index def3d52155..08762abbe0 100644
--- a/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md
@@ -9,10 +9,11 @@ module synthetic-homotopy-theory.rewriting-pushouts where
 <details><summary>Imports</summary>
 
 ```agda
-open import reflection.rewriting
-open import foundation.universe-levels
 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.pushouts

From 88686b0f90480f352b8ab2d87d2aa48c3379724c Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 16 Apr 2024 12:17:58 +0200
Subject: [PATCH 13/29] Naturality of transport in constant type families

---
 .../constant-type-families.lagda.md           | 43 ++++++++++++++++++-
 1 file changed, 42 insertions(+), 1 deletion(-)

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
+```

From f2e276e277159bd7a146566a077455dc3dddcd5c Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 16 Apr 2024 12:18:51 +0200
Subject: [PATCH 14/29] nitpick `dependent-identifications`

---
 src/foundation/dependent-identifications.lagda.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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') =

From 850a9f8975815200018f0014fb968adfcaa79175 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 16 Apr 2024 12:19:16 +0200
Subject: [PATCH 15/29] nitpick `transport-along-identifications`

---
 src/foundation/transport-along-identifications.lagda.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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
 ```

From b0044dbf4f72ff11c57eca5da8b8785b12e1d9ac Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 16 Apr 2024 12:20:00 +0200
Subject: [PATCH 16/29] Computing with the characterization of identifications
 of dependent cocones on constant type families

---
 .../dependent-cocones-under-spans.lagda.md    | 139 +++++++++++++-----
 1 file changed, 105 insertions(+), 34 deletions(-)

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 437e500fb2..a38d7615d2 100644
--- a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
@@ -11,6 +11,7 @@ open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 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
@@ -128,12 +129,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 =
@@ -241,24 +240,27 @@ module _
   (f : S → A) (g : S → B) (c : cocone f g X) {Y : UU l5}
   where
 
-  dependent-cocone-cocone : cocone f g Y → dependent-cocone f g c (λ _ → Y)
-  pr1 (dependent-cocone-cocone (f' , g' , H)) = f'
-  pr1 (pr2 (dependent-cocone-cocone (f' , g' , H))) = g'
-  pr2 (pr2 (dependent-cocone-cocone (f' , g' , H))) s =
+  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
 
-  map-inv-dependent-cocone-cocone :
+  cocone-dependent-cocone-constant-type-family :
     dependent-cocone f g c (λ _ → Y) → cocone f g Y
-  pr1 (map-inv-dependent-cocone-cocone (f' , g' , H)) = f'
-  pr1 (pr2 (map-inv-dependent-cocone-cocone (f' , g' , H))) = g'
-  pr2 (pr2 (map-inv-dependent-cocone-cocone (f' , g' , H))) s =
+  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-map-inv-dependent-cocone-cocone :
-    is-section dependent-cocone-cocone map-inv-dependent-cocone-cocone
-  is-section-map-inv-dependent-cocone-cocone (f' , g' , H) =
+  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
@@ -269,9 +271,11 @@ module _
                 ( f' (f s)))
               ( H s))))
 
-  is-retraction-map-inv-dependent-cocone-cocone :
-    is-retraction dependent-cocone-cocone map-inv-dependent-cocone-cocone
-  is-retraction-map-inv-dependent-cocone-cocone (f' , g' , H) =
+  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
@@ -282,17 +286,19 @@ module _
                 ( f' (f s)))
               ( H s))))
 
-  is-equiv-dependent-cocone-cocone : is-equiv dependent-cocone-cocone
-  is-equiv-dependent-cocone-cocone =
+  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
-      ( map-inv-dependent-cocone-cocone)
-      ( is-section-map-inv-dependent-cocone-cocone)
-      ( is-retraction-map-inv-dependent-cocone-cocone)
+      ( 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-cocone , is-equiv-dependent-cocone-cocone)
+    ( dependent-cocone-constant-type-family-cocone ,
+      is-equiv-dependent-cocone-constant-type-family-cocone)
 ```
 
 ### Computing the dependent cocone map on a constant type family
@@ -305,12 +311,12 @@ module _
 
   triangle-dependent-cocone-map-constant-type-family :
     dependent-cocone-map f g c (λ _ → Y) ~
-    dependent-cocone-cocone f g c ∘ cocone-map f g c
+    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-cocone f g c ∘ cocone-map f g c) h)
+      ( dependent-cocone-constant-type-family-cocone f g c (cocone-map f g c h))
       ( ( refl-htpy) ,
         ( refl-htpy) ,
         ( λ s →
@@ -319,11 +325,12 @@ module _
 
   triangle-dependent-cocone-map-constant-type-family' :
     cocone-map f g c ~
-    map-inv-dependent-cocone-cocone f g c ∘ dependent-cocone-map f g c (λ _ → Y)
+    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)
-      ( ( map-inv-dependent-cocone-cocone f g c
+      ( ( cocone-dependent-cocone-constant-type-family f g c
           ( dependent-cocone-map f g c (λ _ → Y) h)))
       ( ( refl-htpy) ,
         ( refl-htpy) ,
@@ -353,10 +360,10 @@ module _
   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-cocone f g c)
+      ( 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-cocone 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) →
@@ -364,9 +371,73 @@ module _
   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-cocone f g c)
+      ( 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-cocone f g c)
+      ( is-equiv-dependent-cocone-constant-type-family-cocone f g c)
+```
+
+### Computing with the characterization of identifications of dependent cocones on constant type families
+
+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-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-coherence-htpy-dependent-cocone-constant-type-family
+    d d' K L H x =
+    ( assoc
+      ( 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)
+      ( L (g x))) ∙
+    ( ap
+      ( inv
+        ( tr-constant-type-family
+          ( coherence-square-cocone f g c x)
+          ( horizontal-map-dependent-cocone f g c (λ _ → Y) d (f x))) ∙_)
+      ( H x)) ∙
+    ( inv
+      ( assoc
+        ( 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))) ∙
+    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))
 ```

From f88cb2a76e43d45effbbae16b0fef78c3dc76f1c Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 16 Apr 2024 18:45:16 +0200
Subject: [PATCH 17/29] Dependent homotopies of dependent cocones

---
 .../dependent-cocones-under-spans.lagda.md    | 307 +++++++++++++++++-
 1 file changed, 305 insertions(+), 2 deletions(-)

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 a38d7615d2..49b57eac6d 100644
--- a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
@@ -9,6 +9,7 @@ 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-maps
 open import foundation.constant-type-families
 open import foundation.contractible-types
 open import foundation.dependent-homotopies
@@ -27,10 +28,13 @@ 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
 ```
 
@@ -101,6 +105,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
@@ -232,6 +305,174 @@ module _
       is-retraction-map-inv-is-equiv (is-equiv-htpy-eq-dependent-cocone d')
 ```
 
+### Dependent homotopies of dependent 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
+      ( pr2 (pr2 c) s)
+      ( pr2 (pr2 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 _))
+```
+
+We now move to characterize cocones equipped with dependent cocones, from this,
+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
 
 ```agda
@@ -391,7 +632,7 @@ module _
   (Y : UU l5)
   where
 
-  coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family :
+  coherence-htpy-dependent-cocone-constant-type-family-coherence-htpy-cocone :
     ( d d' : dependent-cocone f g c (λ _ → Y)) →
     ( K :
       horizontal-map-dependent-cocone f g c (λ _ → Y) d ~
@@ -405,7 +646,7 @@ module _
       ( cocone-dependent-cocone-constant-type-family f g c d')
       ( K)
       ( L)
-  coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family
+  coherence-htpy-dependent-cocone-constant-type-family-coherence-htpy-cocone
     d d' K L H x =
     ( assoc
       ( inv
@@ -441,3 +682,65 @@ module _
           ( 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)
+    (c c' : cocone f g Y) →
+    ( K : horizontal-map-cocone f g c ~ horizontal-map-cocone f g c')
+    ( L : vertical-map-cocone f g c ~ vertical-map-cocone f g c') →
+    coherence-htpy-dependent-cocone f g c'' (λ _ → Y)
+      ( dependent-cocone-constant-type-family-cocone f g c'' c)
+      ( dependent-cocone-constant-type-family-cocone f g c'' c')
+      ( K)
+      ( L) →
+    statement-coherence-htpy-cocone f g
+      ( c)
+      ( c')
+      ( K)
+      ( L)
+  coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family
+    c'' c c' K L H x =
+    is-injective-concat
+      ( tr-constant-type-family
+        ( coherence-square-cocone f g c'' x)
+        ( horizontal-map-cocone f g c (f x)))
+      ( ( inv
+          ( assoc
+            ( tr-constant-type-family
+              ( coherence-square-cocone f g c'' x)
+              ( horizontal-map-cocone f g c (f x)))
+            ( coherence-square-cocone f g c x)
+            ( L (g x)))) ∙
+        ( H x) ∙
+        ( inv
+          ( assoc
+            ( ap
+              ( tr (λ _ → Y) (coherence-square-cocone f g c'' x))
+              ( K (f x)))
+            ( tr-constant-type-family
+              ( coherence-square-cocone f g c'' x)
+              ( horizontal-map-cocone f g c' (f x)))
+            ( coherence-square-cocone f g c' x))) ∙
+        ( ap
+          ( _∙ coherence-square-cocone f g c' x)
+          ( inv
+            ( naturality-tr-constant-type-family
+              ( coherence-square-cocone f g c'' x)
+              ( K (f x))))) ∙
+        ( assoc
+          ( tr-constant-type-family
+            ( coherence-square-cocone f g c'' x)
+            ( horizontal-map-cocone f g c (f x)))
+          ( K (f x))
+          ( coherence-square-cocone f g c' x)))
+```

From 86b1582ffb4ca5399abaf6888fda4464745bcd21 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 16 Apr 2024 18:45:41 +0200
Subject: [PATCH 18/29] `reflexive-htpy-cocone` -> `refl-htpy-cocone`

---
 .../cocones-under-spans.lagda.md                       | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
index 0fe0acd579..e3adecbb9b 100644
--- a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
@@ -117,15 +117,15 @@ 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)

From ba8ae0b4703872f36af939b0ea360897f06467ad Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 16 Apr 2024 18:45:49 +0200
Subject: [PATCH 19/29] `is-retraction-ind-induction-principle-pushout`

---
 ...ndent-universal-property-pushouts.lagda.md | 80 ++++++++++---------
 1 file changed, 44 insertions(+), 36 deletions(-)

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..63274e881f 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,33 @@ 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)
+        ( pr2 (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)
+      ( pr2 (ind-c P))
+      ( is-retraction-ind-induction-principle-pushout ind-c P)
 ```
 
 #### The dependent universal property of pushouts implies the induction principle of pushouts

From fd189bf921cfebc36e73dc585ee04e76d3e10770 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 16 Apr 2024 18:46:02 +0200
Subject: [PATCH 20/29] `compute-glue-cogap` by hand

---
 .../pushouts.lagda.md                         | 150 +++++++++++++-----
 1 file changed, 110 insertions(+), 40 deletions(-)

diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index e636cf6c30..42b61bae9b 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -1,14 +1,18 @@
 # Pushouts
 
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 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,6 +23,8 @@ 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
 
@@ -157,12 +163,23 @@ module _
   postulate
     compute-glue-dependent-cogap :
       coherence-htpy-dependent-cocone f g
-        (cocone-pushout 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
@@ -186,46 +203,45 @@ module _
       ( P)
       ( dependent-cocone-map f g (cocone-pushout f g) P (dependent-cogap f g c))
       ( c)
-      ( compute-inl-dependent-cogap f g c ,
-        compute-inr-dependent-cogap f g c ,
-        compute-glue-dependent-cogap f g 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 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  {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 l4 f g (cocone-pushout f g)
+    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 l4) →
+    (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
-
-  is-retraction-dependent-cogap :
-    {P : pushout f g → UU l4} →
-    is-retraction
-      ( dependent-cocone-map f g (cocone-pushout f g) P)
-      ( dependent-cogap f g)
-  is-retraction-dependent-cogap {P = P} =
-    is-retraction-map-inv-is-equiv (dup-pushout P)
+  equiv-dup-pushout P =
+    ( dependent-cocone-map f g (cocone-pushout f g) P , dup-pushout P)
 ```
 
 ### The cogap map
@@ -237,7 +253,9 @@ module _
   where
 
   cogap : cocone f g X → pushout f g → X
-  cogap = dependent-cogap f g ∘ dependent-cocone-cocone f g (cocone-pushout f g)
+  cogap =
+    dependent-cogap f g ∘
+    dependent-cocone-constant-type-family-cocone f g (cocone-pushout f g)
 ```
 
 We write out the section and retraction homotopy in full detail to ensure that
@@ -249,10 +267,13 @@ the inverse of `cocone-map` computes to `cogap` judgmentally.
     ( ( triangle-dependent-cocone-map-constant-type-family' f g
         ( cocone-pushout f g)) ·r
       ( cogap)) ∙h
-    ( ( map-inv-dependent-cocone-cocone f g (cocone-pushout f g)) ·l
+    ( ( cocone-dependent-cocone-constant-type-family f g
+      ( cocone-pushout f g)) ·l
       ( is-section-dependent-cogap f g) ·r
-      ( dependent-cocone-cocone f g (cocone-pushout f g))) ∙h
-    ( is-retraction-map-inv-dependent-cocone-cocone f g (cocone-pushout f g))
+      ( 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
@@ -261,7 +282,8 @@ the inverse of `cocone-map` computes to `cogap` judgmentally.
       ( triangle-dependent-cocone-map-constant-type-family' f g
         ( cocone-pushout f g))) ∙h
     ( ( dependent-cogap f g) ·l
-      ( is-section-map-inv-dependent-cocone-cocone f g (cocone-pushout f g)) ·r
+      ( 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)
 ```
@@ -299,27 +321,75 @@ module _
     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-cocone f g (cocone-pushout f g) c)
+      ( 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-cocone f g (cocone-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)
+      ( 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 some construction -->
+
+```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

From 7160b93ec4b8b020174024887d820c1ab48e66e6 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 16 Apr 2024 18:47:23 +0200
Subject: [PATCH 21/29] elaborate

---
 src/synthetic-homotopy-theory/pushouts.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index 42b61bae9b..30b66451e1 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -330,7 +330,7 @@ module _
       ( 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 some construction -->
+<!-- TODO: find the right infrastructure to make the proof below just an application of some 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 -->
 
 ```agda
   abstract

From c736c041e8b7230bf04b14c061492149dd6db33b Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 16 Apr 2024 18:58:14 +0200
Subject: [PATCH 22/29] fixes

---
 src/reflection.lagda.md                                     | 4 ++++
 src/synthetic-homotopy-theory.lagda.md                      | 4 ++++
 src/synthetic-homotopy-theory/pushouts.lagda.md             | 2 --
 .../recursion-principle-pushouts.lagda.md                   | 6 ------
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/reflection.lagda.md b/src/reflection.lagda.md
index 1c00828e43..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
diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 70241e09b8..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
diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index 30b66451e1..6750b14e5a 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -1,8 +1,6 @@
 # Pushouts
 
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
-
 module synthetic-homotopy-theory.pushouts where
 ```
 
diff --git a/src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md b/src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md
index bb2d041fdf..d07198e605 100644
--- a/src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md
@@ -30,12 +30,6 @@ a type `X`, the cocone map
 
 has a [section](foundation.sections.md).
 
-The fact that the recursion principle of pushouts is
-[logically equivalent](foundation.logical-equivalences.md) to the
-[universal property](synthetic-homotopy-theory.universal-property-pushouts.md)
-of pushouts is shown in
-[`universal-property-pushouts`](synthetic-homotopy-theory.universal-property-pushouts.md).
-
 ## Definition
 
 ### The recursion principle of pushouts

From 74505998c338d76f34441532f7cd0d117b05d320 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 16 Apr 2024 19:49:30 +0200
Subject: [PATCH 23/29] refactoring definitions joins of types

---
 .../joins-of-types.lagda.md                   | 123 +++++++++++++-----
 1 file changed, 87 insertions(+), 36 deletions(-)

diff --git a/src/synthetic-homotopy-theory/joins-of-types.lagda.md b/src/synthetic-homotopy-theory/joins-of-types.lagda.md
index 36a860e028..7558e40ca5 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
-[pushout](synthetic-homotopy-theory.pushouts.md) of the
-[span](foundation.spans.md) `A ← A × B → B`.
+The {{#concept "join" Disambiguation="of types" Agda=join 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 = pr1 cocone-join
+
+  inr-join : B → A * B
+  inr-join = pr1 (pr2 cocone-join)
+
+  glue-join : (t : A × B) → inl-join (pr1 t) ＝ inr-join (pr2 t)
+  glue-join = pr2 (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 pr1 pr2 (cocone-join {A = A} {B})
   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)
 ```

From 6aaae1661a7b6ba0c6d8717a2950e5df07a7bf36 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 17 Apr 2024 11:29:01 +0200
Subject: [PATCH 24/29] idea `rewriting`

---
 src/reflection/erasing-equality.lagda.md | 10 +++-------
 src/reflection/rewriting.lagda.md        | 22 ++++++++++++++++++++++
 2 files changed, 25 insertions(+), 7 deletions(-)

diff --git a/src/reflection/erasing-equality.lagda.md b/src/reflection/erasing-equality.lagda.md
index 85d1577a4c..f852991517 100644
--- a/src/reflection/erasing-equality.lagda.md
+++ b/src/reflection/erasing-equality.lagda.md
@@ -26,17 +26,13 @@ reduction behaviour:
 
 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 of the
+`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
-in the expected way. Concretely, if the identification `β` defines a rewrite
-rule, and `β` is defined via `primEraseEqaulity`, then we have the strict
-equality `β ≐ refl`.
-
-**Warning.** Just like rewrite rules, this is an unsafe construction and should
-be used with the utmost caution.
+to `refl`. Concretely, if the identification `β` defines a rewrite rule, and `β`
+is defined via `primEraseEqaulity`, then we have the strict equality `β ≐ refl`.
 
 ## Primitives
 
diff --git a/src/reflection/rewriting.lagda.md b/src/reflection/rewriting.lagda.md
index 226c018236..1c8c484a15 100644
--- a/src/reflection/rewriting.lagda.md
+++ b/src/reflection/rewriting.lagda.md
@@ -16,10 +16,32 @@ open import foundation-core.identity-types
 
 ## Idea
 
+Agda's rewriting functionality allows us to add new strict equalities to our
+type theory. Given an equality `β : 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 [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

From ba8bed8de4c58e59e20d30a52d4d37c73e81112f Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 17 Apr 2024 11:31:02 +0200
Subject: [PATCH 25/29] standard* identity relation

---
 src/reflection/rewriting.lagda.md | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/reflection/rewriting.lagda.md b/src/reflection/rewriting.lagda.md
index 1c8c484a15..c30d08aa4c 100644
--- a/src/reflection/rewriting.lagda.md
+++ b/src/reflection/rewriting.lagda.md
@@ -31,8 +31,9 @@ abundant caution when defining such rules.
 
 ## Definitions
 
-We declare to Agda that the [identity relation](foundation.identity-types.md)
-may be used to define rewrite rules.
+We declare to Agda that the
+[standard identity relation](foundation.identity-types.md) may be used to define
+rewrite rules.
 
 ```agda
 {-# BUILTIN REWRITE _＝_ #-}

From b6e2b5c74521b56ab83b96964c56c66f6481486c Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 17 Apr 2024 12:10:12 +0200
Subject: [PATCH 26/29] headers dependent cocones

---
 .../dependent-cocones-under-spans.lagda.md       | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

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 49b57eac6d..bef1dcf123 100644
--- a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
@@ -191,7 +191,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 _
@@ -305,7 +305,7 @@ module _
       is-retraction-map-inv-is-equiv (is-equiv-htpy-eq-dependent-cocone d')
 ```
 
-### Dependent homotopies of dependent cocones
+### Dependent homotopies of dependent cocones over homotopies of cocones
 
 ```agda
 module _
@@ -391,9 +391,11 @@ module _
           ( is-torsorial-htpy _))
 ```
 
-We now move to characterize cocones equipped with dependent cocones, from this,
-it follows that dependent homotopies of dependent cocones characterize dependent
-identifications of them.
+#### Characterizing equality of cocones equipped with dependent cocones
+
+We now move to characterize equality of cocones equipped with dependent cocones,
+from this, it follows that dependent homotopies of dependent cocones
+characterize dependent identifications of them.
 
 ```agda
 module _
@@ -473,7 +475,7 @@ module _
       is-equiv-htpy-eq-cocone-with-dependent-cocone c c')
 ```
 
-### Dependent cocones on constant type families
+### Dependent cocones on constant type families are equivalent to nondependent cocones
 
 ```agda
 module _
@@ -619,7 +621,7 @@ module _
       ( is-equiv-dependent-cocone-constant-type-family-cocone f g c)
 ```
 
-### Computing with the characterization of identifications of dependent cocones on constant type families
+### 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.

From 6fa81af094a15ca9b44bb194b9032094895c0f65 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 17 Apr 2024 12:16:25 +0200
Subject: [PATCH 27/29] explain computation rules for pushouts

---
 src/synthetic-homotopy-theory/pushouts.lagda.md | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index 6750b14e5a..8e2977c33a 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -308,6 +308,11 @@ 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}
@@ -328,7 +333,7 @@ module _
       ( 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 some 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 -->
+<!-- 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 -->
 
 ```agda
   abstract

From f99e55329ee28a8396e1827428fbe744b794f126 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 19 Apr 2024 13:51:47 +0200
Subject: [PATCH 28/29] review comments

---
 src/reflection/erasing-equality.lagda.md      |  2 +-
 src/reflection/rewriting.lagda.md             |  4 +-
 .../cocones-under-spans.lagda.md              |  6 +--
 .../dependent-cocones-under-spans.lagda.md    | 22 ++++----
 ...ndent-universal-property-pushouts.lagda.md |  5 +-
 .../induction-principle-pushouts.lagda.md     | 23 ++++----
 .../joins-of-types.lagda.md                   | 16 +++---
 .../pushouts.lagda.md                         | 23 +++++---
 .../recursion-principle-pushouts.lagda.md     | 20 +++----
 .../rewriting-pushouts.lagda.md               | 52 +++++++++++++------
 10 files changed, 103 insertions(+), 70 deletions(-)

diff --git a/src/reflection/erasing-equality.lagda.md b/src/reflection/erasing-equality.lagda.md
index f852991517..3f3a0bec8a 100644
--- a/src/reflection/erasing-equality.lagda.md
+++ b/src/reflection/erasing-equality.lagda.md
@@ -17,7 +17,7 @@ open import foundation-core.identity-types
 ## Idea
 
 Agda's builtin primitive `primEraseEquality` is a special construct on
-[identifications](foundation-core.identity-types.md), that, for every
+[identifications](foundation-core.identity-types.md) that for every
 identification `x ＝ y` gives an identification `x ＝ y` with the following
 reduction behaviour:
 
diff --git a/src/reflection/rewriting.lagda.md b/src/reflection/rewriting.lagda.md
index c30d08aa4c..159ba1e1ed 100644
--- a/src/reflection/rewriting.lagda.md
+++ b/src/reflection/rewriting.lagda.md
@@ -17,8 +17,8 @@ open import foundation-core.identity-types
 ## Idea
 
 Agda's rewriting functionality allows us to add new strict equalities to our
-type theory. Given an equality `β : x ＝ y`, then adding a rewrite rule for `β`
-with
+type theory. Given an [identification](foundation-core.identity-types.md)
+`β : x ＝ y`, then adding a rewrite rule for `β` with
 
 ```text
 {-# REWRITE β #-}
diff --git a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
index e3adecbb9b..daaa5bd191 100644
--- a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
@@ -136,20 +136,20 @@ module _
       horizontal-map-cocone f g c ~
       horizontal-map-cocone f g c'
     horizontal-htpy-eq-cocone =
-      pr1 (htpy-eq-cocone c c' p)
+      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 =
-      pr1 (pr2 (htpy-eq-cocone c c' p))
+      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 =
-      pr2 (pr2 (htpy-eq-cocone c c' p))
+      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 bef1dcf123..b68afed9ce 100644
--- a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
@@ -365,8 +365,8 @@ module _
   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
-      ( pr2 (pr2 c) s)
-      ( pr2 (pr2 d) s)
+      ( 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)
@@ -394,7 +394,7 @@ module _
 #### Characterizing equality of cocones equipped with dependent cocones
 
 We now move to characterize equality of cocones equipped with dependent cocones,
-from this, it follows that dependent homotopies of dependent cocones
+from which it follows that dependent homotopies of dependent cocones
 characterize dependent identifications of them.
 
 ```agda
@@ -501,8 +501,8 @@ module _
 
   is-section-cocone-dependent-cocone-constant-type-family :
     is-section
-      dependent-cocone-constant-type-family-cocone
-      cocone-dependent-cocone-constant-type-family
+      ( 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
@@ -516,8 +516,8 @@ module _
 
   is-retraction-cocone-dependent-cocone-constant-type-family :
     is-retraction
-      dependent-cocone-constant-type-family-cocone
-      cocone-dependent-cocone-constant-type-family
+      ( 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
@@ -634,7 +634,7 @@ module _
   (Y : UU l5)
   where
 
-  coherence-htpy-dependent-cocone-constant-type-family-coherence-htpy-cocone :
+  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 ~
@@ -648,7 +648,7 @@ module _
       ( cocone-dependent-cocone-constant-type-family f g c d')
       ( K)
       ( L)
-  coherence-htpy-dependent-cocone-constant-type-family-coherence-htpy-cocone
+  coherence-htpy-cocone-dependent-cocone-coherence-htpy-dependent-cocone-constant-type-family
     d d' K L H x =
     ( assoc
       ( inv
@@ -671,11 +671,11 @@ module _
             ( 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))) ∙
-    ap
+    ( 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))) ∙
+        ( K (f x)))) ∙
     ( assoc
       ( K (f x))
       ( inv
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 63274e881f..eb89f7ca3b 100644
--- a/src/synthetic-homotopy-theory/dependent-universal-property-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-universal-property-pushouts.lagda.md
@@ -144,7 +144,8 @@ module _
           ( P)
           ( dependent-cocone-map f g c P h))
         ( h)
-        ( pr2 (ind-c P) (dependent-cocone-map f g c P 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) →
@@ -152,7 +153,7 @@ module _
   dependent-universal-property-pushout-induction-principle-pushout ind-c P =
     is-equiv-is-invertible
       ( ind-induction-principle-pushout f g c ind-c P)
-      ( pr2 (ind-c P))
+      ( eq-compute-ind-induction-principle-pushout f g c ind-c P)
       ( is-retraction-ind-induction-principle-pushout ind-c P)
 ```
 
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 7558e40ca5..0ef22c971d 100644
--- a/src/synthetic-homotopy-theory/joins-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/joins-of-types.lagda.md
@@ -37,9 +37,9 @@ open import synthetic-homotopy-theory.universal-property-pushouts
 
 ## Idea
 
-The {{#concept "join" Disambiguation="of types" Agda=join Agda=_*_}} of `A` and
-`B` is the [pushout](synthetic-homotopy-theory.pushouts.md) of the
-[span](foundation.spans.md) `A ← A × B → B`,
+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`.
 
 ## Definitions
 
@@ -60,13 +60,13 @@ module _
   cocone-join = cocone-pushout pr1 pr2
 
   inl-join : A → A * B
-  inl-join = pr1 cocone-join
+  inl-join = horizontal-map-cocone pr1 pr2 cocone-join
 
   inr-join : B → A * B
-  inr-join = pr1 (pr2 cocone-join)
+  inr-join = vertical-map-cocone pr1 pr2 cocone-join
 
   glue-join : (t : A × B) → inl-join (pr1 t) ＝ inr-join (pr2 t)
-  glue-join = pr2 (pr2 cocone-join)
+  glue-join = coherence-square-cocone pr1 pr2 cocone-join
 ```
 
 ### The universal property of the join
@@ -77,7 +77,7 @@ module _
   where
 
   up-join :
-    {l : Level} → universal-property-pushout l pr1 pr2 (cocone-join {A = A} {B})
+    {l : Level} → universal-property-pushout l {A = A} {B} pr1 pr2 cocone-join
   up-join = up-pushout pr1 pr2
 
   equiv-up-join :
@@ -102,7 +102,7 @@ module _
   compute-inl-dependent-cogap-join = compute-inl-dependent-cogap pr1 pr2 c
 
   compute-inr-dependent-cogap-join :
-    ( dependent-cogap-join ∘ inr-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
 
diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index 8e2977c33a..2bf9a843b7 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -128,6 +128,14 @@ pr2 (pr2 (cocone-pushout f g)) = glue-pushout f g
 
 ### The dependent cogap map
 
+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}
@@ -238,12 +246,16 @@ module _
   equiv-dup-pushout :
     (P : pushout f g → UU l) →
     ((x : pushout f g) → P x) ≃ dependent-cocone f g (cocone-pushout f g) P
-  equiv-dup-pushout P =
-    ( dependent-cocone-map f g (cocone-pushout f g) P , dup-pushout 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}
@@ -254,19 +266,14 @@ module _
   cogap =
     dependent-cogap f g ∘
     dependent-cocone-constant-type-family-cocone f g (cocone-pushout f g)
-```
 
-We write out the section and retraction homotopy in full detail to ensure that
-the inverse of `cocone-map` computes to `cogap` judgmentally.
-
-```agda
   is-section-cogap : is-section (cocone-map f g (cocone-pushout f g)) cogap
   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
+        ( 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
diff --git a/src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md b/src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md
index d07198e605..af0fa511a5 100644
--- a/src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/recursion-principle-pushouts.lagda.md
@@ -21,8 +21,8 @@ open import synthetic-homotopy-theory.dependent-cocones-under-spans
 ## Idea
 
 The {{#concept "recursion principle of pushouts"}} asserts that for every type
-`Y` and [cocone](synthetic-homotopy-theory.dependent-cocones-under-spans.md) on
-a type `X`, the cocone map
+`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
@@ -64,27 +64,27 @@ module _
       ( h)
       ( pr2 rec-c h)
 
-  left-compute-rec-recursion-principle-pushout :
+  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
-  left-compute-rec-recursion-principle-pushout h =
+  compute-horizontal-map-rec-recursion-principle-pushout h =
     pr1 (compute-rec-recursion-principle-pushout h)
 
-  right-compute-rec-recursion-principle-pushout :
+  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
-  right-compute-rec-recursion-principle-pushout h =
+  compute-vertical-map-rec-recursion-principle-pushout h =
     pr1 (pr2 (compute-rec-recursion-principle-pushout h))
 
-  path-compute-rec-recursion-principle-pushout :
+  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)
-      ( left-compute-rec-recursion-principle-pushout h)
-      ( right-compute-rec-recursion-principle-pushout h)
-  path-compute-rec-recursion-principle-pushout 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
index 08762abbe0..5b471fe9ff 100644
--- a/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/rewriting-pushouts.lagda.md
@@ -16,6 +16,7 @@ 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
 ```
 
@@ -23,10 +24,10 @@ open import synthetic-homotopy-theory.pushouts
 
 ## Idea
 
-We endow the eliminator of the
+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 us the strict
+[rewriting](reflection.rewriting.md) functionality. This gives the strict
 equalities
 
 ```text
@@ -39,8 +40,8 @@ and
   cogap (inr-pushout f g b) ≐ vertical-map-cocone f g c b.
 ```
 
-More generally, we enable strict computation rules for the dependent eliminator,
-giving us the strict equalities
+More generally, strict computation rules for the dependent eliminator are
+enabled, giving the strict equalities
 
 ```text
   dependent-cogap (inl-pushout f g a) ≐
@@ -51,20 +52,27 @@ and
 
 ```text
   dependent-cogap (inr-pushout f g b) ≐
-  vertical-map-dependent-cocone f g (cocone-pushout f g) P c b,
+  vertical-map-dependent-cocone f g (cocone-pushout f g) P c b.
 ```
 
-in such a way that the (pre-existing) witnesses of these equalities reduce to
-`refl`. This is achieved using Agda's
+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.
 
-**Note.** By default, we abstain from using rewrite rules in agda-unimath.
-However, we recognize their usefulness in, for example, 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 don't enable rewrite rules.
+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
 
@@ -75,9 +83,21 @@ be applied in other formalizations that don't enable rewrite rules.
 
 ## Properties
 
-### Verifying the reduction behavior of the computation rules for the nondependent eliminator of standard pushouts
+### 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)
@@ -97,4 +117,4 @@ module _
 
 ## References
 
-{{#bibliography}} {{#reference UF13}}
+{{#bibliography}}

From 001ffc67f9aefca9d806a235bdd5ae1b7456e1e2 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 19 Apr 2024 14:19:28 +0200
Subject: [PATCH 29/29] `assoc ap inv assoc` business

---
 .../dependent-cocones-under-spans.lagda.md    | 81 ++++++++-----------
 .../pushouts.lagda.md                         |  2 +-
 2 files changed, 33 insertions(+), 50 deletions(-)

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 b68afed9ce..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,6 +9,7 @@ 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
@@ -650,27 +651,16 @@ module _
       ( L)
   coherence-htpy-cocone-dependent-cocone-coherence-htpy-dependent-cocone-constant-type-family
     d d' K L H x =
-    ( assoc
+    ( 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)
-      ( L (g x))) ∙
-    ( ap
-      ( 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)
+      ( L (g x))
       ( H x)) ∙
-    ( inv
-      ( assoc
-        ( 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))) ∙
     ( ap
       ( _∙ coherence-square-dependent-cocone f g c (λ _ → Y) d' x)
       ( naturality-inv-tr-constant-type-family
@@ -696,53 +686,46 @@ module _
   where
 
   coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family :
-    (c'' : cocone f g X)
-    (c c' : cocone f g Y) →
-    ( K : horizontal-map-cocone f g c ~ horizontal-map-cocone f g c')
-    ( L : vertical-map-cocone f g c ~ vertical-map-cocone f g c') →
-    coherence-htpy-dependent-cocone f g c'' (λ _ → Y)
-      ( dependent-cocone-constant-type-family-cocone f g c'' c)
-      ( dependent-cocone-constant-type-family-cocone f g c'' c')
+    (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
-      ( c)
-      ( c')
+      ( d)
+      ( d')
       ( K)
       ( L)
   coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family
-    c'' c c' K L H x =
+    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 c (f x)))
+        ( 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 c (f x)))
-            ( coherence-square-cocone f g c x)
+              ( 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) ∙
-        ( inv
-          ( assoc
-            ( ap
-              ( tr (λ _ → Y) (coherence-square-cocone f g c'' x))
-              ( K (f x)))
-            ( tr-constant-type-family
-              ( coherence-square-cocone f g c'' x)
-              ( horizontal-map-cocone f g c' (f x)))
-            ( coherence-square-cocone f g c' x))) ∙
-        ( ap
-          ( _∙ coherence-square-cocone f g c' x)
-          ( inv
-            ( naturality-tr-constant-type-family
-              ( coherence-square-cocone f g c'' x)
-              ( K (f x))))) ∙
-        ( assoc
+        ( right-whisker-concat-coherence-square-identifications
           ( tr-constant-type-family
-            ( coherence-square-cocone f g c'' x)
-            ( horizontal-map-cocone f g c (f x)))
+            ( 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))
-          ( coherence-square-cocone f g c' 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/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index 2bf9a843b7..9fcda8bd15 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -340,7 +340,7 @@ module _
       ( 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 -->
+<!-- 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