From 8ebe1d3c6f17ff4140a75f9053096a237afcf8f0 Mon Sep 17 00:00:00 2001
From: VojtechStep <vojtechstepancik@outlook.com>
Date: Thu, 16 May 2024 22:30:29 +0200
Subject: [PATCH 01/10] Make double arrow implicit if possible

---
 .../coequalizers.lagda.md                     |   9 +-
 ...cocones-under-sequential-diagrams.lagda.md |  49 ++------
 .../coforks.lagda.md                          |  77 +++++++------
 .../dependent-coforks.lagda.md                | 108 +++++++++---------
 ...t-universal-property-coequalizers.lagda.md |  92 ++++++++-------
 ...rsal-property-sequential-colimits.lagda.md |  25 ++--
 ...-under-equivalences-double-arrows.lagda.md |  20 ++--
 .../flattening-lemma-coequalizers.lagda.md    |  32 +++---
 ...ttening-lemma-sequential-colimits.lagda.md |   9 +-
 ...rks-under-morphisms-double-arrows.lagda.md |  14 +--
 .../sequential-colimits.lagda.md              |   3 +-
 .../universal-property-coequalizers.lagda.md  |  82 ++++++-------
 ...rsal-property-sequential-colimits.lagda.md |  30 ++---
 13 files changed, 242 insertions(+), 308 deletions(-)

diff --git a/src/synthetic-homotopy-theory/coequalizers.lagda.md b/src/synthetic-homotopy-theory/coequalizers.lagda.md
index a89b394839..62861dbe19 100644
--- a/src/synthetic-homotopy-theory/coequalizers.lagda.md
+++ b/src/synthetic-homotopy-theory/coequalizers.lagda.md
@@ -77,11 +77,9 @@ module _
           ( horizontal-map-span-cocone-cofork a))
 
     dup-standard-coequalizer :
-      dependent-universal-property-coequalizer a cofork-standard-coequalizer
+      dependent-universal-property-coequalizer cofork-standard-coequalizer
     dup-standard-coequalizer =
       dependent-universal-property-coequalizer-dependent-universal-property-pushout
-        ( a)
-        ( cofork-standard-coequalizer)
         ( λ P →
           tr
             ( λ c →
@@ -103,9 +101,8 @@ module _
               ( P)))
 
     up-standard-coequalizer :
-      universal-property-coequalizer a cofork-standard-coequalizer
+      universal-property-coequalizer cofork-standard-coequalizer
     up-standard-coequalizer =
-      universal-property-dependent-universal-property-coequalizer a
-        ( cofork-standard-coequalizer)
+      universal-property-dependent-universal-property-coequalizer
         ( dup-standard-coequalizer)
 ```
diff --git a/src/synthetic-homotopy-theory/coforks-cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/coforks-cocones-under-sequential-diagrams.lagda.md
index 0efd91005f..7bf9afe768 100644
--- a/src/synthetic-homotopy-theory/coforks-cocones-under-sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/coforks-cocones-under-sequential-diagrams.lagda.md
@@ -233,10 +233,7 @@ module _
 
   dependent-cofork-dependent-cocone-sequential-diagram :
     dependent-cocone-sequential-diagram c P →
-    dependent-cofork
-      ( double-arrow-sequential-diagram A)
-      ( cofork-cocone-sequential-diagram c)
-      ( P)
+    dependent-cofork (cofork-cocone-sequential-diagram c) P
   pr1 (dependent-cofork-dependent-cocone-sequential-diagram d) =
     ind-Σ (map-dependent-cocone-sequential-diagram P d)
   pr2 (dependent-cofork-dependent-cocone-sequential-diagram d) =
@@ -377,9 +374,9 @@ module _
     cofork (double-arrow-sequential-diagram A) X →
     cocone-sequential-diagram A X
   pr1 (cocone-sequential-diagram-cofork e) =
-    ev-pair (map-cofork (double-arrow-sequential-diagram A) e)
+    ev-pair (map-cofork e)
   pr2 (cocone-sequential-diagram-cofork e) =
-    ev-pair (coh-cofork (double-arrow-sequential-diagram A) e)
+    ev-pair (coh-cofork e)
 
   abstract
     is-section-cocone-sequential-diagram-cofork :
@@ -431,15 +428,12 @@ module _
     coherence-triangle-maps
       ( cocone-map-sequential-diagram c {Y = Y})
       ( cocone-sequential-diagram-cofork)
-      ( cofork-map
-        ( double-arrow-sequential-diagram A)
-        ( cofork-cocone-sequential-diagram c))
+      ( cofork-map (cofork-cocone-sequential-diagram c))
   triangle-cocone-sequential-diagram-cofork h =
     eq-htpy-cocone-sequential-diagram A
       ( cocone-map-sequential-diagram c h)
       ( cocone-sequential-diagram-cofork
         ( cofork-map
-          ( double-arrow-sequential-diagram A)
           ( cofork-cocone-sequential-diagram c)
           ( h)))
       ( refl-htpy-cocone-sequential-diagram _ _)
@@ -468,23 +462,14 @@ module _
   where
 
   dependent-cocone-sequential-diagram-dependent-cofork :
-    dependent-cofork
-      ( double-arrow-sequential-diagram A)
-      ( cofork-cocone-sequential-diagram c)
-      ( P) →
+    dependent-cofork (cofork-cocone-sequential-diagram c) P →
     dependent-cocone-sequential-diagram c P
   pr1 (dependent-cocone-sequential-diagram-dependent-cofork e) =
     ev-pair
-      ( map-dependent-cofork
-        ( double-arrow-sequential-diagram A)
-        ( P)
-        ( e))
+      ( map-dependent-cofork P e)
   pr2 (dependent-cocone-sequential-diagram-dependent-cofork e) =
     ev-pair
-      ( coherence-dependent-cofork
-        ( double-arrow-sequential-diagram A)
-        ( P)
-        ( e))
+      ( coherence-dependent-cofork P e)
 
   abstract
     is-section-dependent-cocone-sequential-diagram-dependent-cofork :
@@ -492,13 +477,11 @@ module _
         ( dependent-cofork-dependent-cocone-sequential-diagram P)
         ( dependent-cocone-sequential-diagram-dependent-cofork)
     is-section-dependent-cocone-sequential-diagram-dependent-cofork e =
-      eq-htpy-dependent-cofork
-        ( double-arrow-sequential-diagram A)
-        ( P)
+      eq-htpy-dependent-cofork P
         ( dependent-cofork-dependent-cocone-sequential-diagram P
           ( dependent-cocone-sequential-diagram-dependent-cofork e))
         ( e)
-        ( refl-htpy-dependent-cofork _ _ _)
+        ( refl-htpy-dependent-cofork _ _)
 
     is-retraction-dependent-cocone-sequential-diagram-dependent-cofork :
       is-retraction
@@ -520,10 +503,7 @@ module _
       ( is-section-dependent-cocone-sequential-diagram-dependent-cofork)
 
   equiv-dependent-cocone-sequential-diagram-dependent-cofork :
-    dependent-cofork
-      ( double-arrow-sequential-diagram A)
-      ( cofork-cocone-sequential-diagram c)
-      ( P) ≃
+    dependent-cofork (cofork-cocone-sequential-diagram c) P ≃
     dependent-cocone-sequential-diagram c P
   pr1 equiv-dependent-cocone-sequential-diagram-dependent-cofork =
     dependent-cocone-sequential-diagram-dependent-cofork
@@ -540,16 +520,11 @@ module _
     coherence-triangle-maps
       ( dependent-cocone-map-sequential-diagram c P)
       ( dependent-cocone-sequential-diagram-dependent-cofork P)
-      ( dependent-cofork-map
-        ( double-arrow-sequential-diagram A)
-        ( cofork-cocone-sequential-diagram c))
+      ( dependent-cofork-map (cofork-cocone-sequential-diagram c))
   triangle-dependent-cocone-sequential-diagram-dependent-cofork h =
     eq-htpy-dependent-cocone-sequential-diagram P
       ( dependent-cocone-map-sequential-diagram c P h)
       ( dependent-cocone-sequential-diagram-dependent-cofork P
-        ( dependent-cofork-map
-          ( double-arrow-sequential-diagram A)
-          ( cofork-cocone-sequential-diagram c)
-          ( h)))
+        ( dependent-cofork-map (cofork-cocone-sequential-diagram c) h))
       ( refl-htpy-dependent-cocone-sequential-diagram _ _)
 ```
diff --git a/src/synthetic-homotopy-theory/coforks.lagda.md b/src/synthetic-homotopy-theory/coforks.lagda.md
index fa5ea65e19..d83711e13b 100644
--- a/src/synthetic-homotopy-theory/coforks.lagda.md
+++ b/src/synthetic-homotopy-theory/coforks.lagda.md
@@ -76,15 +76,16 @@ module _
   cofork X =
     Σ (codomain-double-arrow a → X) (coherence-cofork)
 
-  module _
-    {X : UU l3} (e : cofork X)
-    where
+module _
+  {l1 l2 l3 : Level} {a : double-arrow l1 l2}
+  {X : UU l3} (e : cofork a X)
+  where
 
-    map-cofork : codomain-double-arrow a → X
-    map-cofork = pr1 e
+  map-cofork : codomain-double-arrow a → X
+  map-cofork = pr1 e
 
-    coh-cofork : coherence-cofork map-cofork
-    coh-cofork = pr2 e
+  coh-cofork : coherence-cofork a map-cofork
+  coh-cofork = pr2 e
 ```
 
 ### Homotopies of coforks
@@ -95,20 +96,20 @@ given homotopy and the appropriate cofork homotopy in either order.
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 : Level} {a : double-arrow l1 l2} {X : UU l3}
   where
 
   coherence-htpy-cofork :
     (e e' : cofork a X) →
-    (K : map-cofork a e ~ map-cofork a e') →
+    (K : map-cofork e ~ map-cofork e') →
     UU (l1 ⊔ l3)
   coherence-htpy-cofork e e' K =
-    ( (coh-cofork a e) ∙h (K ·r right-map-double-arrow a)) ~
-    ( (K ·r left-map-double-arrow a) ∙h (coh-cofork a e'))
+    ( (coh-cofork e) ∙h (K ·r right-map-double-arrow a)) ~
+    ( (K ·r left-map-double-arrow a) ∙h (coh-cofork e'))
 
   htpy-cofork : cofork a X → cofork a X → UU (l1 ⊔ l2 ⊔ l3)
   htpy-cofork e e' =
-    Σ ( map-cofork a e ~ map-cofork a e')
+    Σ ( map-cofork e ~ map-cofork e')
       ( coherence-htpy-cofork e e')
 ```
 
@@ -126,13 +127,13 @@ a new cofork `h ∘ e`.
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 : Level} {a : double-arrow l1 l2} {X : UU l3}
   (e : cofork a X)
   where
 
   cofork-map : {l : Level} {Y : UU l} → (X → Y) → cofork a Y
-  pr1 (cofork-map h) = h ∘ map-cofork a e
-  pr2 (cofork-map h) = h ·l (coh-cofork a e)
+  pr1 (cofork-map h) = h ∘ map-cofork e
+  pr2 (cofork-map h) = h ·l (coh-cofork e)
 ```
 
 ## Properties
@@ -144,35 +145,35 @@ module _
   {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
   where
 
-  refl-htpy-cofork : (e : cofork a X) → htpy-cofork a e e
+  refl-htpy-cofork : (e : cofork a X) → htpy-cofork e e
   pr1 (refl-htpy-cofork e) = refl-htpy
   pr2 (refl-htpy-cofork e) = right-unit-htpy
 
   htpy-cofork-eq :
-    (e e' : cofork a X) → (e ＝ e') → htpy-cofork a e e'
+    (e e' : cofork a X) → (e ＝ e') → htpy-cofork e e'
   htpy-cofork-eq e .e refl = refl-htpy-cofork e
 
   abstract
     is-torsorial-htpy-cofork :
-      (e : cofork a X) → is-torsorial (htpy-cofork a e)
+      (e : cofork a X) → is-torsorial (htpy-cofork e)
     is-torsorial-htpy-cofork e =
       is-torsorial-Eq-structure
-        ( is-torsorial-htpy (map-cofork a e))
-        ( map-cofork a e , refl-htpy)
+        ( is-torsorial-htpy (map-cofork e))
+        ( map-cofork e , refl-htpy)
         ( is-contr-is-equiv'
-          ( Σ ( coherence-cofork a (map-cofork a e))
-              ( λ K → coh-cofork a e ~ K))
+          ( Σ ( coherence-cofork a (map-cofork e))
+              ( λ K → coh-cofork e ~ K))
           ( tot (λ K M → right-unit-htpy ∙h M))
           ( is-equiv-tot-is-fiberwise-equiv
             ( is-equiv-concat-htpy right-unit-htpy))
-          ( is-torsorial-htpy (coh-cofork a e)))
+          ( is-torsorial-htpy (coh-cofork e)))
 
     is-equiv-htpy-cofork-eq :
       (e e' : cofork a X) → is-equiv (htpy-cofork-eq e e')
     is-equiv-htpy-cofork-eq e =
       fundamental-theorem-id (is-torsorial-htpy-cofork e) (htpy-cofork-eq e)
 
-  eq-htpy-cofork : (e e' : cofork a X) → htpy-cofork a e e' → e ＝ e'
+  eq-htpy-cofork : (e e' : cofork a X) → htpy-cofork e e' → e ＝ e'
   eq-htpy-cofork e e' = map-inv-is-equiv (is-equiv-htpy-cofork-eq e e')
 ```
 
@@ -180,17 +181,17 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 : Level} {a : double-arrow l1 l2} {X : UU l3}
   (e : cofork a X)
   where
 
-  cofork-map-id : cofork-map a e id ＝ e
+  cofork-map-id : cofork-map e id ＝ e
   cofork-map-id =
     eq-htpy-cofork a
-      ( cofork-map a e id)
+      ( cofork-map e id)
       ( e)
       ( ( refl-htpy) ,
-        ( right-unit-htpy ∙h left-unit-law-left-whisker-comp (coh-cofork a e)))
+        ( right-unit-htpy ∙h left-unit-law-left-whisker-comp (coh-cofork e)))
 ```
 
 ### Postcomposing coforks distributes over function composition
@@ -204,21 +205,21 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} (a : double-arrow l1 l2)
+  {l1 l2 l3 l4 l5 : Level} {a : double-arrow l1 l2}
   {X : UU l3} {Y : UU l4} {Z : UU l5}
   (e : cofork a X)
   where
 
   cofork-map-comp :
     (h : X → Y) (k : Y → Z) →
-    cofork-map a e (k ∘ h) ＝ cofork-map a (cofork-map a e h) k
+    cofork-map e (k ∘ h) ＝ cofork-map (cofork-map e h) k
   cofork-map-comp h k =
     eq-htpy-cofork a
-      ( cofork-map a e (k ∘ h))
-      ( cofork-map a (cofork-map a e h) k)
+      ( cofork-map e (k ∘ h))
+      ( cofork-map (cofork-map e h) k)
       ( ( refl-htpy) ,
         ( ( right-unit-htpy) ∙h
-          ( inv-preserves-comp-left-whisker-comp k h (coh-cofork a e))))
+          ( inv-preserves-comp-left-whisker-comp k h (coh-cofork e))))
 ```
 
 ### Coforks are special cases of cocones under spans
@@ -280,10 +281,10 @@ module _
         ( inr))
 
     horizontal-map-cocone-cofork : cofork a X → domain-double-arrow a → X
-    horizontal-map-cocone-cofork e = map-cofork a e ∘ left-map-double-arrow a
+    horizontal-map-cocone-cofork e = map-cofork e ∘ left-map-double-arrow a
 
     vertical-map-cocone-cofork : cofork a X → codomain-double-arrow a → X
-    vertical-map-cocone-cofork e = map-cofork a e
+    vertical-map-cocone-cofork e = map-cofork e
 
     coherence-square-cocone-cofork :
       (e : cofork a X) →
@@ -293,7 +294,7 @@ module _
         ( vertical-map-cocone-cofork e)
         ( horizontal-map-cocone-cofork e)
     coherence-square-cocone-cofork e (inl x) = refl
-    coherence-square-cocone-cofork e (inr x) = coh-cofork a e x
+    coherence-square-cocone-cofork e (inr x) = coh-cofork e x
 
     cocone-codiagonal-cofork :
       cofork a X →
@@ -359,7 +360,7 @@ module _
     {l3 l4 : Level} {X : UU l3} {Y : UU l4} →
     (e : cofork a X) →
     coherence-triangle-maps
-      ( cofork-map a e {Y = Y})
+      ( cofork-map e {Y = Y})
       ( cofork-cocone-codiagonal)
       ( cocone-map
         ( vertical-map-span-cocone-cofork)
@@ -367,7 +368,7 @@ module _
         ( cocone-codiagonal-cofork e))
   triangle-cofork-cocone e h =
     eq-htpy-cofork a
-      ( cofork-map a e h)
+      ( cofork-map e h)
       ( cofork-cocone-codiagonal
         ( cocone-map
           ( vertical-map-span-cocone-cofork)
diff --git a/src/synthetic-homotopy-theory/dependent-coforks.lagda.md b/src/synthetic-homotopy-theory/dependent-coforks.lagda.md
index 39b40000f5..27b929c08c 100644
--- a/src/synthetic-homotopy-theory/dependent-coforks.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-coforks.lagda.md
@@ -69,33 +69,33 @@ for double arrows.
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 l4 : Level} {a : double-arrow l1 l2} {X : UU l3}
   (e : cofork a X) (P : X → UU l4)
   where
 
   dependent-cofork : UU (l1 ⊔ l2 ⊔ l4)
   dependent-cofork =
-    Σ ( (b : codomain-double-arrow a) → P (map-cofork a e b))
+    Σ ( (b : codomain-double-arrow a) → P (map-cofork e b))
       ( λ k →
         (x : domain-double-arrow a) →
         dependent-identification P
-          ( coh-cofork a e x)
+          ( coh-cofork e x)
           ( k (left-map-double-arrow a x))
           ( k (right-map-double-arrow a x)))
 
 module _
-  {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 l4 : Level} {a : double-arrow l1 l2} {X : UU l3}
   {e : cofork a X} (P : X → UU l4)
-  (k : dependent-cofork a e P)
+  (k : dependent-cofork e P)
   where
 
-  map-dependent-cofork : (b : codomain-double-arrow a) → P (map-cofork a e b)
+  map-dependent-cofork : (b : codomain-double-arrow a) → P (map-cofork e b)
   map-dependent-cofork = pr1 k
 
   coherence-dependent-cofork :
     (x : domain-double-arrow a) →
     dependent-identification P
-      ( coh-cofork a e x)
+      ( coh-cofork e x)
       ( map-dependent-cofork (left-map-double-arrow a x))
       ( map-dependent-cofork (right-map-double-arrow a x))
   coherence-dependent-cofork = pr2 k
@@ -108,24 +108,24 @@ together with a coherence condition.
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 l4 : Level} {a : double-arrow l1 l2} {X : UU l3}
   {e : cofork a X} (P : X → UU l4)
   where
 
   coherence-htpy-dependent-cofork :
-    (k k' : dependent-cofork a e P) →
-    (K : map-dependent-cofork a P k ~ map-dependent-cofork a P k') →
+    (k k' : dependent-cofork e P) →
+    (K : map-dependent-cofork P k ~ map-dependent-cofork P k') →
     UU (l1 ⊔ l4)
   coherence-htpy-dependent-cofork k k' K =
-    ( (coherence-dependent-cofork a P k) ∙h (K ·r right-map-double-arrow a)) ~
-    ( ( (λ {x} → tr P (coh-cofork a e x)) ·l (K ·r left-map-double-arrow a)) ∙h
-      ( coherence-dependent-cofork a P k'))
+    ( (coherence-dependent-cofork P k) ∙h (K ·r right-map-double-arrow a)) ~
+    ( ( (λ {x} → tr P (coh-cofork e x)) ·l (K ·r left-map-double-arrow a)) ∙h
+      ( coherence-dependent-cofork P k'))
 
   htpy-dependent-cofork :
-    (k k' : dependent-cofork a e P) →
+    (k k' : dependent-cofork e P) →
     UU (l1 ⊔ l2 ⊔ l4)
   htpy-dependent-cofork k k' =
-    Σ ( map-dependent-cofork a P k ~ map-dependent-cofork a P k')
+    Σ ( map-dependent-cofork P k ~ map-dependent-cofork P k')
       ( coherence-htpy-dependent-cofork k k')
 ```
 
@@ -143,14 +143,14 @@ a dependent map, according to the diagram
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 : Level} {a : double-arrow l1 l2} {X : UU l3}
   (e : cofork a X)
   where
 
   dependent-cofork-map :
-    {l : Level} {P : X → UU l} → ((x : X) → P x) → dependent-cofork a e P
-  pr1 (dependent-cofork-map h) = h ∘ map-cofork a e
-  pr2 (dependent-cofork-map h) = apd h ∘ coh-cofork a e
+    {l : Level} {P : X → UU l} → ((x : X) → P x) → dependent-cofork e P
+  pr1 (dependent-cofork-map h) = h ∘ map-cofork e
+  pr2 (dependent-cofork-map h) = apd h ∘ coh-cofork e
 ```
 
 ## Properties
@@ -159,34 +159,34 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 l4 : Level} {a : double-arrow l1 l2} {X : UU l3}
   {e : cofork a X} (P : X → UU l4)
   where
 
   refl-htpy-dependent-cofork :
-    (k : dependent-cofork a e P) →
-    htpy-dependent-cofork a P k k
+    (k : dependent-cofork e P) →
+    htpy-dependent-cofork P k k
   pr1 (refl-htpy-dependent-cofork k) = refl-htpy
   pr2 (refl-htpy-dependent-cofork k) = right-unit-htpy
 
   htpy-dependent-cofork-eq :
-    (k k' : dependent-cofork a e P) →
-    (k ＝ k') → htpy-dependent-cofork a P k k'
+    (k k' : dependent-cofork e P) →
+    (k ＝ k') → htpy-dependent-cofork P k k'
   htpy-dependent-cofork-eq k .k refl = refl-htpy-dependent-cofork k
 
   abstract
     is-torsorial-htpy-dependent-cofork :
-      (k : dependent-cofork a e P) →
-      is-torsorial (htpy-dependent-cofork a P k)
+      (k : dependent-cofork e P) →
+      is-torsorial (htpy-dependent-cofork P k)
     is-torsorial-htpy-dependent-cofork k =
       is-torsorial-Eq-structure
-        ( is-torsorial-htpy (map-dependent-cofork a P k))
-        ( map-dependent-cofork a P k , refl-htpy)
+        ( is-torsorial-htpy (map-dependent-cofork P k))
+        ( map-dependent-cofork P k , refl-htpy)
         ( is-torsorial-htpy
-          ( coherence-dependent-cofork a P k ∙h refl-htpy))
+          ( coherence-dependent-cofork P k ∙h refl-htpy))
 
     is-equiv-htpy-dependent-cofork-eq :
-      (k k' : dependent-cofork a e P) →
+      (k k' : dependent-cofork e P) →
       is-equiv (htpy-dependent-cofork-eq k k')
     is-equiv-htpy-dependent-cofork-eq k =
       fundamental-theorem-id
@@ -194,8 +194,8 @@ module _
         ( htpy-dependent-cofork-eq k)
 
   eq-htpy-dependent-cofork :
-    (k k' : dependent-cofork a e P) →
-    htpy-dependent-cofork a P k k' → k ＝ k'
+    (k k' : dependent-cofork e P) →
+    htpy-dependent-cofork P k k' → k ＝ k'
   eq-htpy-dependent-cofork k k' =
     map-inv-is-equiv (is-equiv-htpy-dependent-cofork-eq k k')
 ```
@@ -204,12 +204,12 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 l4 : Level} {a : double-arrow l1 l2} {X : UU l3}
   (e : cofork a X) (Y : UU l4)
   where
 
   compute-dependent-cofork-constant-family :
-    dependent-cofork a e (λ _ → Y) ≃ cofork a Y
+    dependent-cofork e (λ _ → Y) ≃ cofork a Y
   compute-dependent-cofork-constant-family =
     equiv-tot
       ( λ h →
@@ -218,30 +218,30 @@ module _
             equiv-concat
               ( inv
                 ( tr-constant-type-family
-                  ( coh-cofork a e x)
+                  ( coh-cofork e x)
                   ( h (left-map-double-arrow a x))))
               ( h (right-map-double-arrow a x))))
 
   map-compute-dependent-cofork-constant-family :
-    dependent-cofork a e (λ _ → Y) → cofork a Y
+    dependent-cofork e (λ _ → Y) → cofork a Y
   map-compute-dependent-cofork-constant-family =
     map-equiv compute-dependent-cofork-constant-family
 
   triangle-compute-dependent-cofork-constant-family :
     coherence-triangle-maps
-      ( cofork-map a e)
+      ( cofork-map e)
       ( map-compute-dependent-cofork-constant-family)
-      ( dependent-cofork-map a e)
+      ( dependent-cofork-map e)
   triangle-compute-dependent-cofork-constant-family h =
     eq-htpy-cofork a
-      ( cofork-map a e h)
+      ( cofork-map e h)
       ( map-compute-dependent-cofork-constant-family
-        ( dependent-cofork-map a e h))
+        ( dependent-cofork-map e h))
       ( ( refl-htpy) ,
         ( right-unit-htpy ∙h
           ( λ x →
             left-transpose-eq-concat _ _ _
-              ( inv (apd-constant-type-family h (coh-cofork a e x))))))
+              ( inv (apd-constant-type-family h (coh-cofork e x))))))
 ```
 
 ### Dependent coforks are special cases of dependent cocones under spans
@@ -252,7 +252,7 @@ on `P` over a cocone corresponding to `e` via `cocone-codiagonal-cofork`.
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 : Level} {a : double-arrow l1 l2} {X : UU l3}
   (e : cofork a X)
   where
 
@@ -266,7 +266,7 @@ module _
         ( horizontal-map-span-cocone-cofork a)
         ( cocone-codiagonal-cofork a e)
         ( P) →
-      dependent-cofork a e P
+      dependent-cofork e P
     pr1 (dependent-cofork-dependent-cocone-codiagonal k) =
       vertical-map-dependent-cocone
         ( vertical-map-span-cocone-cofork a)
@@ -277,7 +277,7 @@ module _
     pr2 (dependent-cofork-dependent-cocone-codiagonal k) x =
       inv
         ( ap
-          ( tr P (coh-cofork a e x))
+          ( tr P (coh-cofork e x))
           ( coherence-square-dependent-cocone
             ( vertical-map-span-cocone-cofork a)
             ( horizontal-map-span-cocone-cofork a)
@@ -294,20 +294,20 @@ module _
         ( inr x)
 
     dependent-cocone-codiagonal-dependent-cofork :
-      dependent-cofork a e P →
+      dependent-cofork e P →
       dependent-cocone
         ( vertical-map-span-cocone-cofork a)
         ( horizontal-map-span-cocone-cofork a)
         ( cocone-codiagonal-cofork a e)
         ( P)
     pr1 (dependent-cocone-codiagonal-dependent-cofork k) =
-      map-dependent-cofork a P k ∘ left-map-double-arrow a
+      map-dependent-cofork P k ∘ left-map-double-arrow a
     pr1 (pr2 (dependent-cocone-codiagonal-dependent-cofork k)) =
-      map-dependent-cofork a P k
+      map-dependent-cofork P k
     pr2 (pr2 (dependent-cocone-codiagonal-dependent-cofork k)) (inl a) =
       refl
     pr2 (pr2 (dependent-cocone-codiagonal-dependent-cofork k)) (inr x) =
-      coherence-dependent-cofork a P k x
+      coherence-dependent-cofork P k x
 
     abstract
       is-section-dependent-cocone-codiagonal-dependent-cofork :
@@ -315,7 +315,7 @@ module _
           ( dependent-cocone-codiagonal-dependent-cofork)) ~
         ( id)
       is-section-dependent-cocone-codiagonal-dependent-cofork k =
-        eq-htpy-dependent-cofork a P
+        eq-htpy-dependent-cofork P
           ( dependent-cofork-dependent-cocone-codiagonal
             ( dependent-cocone-codiagonal-dependent-cofork k))
           ( k)
@@ -376,7 +376,7 @@ module _
                   right-whisker-concat
                     ( inv
                       ( ap-inv
-                        ( tr P (coh-cofork a e x))
+                        ( tr P (coh-cofork e x))
                         ( coherence-square-dependent-cocone
                           ( vertical-map-span-cocone-cofork a)
                           ( horizontal-map-span-cocone-cofork a)
@@ -406,7 +406,7 @@ module _
         ( horizontal-map-span-cocone-cofork a)
         ( cocone-codiagonal-cofork a e)
         ( P) ≃
-      dependent-cofork a e P
+      dependent-cofork e P
     pr1 equiv-dependent-cofork-dependent-cocone-codiagonal =
       dependent-cofork-dependent-cocone-codiagonal
     pr2 equiv-dependent-cofork-dependent-cocone-codiagonal =
@@ -415,7 +415,7 @@ module _
   triangle-dependent-cofork-dependent-cocone-codiagonal :
     {l4 : Level} (P : X → UU l4) →
     coherence-triangle-maps
-      ( dependent-cofork-map a e)
+      ( dependent-cofork-map e)
       ( dependent-cofork-dependent-cocone-codiagonal P)
       ( dependent-cocone-map
         ( vertical-map-span-cocone-cofork a)
@@ -423,8 +423,8 @@ module _
         ( cocone-codiagonal-cofork a e)
         ( P))
   triangle-dependent-cofork-dependent-cocone-codiagonal P h =
-    eq-htpy-dependent-cofork a P
-      ( dependent-cofork-map a e h)
+    eq-htpy-dependent-cofork P
+      ( dependent-cofork-map e h)
       ( dependent-cofork-dependent-cocone-codiagonal P
         ( dependent-cocone-map
           ( vertical-map-span-cocone-cofork a)
diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-coequalizers.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-coequalizers.lagda.md
index ba60811fcb..ae1e8f8012 100644
--- a/src/synthetic-homotopy-theory/dependent-universal-property-coequalizers.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-universal-property-coequalizers.lagda.md
@@ -44,22 +44,22 @@ dependent-cofork-map : ((x : X) → P x) → dependent-cocone e P.
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 : Level} {a : double-arrow l1 l2} {X : UU l3}
   (e : cofork a X)
   where
 
   dependent-universal-property-coequalizer : UUω
   dependent-universal-property-coequalizer =
-    {l : Level} (P : X → UU l) → is-equiv (dependent-cofork-map a e {P = P})
+    {l : Level} (P : X → UU l) → is-equiv (dependent-cofork-map e {P = P})
 
 module _
-  {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) {X : UU l3}
-  (e : cofork a X) {P : X → UU l4}
-  (dup-coequalizer : dependent-universal-property-coequalizer a e)
+  {l1 l2 l3 l4 : Level} {a : double-arrow l1 l2} {X : UU l3}
+  {e : cofork a X} {P : X → UU l4}
+  (dup-coequalizer : dependent-universal-property-coequalizer e)
   where
 
   map-dependent-universal-property-coequalizer :
-    dependent-cofork a e P →
+    dependent-cofork e P →
     (x : X) → P x
   map-dependent-universal-property-coequalizer =
     map-inv-is-equiv (dup-coequalizer P)
@@ -71,23 +71,23 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) {X : UU l3}
-  (e : cofork a X) {P : X → UU l4}
-  (dup-coequalizer : dependent-universal-property-coequalizer a e)
-  (k : dependent-cofork a e P)
+  {l1 l2 l3 l4 : Level} {a : double-arrow l1 l2} {X : UU l3}
+  {e : cofork a X} {P : X → UU l4}
+  (dup-coequalizer : dependent-universal-property-coequalizer e)
+  (k : dependent-cofork e P)
   where
 
   htpy-dependent-cofork-dependent-universal-property-coequalizer :
-    htpy-dependent-cofork a P
-      ( dependent-cofork-map a e
-        ( map-dependent-universal-property-coequalizer a e
+    htpy-dependent-cofork P
+      ( dependent-cofork-map e
+        ( map-dependent-universal-property-coequalizer
           ( dup-coequalizer)
           ( k)))
       ( k)
   htpy-dependent-cofork-dependent-universal-property-coequalizer =
-    htpy-dependent-cofork-eq a P
-      ( dependent-cofork-map a e
-        ( map-dependent-universal-property-coequalizer a e
+    htpy-dependent-cofork-eq P
+      ( dependent-cofork-map e
+        ( map-dependent-universal-property-coequalizer
           ( dup-coequalizer)
           ( k)))
       ( k)
@@ -97,17 +97,17 @@ module _
     uniqueness-dependent-universal-property-coequalizer :
       is-contr
         ( Σ ((x : X) → P x)
-          ( λ h → htpy-dependent-cofork a P (dependent-cofork-map a e h) k))
+          ( λ h → htpy-dependent-cofork P (dependent-cofork-map e h) k))
     uniqueness-dependent-universal-property-coequalizer =
       is-contr-is-equiv'
-        ( fiber (dependent-cofork-map a e) k)
+        ( fiber (dependent-cofork-map e) k)
         ( tot
           ( λ h →
-            htpy-dependent-cofork-eq a P (dependent-cofork-map a e h) k))
+            htpy-dependent-cofork-eq P (dependent-cofork-map e h) k))
         ( is-equiv-tot-is-fiberwise-equiv
           ( λ h →
-            is-equiv-htpy-dependent-cofork-eq a P
-              ( dependent-cofork-map a e h)
+            is-equiv-htpy-dependent-cofork-eq P
+              ( dependent-cofork-map e h)
               ( k)))
         ( is-contr-map-is-equiv (dup-coequalizer P) k)
 ```
@@ -122,8 +122,8 @@ more precise, asserting that under this mapping,
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
-  (e : cofork a X)
+  {l1 l2 l3 : Level} {a : double-arrow l1 l2} {X : UU l3}
+  {e : cofork a X}
   where
 
   dependent-universal-property-coequalizer-dependent-universal-property-pushout :
@@ -131,24 +131,24 @@ module _
       ( vertical-map-span-cocone-cofork a)
       ( horizontal-map-span-cocone-cofork a)
       ( cocone-codiagonal-cofork a e) →
-    dependent-universal-property-coequalizer a e
+    dependent-universal-property-coequalizer e
   dependent-universal-property-coequalizer-dependent-universal-property-pushout
     ( dup-pushout)
     ( P) =
     is-equiv-left-map-triangle
-      ( dependent-cofork-map a e)
-      ( dependent-cofork-dependent-cocone-codiagonal a e P)
+      ( dependent-cofork-map e)
+      ( dependent-cofork-dependent-cocone-codiagonal e P)
       ( dependent-cocone-map
         ( vertical-map-span-cocone-cofork a)
         ( horizontal-map-span-cocone-cofork a)
         ( cocone-codiagonal-cofork a e)
         ( P))
-      ( triangle-dependent-cofork-dependent-cocone-codiagonal a e P)
+      ( triangle-dependent-cofork-dependent-cocone-codiagonal e P)
       ( dup-pushout P)
-      ( is-equiv-dependent-cofork-dependent-cocone-codiagonal a e P)
+      ( is-equiv-dependent-cofork-dependent-cocone-codiagonal e P)
 
   dependent-universal-property-pushout-dependent-universal-property-coequalizer :
-    dependent-universal-property-coequalizer a e →
+    dependent-universal-property-coequalizer e →
     dependent-universal-property-pushout
       ( vertical-map-span-cocone-cofork a)
       ( horizontal-map-span-cocone-cofork a)
@@ -157,15 +157,15 @@ module _
     ( dup-coequalizer)
     ( P) =
     is-equiv-top-map-triangle
-      ( dependent-cofork-map a e)
-      ( dependent-cofork-dependent-cocone-codiagonal a e P)
+      ( dependent-cofork-map e)
+      ( dependent-cofork-dependent-cocone-codiagonal e P)
       ( dependent-cocone-map
         ( vertical-map-span-cocone-cofork a)
         ( horizontal-map-span-cocone-cofork a)
         ( cocone-codiagonal-cofork a e)
         ( P))
-      ( triangle-dependent-cofork-dependent-cocone-codiagonal a e P)
-      ( is-equiv-dependent-cofork-dependent-cocone-codiagonal a e P)
+      ( triangle-dependent-cofork-dependent-cocone-codiagonal e P)
+      ( is-equiv-dependent-cofork-dependent-cocone-codiagonal e P)
       ( dup-coequalizer P)
 ```
 
@@ -173,36 +173,34 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
-  (e : cofork a X)
+  {l1 l2 l3 : Level} {a : double-arrow l1 l2} {X : UU l3}
+  {e : cofork a X}
   where
 
   universal-property-dependent-universal-property-coequalizer :
-    dependent-universal-property-coequalizer a e →
-    universal-property-coequalizer a e
+    dependent-universal-property-coequalizer e →
+    universal-property-coequalizer e
   universal-property-dependent-universal-property-coequalizer
     ( dup-coequalizer)
     ( Y) =
     is-equiv-left-map-triangle
-      ( cofork-map a e)
-      ( map-compute-dependent-cofork-constant-family a e Y)
-      ( dependent-cofork-map a e)
-      ( triangle-compute-dependent-cofork-constant-family a e Y)
+      ( cofork-map e)
+      ( map-compute-dependent-cofork-constant-family e Y)
+      ( dependent-cofork-map e)
+      ( triangle-compute-dependent-cofork-constant-family e Y)
       ( dup-coequalizer (λ _ → Y))
       ( is-equiv-map-equiv
-        ( compute-dependent-cofork-constant-family a e Y))
+        ( compute-dependent-cofork-constant-family e Y))
 
   dependent-universal-property-universal-property-coequalizer :
-    universal-property-coequalizer a e →
-    dependent-universal-property-coequalizer a e
+    universal-property-coequalizer e →
+    dependent-universal-property-coequalizer e
   dependent-universal-property-universal-property-coequalizer up-coequalizer =
     dependent-universal-property-coequalizer-dependent-universal-property-pushout
-      ( a)
-      ( e)
       ( dependent-universal-property-universal-property-pushout
           ( vertical-map-span-cocone-cofork a)
           ( horizontal-map-span-cocone-cofork a)
           ( cocone-codiagonal-cofork a e)
-          ( universal-property-pushout-universal-property-coequalizer a e
+          ( universal-property-pushout-universal-property-coequalizer
             ( up-coequalizer)))
 ```
diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md
index 449c744b8e..9efdfc8019 100644
--- a/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md
@@ -153,7 +153,6 @@ module _
 
   dependent-universal-property-sequential-colimit-dependent-universal-property-coequalizer :
     dependent-universal-property-coequalizer
-      ( double-arrow-sequential-diagram A)
       ( cofork-cocone-sequential-diagram c) →
     dependent-universal-property-sequential-colimit c
   dependent-universal-property-sequential-colimit-dependent-universal-property-coequalizer
@@ -162,9 +161,7 @@ module _
     is-equiv-left-map-triangle
       ( dependent-cocone-map-sequential-diagram c P)
       ( dependent-cocone-sequential-diagram-dependent-cofork P)
-      ( dependent-cofork-map
-        ( double-arrow-sequential-diagram A)
-        ( cofork-cocone-sequential-diagram c))
+      ( dependent-cofork-map (cofork-cocone-sequential-diagram c))
       ( triangle-dependent-cocone-sequential-diagram-dependent-cofork P)
       ( dup-coequalizer P)
       ( is-equiv-dependent-cocone-sequential-diagram-dependent-cofork P)
@@ -172,7 +169,6 @@ module _
   dependent-universal-property-coequalizer-dependent-universal-property-sequential-colimit :
     dependent-universal-property-sequential-colimit c →
     dependent-universal-property-coequalizer
-      ( double-arrow-sequential-diagram A)
       ( cofork-cocone-sequential-diagram c)
   dependent-universal-property-coequalizer-dependent-universal-property-sequential-colimit
     ( dup-c)
@@ -180,9 +176,7 @@ module _
     is-equiv-top-map-triangle
       ( dependent-cocone-map-sequential-diagram c P)
       ( dependent-cocone-sequential-diagram-dependent-cofork P)
-      ( dependent-cofork-map
-        ( double-arrow-sequential-diagram A)
-        ( cofork-cocone-sequential-diagram c))
+      ( dependent-cofork-map (cofork-cocone-sequential-diagram c))
       ( triangle-dependent-cocone-sequential-diagram-dependent-cofork P)
       ( is-equiv-dependent-cocone-sequential-diagram-dependent-cofork P)
       ( dup-c P)
@@ -193,7 +187,7 @@ module _
 ```agda
 module _
   { l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
-  ( c : cocone-sequential-diagram A X)
+  { c : cocone-sequential-diagram A X}
   where
 
   universal-property-dependent-universal-property-sequential-colimit :
@@ -220,10 +214,7 @@ module _
     dependent-universal-property-sequential-colimit-dependent-universal-property-coequalizer
       ( c)
       ( dependent-universal-property-universal-property-coequalizer
-        ( double-arrow-sequential-diagram A)
-        ( cofork-cocone-sequential-diagram c)
         ( universal-property-coequalizer-universal-property-sequential-colimit
-          ( c)
           ( up-sequential-diagram)))
 ```
 
@@ -256,10 +247,9 @@ module _
           ( c')
           ( h)
           ( H)
-          ( universal-property-dependent-universal-property-sequential-colimit c
+          ( universal-property-dependent-universal-property-sequential-colimit
             ( dup-c))
           ( universal-property-dependent-universal-property-sequential-colimit
-            ( c')
             ( dup-c'))
 
     dependent-universal-property-sequential-colimit-is-equiv-dependent-universal-property-sequential-colimit :
@@ -268,13 +258,13 @@ module _
       dependent-universal-property-sequential-colimit c'
     dependent-universal-property-sequential-colimit-is-equiv-dependent-universal-property-sequential-colimit
       ( dup-c) (is-equiv-h) =
-      dependent-universal-property-universal-property-sequential-colimit c'
+      dependent-universal-property-universal-property-sequential-colimit
         ( universal-property-sequential-colimit-is-equiv-universal-property-sequential-colimit
           ( c)
           ( c')
           ( h)
           ( H)
-          ( universal-property-dependent-universal-property-sequential-colimit c
+          ( universal-property-dependent-universal-property-sequential-colimit
             ( dup-c))
           ( is-equiv-h))
 
@@ -285,7 +275,7 @@ module _
     dependent-universal-property-sequential-colimit-dependent-universal-property-sequential-colimit-is-equiv
       ( is-equiv-h)
       ( dup-c') =
-      dependent-universal-property-universal-property-sequential-colimit c
+      dependent-universal-property-universal-property-sequential-colimit
         ( universal-property-sequential-colimit-universal-property-sequential-colimit-is-equiv
           ( c)
           ( c')
@@ -293,6 +283,5 @@ module _
           ( H)
           ( is-equiv-h)
           ( universal-property-dependent-universal-property-sequential-colimit
-            ( c')
             ( dup-c')))
 ```
diff --git a/src/synthetic-homotopy-theory/equivalences-coforks-under-equivalences-double-arrows.lagda.md b/src/synthetic-homotopy-theory/equivalences-coforks-under-equivalences-double-arrows.lagda.md
index a5fa74bee9..c573ddb4f3 100644
--- a/src/synthetic-homotopy-theory/equivalences-coforks-under-equivalences-double-arrows.lagda.md
+++ b/src/synthetic-homotopy-theory/equivalences-coforks-under-equivalences-double-arrows.lagda.md
@@ -129,8 +129,8 @@ module _
   coherence-map-cofork-equiv-cofork-equiv-double-arrow m =
     coherence-square-maps
       ( codomain-map-equiv-double-arrow a a' e)
-      ( map-cofork a c)
-      ( map-cofork a' c')
+      ( map-cofork c)
+      ( map-cofork c')
       ( map-equiv m)
 
   coherence-equiv-cofork-equiv-double-arrow :
@@ -138,12 +138,12 @@ module _
     UU (l1 ⊔ l6)
   coherence-equiv-cofork-equiv-double-arrow m H =
     ( ( H ·r (left-map-double-arrow a)) ∙h
-      ( ( map-cofork a' c') ·l
+      ( ( map-cofork c') ·l
         ( left-square-equiv-double-arrow a a' e)) ∙h
-      ( (coh-cofork a' c') ·r (domain-map-equiv-double-arrow a a' e))) ~
-    ( ( (map-equiv m) ·l (coh-cofork a c)) ∙h
+      ( (coh-cofork c') ·r (domain-map-equiv-double-arrow a a' e))) ~
+    ( ( (map-equiv m) ·l (coh-cofork c)) ∙h
       ( H ·r (right-map-double-arrow a)) ∙h
-      ( (map-cofork a' c') ·l (right-square-equiv-double-arrow a a' e)))
+      ( (map-cofork c') ·l (right-square-equiv-double-arrow a a' e)))
 
   equiv-cofork-equiv-double-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l6)
   equiv-cofork-equiv-double-arrow =
@@ -174,7 +174,7 @@ module _
     coh-map-cofork-equiv-cofork-equiv-double-arrow = pr1 (pr2 e')
 
     equiv-map-cofork-equiv-cofork-equiv-double-arrow :
-      equiv-arrow (map-cofork a c) (map-cofork a' c')
+      equiv-arrow (map-cofork c) (map-cofork c')
     pr1 equiv-map-cofork-equiv-cofork-equiv-double-arrow =
       codomain-equiv-equiv-double-arrow a a' e
     pr1 (pr2 equiv-map-cofork-equiv-cofork-equiv-double-arrow) =
@@ -183,11 +183,11 @@ module _
       coh-map-cofork-equiv-cofork-equiv-double-arrow
 
     hom-map-cofork-equiv-cofork-equiv-double-arrow :
-      hom-arrow (map-cofork a c) (map-cofork a' c')
+      hom-arrow (map-cofork c) (map-cofork c')
     hom-map-cofork-equiv-cofork-equiv-double-arrow =
       hom-equiv-arrow
-        ( map-cofork a c)
-        ( map-cofork a' c')
+        ( map-cofork c)
+        ( map-cofork c')
         ( equiv-map-cofork-equiv-cofork-equiv-double-arrow)
 
     coh-equiv-cofork-equiv-double-arrow :
diff --git a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
index 96888b334f..b04f7516c4 100644
--- a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
+++ b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
@@ -66,21 +66,21 @@ module _
   where
 
   left-map-double-arrow-flattening-lemma-coequalizer :
-    Σ (domain-double-arrow a) (P ∘ map-cofork a e ∘ left-map-double-arrow a) →
-    Σ (codomain-double-arrow a) (P ∘ map-cofork a e)
+    Σ (domain-double-arrow a) (P ∘ map-cofork e ∘ left-map-double-arrow a) →
+    Σ (codomain-double-arrow a) (P ∘ map-cofork e)
   left-map-double-arrow-flattening-lemma-coequalizer =
     map-Σ-map-base
       ( left-map-double-arrow a)
-      ( P ∘ map-cofork a e)
+      ( P ∘ map-cofork e)
 
   right-map-double-arrow-flattening-lemma-coequalizer :
-    Σ (domain-double-arrow a) (P ∘ map-cofork a e ∘ left-map-double-arrow a) →
-    Σ (codomain-double-arrow a) (P ∘ map-cofork a e)
+    Σ (domain-double-arrow a) (P ∘ map-cofork e ∘ left-map-double-arrow a) →
+    Σ (codomain-double-arrow a) (P ∘ map-cofork e)
   right-map-double-arrow-flattening-lemma-coequalizer =
     map-Σ
-      ( P ∘ map-cofork a e)
+      ( P ∘ map-cofork e)
       ( right-map-double-arrow a)
-      ( λ x → tr P (coh-cofork a e x))
+      ( λ x → tr P (coh-cofork e x))
 
   double-arrow-flattening-lemma-coequalizer : double-arrow (l1 ⊔ l4) (l2 ⊔ l4)
   double-arrow-flattening-lemma-coequalizer =
@@ -90,21 +90,19 @@ module _
 
   cofork-flattening-lemma-coequalizer :
     cofork double-arrow-flattening-lemma-coequalizer (Σ X P)
-  pr1 cofork-flattening-lemma-coequalizer = map-Σ-map-base (map-cofork a e) P
+  pr1 cofork-flattening-lemma-coequalizer = map-Σ-map-base (map-cofork e) P
   pr2 cofork-flattening-lemma-coequalizer =
     coherence-square-maps-map-Σ-map-base P
       ( right-map-double-arrow a)
       ( left-map-double-arrow a)
-      ( map-cofork a e)
-      ( map-cofork a e)
-      ( coh-cofork a e)
+      ( map-cofork e)
+      ( map-cofork e)
+      ( coh-cofork e)
 
   flattening-lemma-coequalizer-statement : UUω
   flattening-lemma-coequalizer-statement =
-    dependent-universal-property-coequalizer a e →
-    universal-property-coequalizer
-      ( double-arrow-flattening-lemma-coequalizer)
-      ( cofork-flattening-lemma-coequalizer)
+    dependent-universal-property-coequalizer e →
+    universal-property-coequalizer (cofork-flattening-lemma-coequalizer)
 ```
 
 ## Properties
@@ -135,8 +133,6 @@ module _
     flattening-lemma-coequalizer : flattening-lemma-coequalizer-statement a P e
     flattening-lemma-coequalizer dup-coequalizer =
       universal-property-coequalizer-universal-property-pushout
-        ( double-arrow-flattening-lemma-coequalizer a P e)
-        ( cofork-flattening-lemma-coequalizer a P e)
         ( universal-property-pushout-bottom-universal-property-pushout-top-cube-is-equiv
           ( vertical-map-span-cocone-cofork
             ( double-arrow-flattening-lemma-coequalizer a P e))
@@ -206,7 +202,5 @@ module _
             ( horizontal-map-span-cocone-cofork a)
             ( cocone-codiagonal-cofork a e)
             ( dependent-universal-property-pushout-dependent-universal-property-coequalizer
-              ( a)
-              ( e)
               ( dup-coequalizer))))
 ```
diff --git a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md
index 9dd5911269..9bd350aeca 100644
--- a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md
@@ -153,7 +153,7 @@ module _
       ( ( right-unit-htpy) ∙h
         ( right-unit-htpy) ∙h
         ( left-unit-law-left-whisker-comp
-          ( coh-cofork _
+          ( coh-cofork
             ( cofork-cocone-sequential-diagram
               ( total-cocone-family-cocone-sequential-diagram c P)))))
 
@@ -164,13 +164,7 @@ module _
         ( total-cocone-family-cocone-sequential-diagram c P)
     flattening-lemma-sequential-colimit up-c =
       universal-property-sequential-colimit-universal-property-coequalizer
-        ( total-cocone-family-cocone-sequential-diagram c P)
         ( universal-property-coequalizer-equiv-cofork-equiv-double-arrow
-          ( cofork-cocone-sequential-diagram
-            ( total-cocone-family-cocone-sequential-diagram c P))
-          ( cofork-flattening-lemma-coequalizer _
-            ( P)
-            ( cofork-cocone-sequential-diagram c))
           ( equiv-double-arrow-flattening-lemma-sequential-colimit)
           ( equiv-cofork-flattening-lemma-sequential-colimit)
           ( flattening-lemma-coequalizer _
@@ -179,7 +173,6 @@ module _
             ( dependent-universal-property-coequalizer-dependent-universal-property-sequential-colimit
               ( c)
               ( dependent-universal-property-universal-property-sequential-colimit
-                ( c)
                 ( up-c)))))
 ```
 
diff --git a/src/synthetic-homotopy-theory/morphisms-coforks-under-morphisms-double-arrows.lagda.md b/src/synthetic-homotopy-theory/morphisms-coforks-under-morphisms-double-arrows.lagda.md
index 05c6762c56..f0e086a5df 100644
--- a/src/synthetic-homotopy-theory/morphisms-coforks-under-morphisms-double-arrows.lagda.md
+++ b/src/synthetic-homotopy-theory/morphisms-coforks-under-morphisms-double-arrows.lagda.md
@@ -125,8 +125,8 @@ module _
   coherence-map-cofork-hom-cofork-hom-double-arrow u =
     coherence-square-maps
       ( codomain-map-hom-double-arrow a a' h)
-      ( map-cofork a c)
-      ( map-cofork a' c')
+      ( map-cofork c)
+      ( map-cofork c')
       ( u)
 
   coherence-hom-cofork-hom-double-arrow :
@@ -134,12 +134,12 @@ module _
     UU (l1 ⊔ l6)
   coherence-hom-cofork-hom-double-arrow u H =
     ( ( H ·r (left-map-double-arrow a)) ∙h
-      ( ( map-cofork a' c') ·l
+      ( ( map-cofork c') ·l
         ( left-square-hom-double-arrow a a' h)) ∙h
-      ( (coh-cofork a' c') ·r (domain-map-hom-double-arrow a a' h))) ~
-    ( ( u ·l (coh-cofork a c)) ∙h
+      ( (coh-cofork c') ·r (domain-map-hom-double-arrow a a' h))) ~
+    ( ( u ·l (coh-cofork c)) ∙h
       ( H ·r (right-map-double-arrow a)) ∙h
-      ( (map-cofork a' c') ·l (right-square-hom-double-arrow a a' h)))
+      ( (map-cofork c') ·l (right-square-hom-double-arrow a a' h)))
 
   hom-cofork-hom-double-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l6)
   hom-cofork-hom-double-arrow =
@@ -168,7 +168,7 @@ module _
   coh-map-cofork-hom-cofork-hom-double-arrow = pr1 (pr2 m)
 
   hom-map-cofork-hom-cofork-hom-double-arrow :
-    hom-arrow (map-cofork a c) (map-cofork a' c')
+    hom-arrow (map-cofork c) (map-cofork c')
   pr1 hom-map-cofork-hom-cofork-hom-double-arrow =
     codomain-map-hom-double-arrow a a' h
   pr1 (pr2 hom-map-cofork-hom-cofork-hom-double-arrow) =
diff --git a/src/synthetic-homotopy-theory/sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/sequential-colimits.lagda.md
index e0767413bd..6e01be2a76 100644
--- a/src/synthetic-homotopy-theory/sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/sequential-colimits.lagda.md
@@ -71,7 +71,7 @@ module _
   equiv-htpy-htpy-out-of-sequential-colimit up-c f g =
     ( inv-equiv
       ( equiv-dependent-universal-property-sequential-colimit
-        ( dependent-universal-property-universal-property-sequential-colimit c
+        ( dependent-universal-property-universal-property-sequential-colimit
           ( up-c)))) ∘e
     ( equiv-tot
       ( λ K →
@@ -140,7 +140,6 @@ abstract
       ( cocone-standard-sequential-colimit A)
   up-standard-sequential-colimit {A = A} =
     universal-property-dependent-universal-property-sequential-colimit
-      ( cocone-standard-sequential-colimit A)
       ( dup-standard-sequential-colimit)
 
 module _
diff --git a/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md b/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md
index 14abaccfc2..37a8313c9b 100644
--- a/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md
@@ -49,18 +49,18 @@ is an [equivalence](foundation.equivalences.md).
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
+  {l1 l2 l3 : Level} {a : double-arrow l1 l2} {X : UU l3}
   (e : cofork a X)
   where
 
   universal-property-coequalizer : UUω
   universal-property-coequalizer =
-    {l : Level} (Y : UU l) → is-equiv (cofork-map a e {Y = Y})
+    {l : Level} (Y : UU l) → is-equiv (cofork-map e {Y = Y})
 
 module _
-  {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) {X : UU l3}
-  (e : cofork a X) {Y : UU l4}
-  (up-coequalizer : universal-property-coequalizer a e)
+  {l1 l2 l3 l4 : Level} {a : double-arrow l1 l2} {X : UU l3}
+  {e : cofork a X} {Y : UU l4}
+  (up-coequalizer : universal-property-coequalizer e)
   where
 
   map-universal-property-coequalizer : cofork a Y → (X → Y)
@@ -73,33 +73,33 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) {X : UU l3}
-  (e : cofork a X) {Y : UU l4}
-  (up-coequalizer : universal-property-coequalizer a e)
+  {l1 l2 l3 l4 : Level} {a : double-arrow l1 l2} {X : UU l3}
+  {e : cofork a X} {Y : UU l4}
+  (up-coequalizer : universal-property-coequalizer e)
   (e' : cofork a Y)
   where
 
   htpy-cofork-map-universal-property-coequalizer :
-    htpy-cofork a
-      ( cofork-map a e
-        ( map-universal-property-coequalizer a e up-coequalizer e'))
+    htpy-cofork
+      ( cofork-map e
+        ( map-universal-property-coequalizer up-coequalizer e'))
       ( e')
   htpy-cofork-map-universal-property-coequalizer =
     htpy-cofork-eq a
-      ( cofork-map a e
-        ( map-universal-property-coequalizer a e up-coequalizer e'))
+      ( cofork-map e
+        ( map-universal-property-coequalizer up-coequalizer e'))
       ( e')
       ( is-section-map-inv-is-equiv (up-coequalizer Y) e')
 
   abstract
     uniqueness-map-universal-property-coequalizer :
-      is-contr (Σ (X → Y) (λ h → htpy-cofork a (cofork-map a e h) e'))
+      is-contr (Σ (X → Y) (λ h → htpy-cofork (cofork-map e h) e'))
     uniqueness-map-universal-property-coequalizer =
       is-contr-is-equiv'
-        ( fiber (cofork-map a e) e')
-        ( tot (λ h → htpy-cofork-eq a (cofork-map a e h) e'))
+        ( fiber (cofork-map e) e')
+        ( tot (λ h → htpy-cofork-eq a (cofork-map e h) e'))
         ( is-equiv-tot-is-fiberwise-equiv
-          ( λ h → is-equiv-htpy-cofork-eq a (cofork-map a e h) e'))
+          ( λ h → is-equiv-htpy-cofork-eq a (cofork-map e h) e'))
         ( is-contr-map-is-equiv (up-coequalizer Y) e')
 ```
 
@@ -113,8 +113,8 @@ more precise, asserting that under this mapping,
 
 ```agda
 module _
-  {l1 l2 l3 : Level} (a : double-arrow l1 l2) {X : UU l3}
-  (e : cofork a X)
+  {l1 l2 l3 : Level} {a : double-arrow l1 l2} {X : UU l3}
+  {e : cofork a X}
   where
 
   universal-property-coequalizer-universal-property-pushout :
@@ -122,10 +122,10 @@ module _
       ( vertical-map-span-cocone-cofork a)
       ( horizontal-map-span-cocone-cofork a)
       ( cocone-codiagonal-cofork a e) →
-      universal-property-coequalizer a e
+      universal-property-coequalizer e
   universal-property-coequalizer-universal-property-pushout up-pushout Y =
     is-equiv-left-map-triangle
-      ( cofork-map a e)
+      ( cofork-map e)
       ( cofork-cocone-codiagonal a)
       ( cocone-map
         ( vertical-map-span-cocone-cofork a)
@@ -136,14 +136,14 @@ module _
       ( is-equiv-cofork-cocone-codiagonal a)
 
   universal-property-pushout-universal-property-coequalizer :
-    universal-property-coequalizer a e →
+    universal-property-coequalizer e →
     universal-property-pushout
       ( vertical-map-span-cocone-cofork a)
       ( horizontal-map-span-cocone-cofork a)
       ( cocone-codiagonal-cofork a e)
   universal-property-pushout-universal-property-coequalizer up-coequalizer Y =
     is-equiv-top-map-triangle
-      ( cofork-map a e)
+      ( cofork-map e)
       ( cofork-cocone-codiagonal a)
       ( cocone-map
         ( vertical-map-span-cocone-cofork a)
@@ -185,16 +185,16 @@ a coequalizer.
 ```agda
 module _
   {l1 l2 l3 l4 l5 l6 : Level}
-  {a : double-arrow l1 l2} {X : UU l3} (c : cofork a X)
-  {a' : double-arrow l4 l5} {Y : UU l6} (c' : cofork a' Y)
+  {a : double-arrow l1 l2} {X : UU l3} {c : cofork a X}
+  {a' : double-arrow l4 l5} {Y : UU l6} {c' : cofork a' Y}
   (e : equiv-double-arrow a a') (e' : equiv-cofork-equiv-double-arrow c c' e)
   where
 
   universal-property-coequalizer-equiv-cofork-equiv-double-arrow :
-    universal-property-coequalizer a' c' →
-    universal-property-coequalizer a c
+    universal-property-coequalizer c' →
+    universal-property-coequalizer c
   universal-property-coequalizer-equiv-cofork-equiv-double-arrow up-c' =
-    universal-property-coequalizer-universal-property-pushout a c
+    universal-property-coequalizer-universal-property-pushout
       ( universal-property-pushout-top-universal-property-pushout-bottom-cube-is-equiv
         ( vertical-map-span-cocone-cofork a')
         ( horizontal-map-span-cocone-cofork a')
@@ -222,8 +222,8 @@ module _
             ( left-map-double-arrow a)
             ( left-map-double-arrow a')
             ( codomain-map-equiv-double-arrow a a' e)
-            ( map-cofork a c)
-            ( map-cofork a' c')
+            ( map-cofork c)
+            ( map-cofork c')
             ( map-equiv-cofork-equiv-double-arrow c c' e e')
             ( left-square-equiv-double-arrow a a' e)
             ( coh-map-cofork-equiv-cofork-equiv-double-arrow c c' e e')))
@@ -255,8 +255,8 @@ module _
             ( left-map-double-arrow a)
             ( left-map-double-arrow a')
             ( codomain-map-equiv-double-arrow a a' e)
-            ( map-cofork a c)
-            ( map-cofork a' c')
+            ( map-cofork c)
+            ( map-cofork c')
             ( map-equiv-cofork-equiv-double-arrow c c' e e')
             ( left-square-equiv-double-arrow a a' e)
             ( coh-map-cofork-equiv-cofork-equiv-double-arrow c c' e e'))
@@ -270,14 +270,14 @@ module _
         ( is-equiv-domain-map-equiv-double-arrow a a' e)
         ( is-equiv-codomain-map-equiv-double-arrow a a' e)
         ( is-equiv-map-equiv-cofork-equiv-double-arrow c c' e e')
-        ( universal-property-pushout-universal-property-coequalizer a' c'
+        ( universal-property-pushout-universal-property-coequalizer
           ( up-c')))
 
   universal-property-coequalizer-equiv-cofork-equiv-double-arrow' :
-    universal-property-coequalizer a c →
-    universal-property-coequalizer a' c'
+    universal-property-coequalizer c →
+    universal-property-coequalizer c'
   universal-property-coequalizer-equiv-cofork-equiv-double-arrow' up-c =
-    universal-property-coequalizer-universal-property-pushout a' c'
+    universal-property-coequalizer-universal-property-pushout
       ( universal-property-pushout-bottom-universal-property-pushout-top-cube-is-equiv
         ( vertical-map-span-cocone-cofork a')
         ( horizontal-map-span-cocone-cofork a')
@@ -305,8 +305,8 @@ module _
             ( left-map-double-arrow a)
             ( left-map-double-arrow a')
             ( codomain-map-equiv-double-arrow a a' e)
-            ( map-cofork a c)
-            ( map-cofork a' c')
+            ( map-cofork c)
+            ( map-cofork c')
             ( map-equiv-cofork-equiv-double-arrow c c' e e')
             ( left-square-equiv-double-arrow a a' e)
             ( coh-map-cofork-equiv-cofork-equiv-double-arrow c c' e e')))
@@ -338,8 +338,8 @@ module _
             ( left-map-double-arrow a)
             ( left-map-double-arrow a')
             ( codomain-map-equiv-double-arrow a a' e)
-            ( map-cofork a c)
-            ( map-cofork a' c')
+            ( map-cofork c)
+            ( map-cofork c')
             ( map-equiv-cofork-equiv-double-arrow c c' e e')
             ( left-square-equiv-double-arrow a a' e)
             ( coh-map-cofork-equiv-cofork-equiv-double-arrow c c' e e'))
@@ -353,5 +353,5 @@ module _
         ( is-equiv-domain-map-equiv-double-arrow a a' e)
         ( is-equiv-codomain-map-equiv-double-arrow a a' e)
         ( is-equiv-map-equiv-cofork-equiv-double-arrow c c' e e')
-        ( universal-property-pushout-universal-property-coequalizer a c up-c))
+        ( universal-property-pushout-universal-property-coequalizer up-c))
 ```
diff --git a/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md
index 8cf231f399..e566be14d1 100644
--- a/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md
@@ -160,13 +160,11 @@ has the universal property of coequalizers.
 ```agda
 module _
   { l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
-  ( c : cocone-sequential-diagram A X)
+  { c : cocone-sequential-diagram A X}
   where
 
   universal-property-sequential-colimit-universal-property-coequalizer :
-    universal-property-coequalizer
-      ( double-arrow-sequential-diagram A)
-      ( cofork-cocone-sequential-diagram c) →
+    universal-property-coequalizer (cofork-cocone-sequential-diagram c) →
     universal-property-sequential-colimit c
   universal-property-sequential-colimit-universal-property-coequalizer
     ( up-cofork)
@@ -174,27 +172,21 @@ module _
     is-equiv-left-map-triangle
       ( cocone-map-sequential-diagram c)
       ( cocone-sequential-diagram-cofork)
-      ( cofork-map
-        ( double-arrow-sequential-diagram A)
-        ( cofork-cocone-sequential-diagram c))
+      ( cofork-map (cofork-cocone-sequential-diagram c))
       ( triangle-cocone-sequential-diagram-cofork c)
       ( up-cofork Y)
       ( is-equiv-cocone-sequential-diagram-cofork)
 
   universal-property-coequalizer-universal-property-sequential-colimit :
     universal-property-sequential-colimit c →
-    universal-property-coequalizer
-      ( double-arrow-sequential-diagram A)
-      ( cofork-cocone-sequential-diagram c)
+    universal-property-coequalizer (cofork-cocone-sequential-diagram c)
   universal-property-coequalizer-universal-property-sequential-colimit
     ( up-sequential-colimit)
     ( Y) =
     is-equiv-top-map-triangle
       ( cocone-map-sequential-diagram c)
       ( cocone-sequential-diagram-cofork)
-      ( cofork-map
-        ( double-arrow-sequential-diagram A)
-        ( cofork-cocone-sequential-diagram c))
+      ( cofork-map (cofork-cocone-sequential-diagram c))
       ( triangle-cocone-sequential-diagram-cofork c)
       ( is-equiv-cocone-sequential-diagram-cofork)
       ( up-sequential-colimit Y)
@@ -216,13 +208,11 @@ module _
     universal-property-sequential-colimit c
   universal-property-sequential-colimit-equiv-cocone-equiv-sequential-diagram
     up-c' =
-    universal-property-sequential-colimit-universal-property-coequalizer c
+    universal-property-sequential-colimit-universal-property-coequalizer
       ( universal-property-coequalizer-equiv-cofork-equiv-double-arrow
-        ( cofork-cocone-sequential-diagram c)
-        ( cofork-cocone-sequential-diagram c')
         ( equiv-double-arrow-equiv-sequential-diagram A B e)
         ( equiv-cofork-equiv-cocone-equiv-sequential-diagram c c' e e')
-        ( universal-property-coequalizer-universal-property-sequential-colimit _
+        ( universal-property-coequalizer-universal-property-sequential-colimit
           ( up-c')))
 
   universal-property-sequential-colimit-equiv-cocone-equiv-sequential-diagram' :
@@ -230,13 +220,11 @@ module _
     universal-property-sequential-colimit c'
   universal-property-sequential-colimit-equiv-cocone-equiv-sequential-diagram'
     up-c =
-    universal-property-sequential-colimit-universal-property-coequalizer c'
+    universal-property-sequential-colimit-universal-property-coequalizer
       ( universal-property-coequalizer-equiv-cofork-equiv-double-arrow'
-        ( cofork-cocone-sequential-diagram c)
-        ( cofork-cocone-sequential-diagram c')
         ( equiv-double-arrow-equiv-sequential-diagram A B e)
         ( equiv-cofork-equiv-cocone-equiv-sequential-diagram c c' e e')
-        ( universal-property-coequalizer-universal-property-sequential-colimit _
+        ( universal-property-coequalizer-universal-property-sequential-colimit
           ( up-c)))
 ```
 

From ddb06c3637d791f658b0a82a4e9ab39017882add Mon Sep 17 00:00:00 2001
From: VojtechStep <vojtechstepancik@outlook.com>
Date: Thu, 16 May 2024 22:31:24 +0200
Subject: [PATCH 02/10] Descent property of coequalizers

---
 src/synthetic-homotopy-theory.lagda.md        |   4 +
 .../descent-data-coequalizers.lagda.md        | 119 +++++++++
 .../descent-property-coequalizers.lagda.md    | 145 +++++++++++
 ...alences-descent-data-coequalizers.lagda.md | 200 +++++++++++++++
 ...rphisms-descent-data-coequalizers.lagda.md | 228 ++++++++++++++++++
 5 files changed, 696 insertions(+)
 create mode 100644 src/synthetic-homotopy-theory/descent-data-coequalizers.lagda.md
 create mode 100644 src/synthetic-homotopy-theory/descent-property-coequalizers.lagda.md
 create mode 100644 src/synthetic-homotopy-theory/equivalences-descent-data-coequalizers.lagda.md
 create mode 100644 src/synthetic-homotopy-theory/morphisms-descent-data-coequalizers.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index dbe44b253b..ba1fbc4726 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -48,7 +48,9 @@ open import synthetic-homotopy-theory.descent-circle-dependent-pair-types public
 open import synthetic-homotopy-theory.descent-circle-equivalence-types public
 open import synthetic-homotopy-theory.descent-circle-function-types public
 open import synthetic-homotopy-theory.descent-circle-subtypes public
+open import synthetic-homotopy-theory.descent-data-coequalizers public
 open import synthetic-homotopy-theory.descent-data-sequential-colimits public
+open import synthetic-homotopy-theory.descent-property-coequalizers public
 open import synthetic-homotopy-theory.descent-property-sequential-colimits public
 open import synthetic-homotopy-theory.double-loop-spaces public
 open import synthetic-homotopy-theory.eckmann-hilton-argument public
@@ -56,6 +58,7 @@ open import synthetic-homotopy-theory.equifibered-sequential-diagrams public
 open import synthetic-homotopy-theory.equivalences-cocones-under-equivalences-sequential-diagrams public
 open import synthetic-homotopy-theory.equivalences-coforks-under-equivalences-double-arrows public
 open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams public
+open import synthetic-homotopy-theory.equivalences-descent-data-coequalizers public
 open import synthetic-homotopy-theory.equivalences-sequential-diagrams public
 open import synthetic-homotopy-theory.families-descent-data-sequential-colimits public
 open import synthetic-homotopy-theory.flattening-lemma-coequalizers public
@@ -83,6 +86,7 @@ open import synthetic-homotopy-theory.morphisms-cocones-under-morphisms-sequenti
 open import synthetic-homotopy-theory.morphisms-coforks-under-morphisms-double-arrows public
 open import synthetic-homotopy-theory.morphisms-dependent-sequential-diagrams public
 open import synthetic-homotopy-theory.morphisms-descent-data-circle public
+open import synthetic-homotopy-theory.morphisms-descent-data-coequalizers public
 open import synthetic-homotopy-theory.morphisms-sequential-diagrams public
 open import synthetic-homotopy-theory.multiplication-circle public
 open import synthetic-homotopy-theory.null-cocones-under-pointed-span-diagrams public
diff --git a/src/synthetic-homotopy-theory/descent-data-coequalizers.lagda.md b/src/synthetic-homotopy-theory/descent-data-coequalizers.lagda.md
new file mode 100644
index 0000000000..7e0b0805a5
--- /dev/null
+++ b/src/synthetic-homotopy-theory/descent-data-coequalizers.lagda.md
@@ -0,0 +1,119 @@
+# Descent data for coequalizers
+
+```agda
+module synthetic-homotopy-theory.descent-data-coequalizers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.double-arrows
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.coforks
+```
+
+</details>
+
+## Idea
+
+Given a [double arrow](foundation.double-arrows.md) `f, g : A → B`, we may ask
+how to construct type families over its
+[coequalizer](synthetic-homotopy-theory.coequalizers.md).
+
+The data required to construct a type family is called
+{{#concept "descent data" Disambiguation="coequalizers" Agda=descent-data-coequalizer}}
+for coequalizers. It consists of a type family `PB : B → 𝒰`, and a family of
+[equivalences](foundation-core.equivalences.md)
+`PA: (a : A) → PB (f a) ≃ PB (g a)`.
+
+The fact that the type of descent data over a double arrow is equivalent to the
+type of type families over its coequalizer is recorded in
+[`descent-property-coequalizers`](synthetic-homotopy-theory.descent-property-coequalizers.md).
+
+The [identity type](foundation-core.identity-types.md) of descent data for
+coequalizers is characterized in
+[`equivalences-descent-data-coequalizers`](synthetic-homotopy-theory.equivalences-descent-data-coequalizers.md).
+
+## Definitions
+
+### Descent data for coequalizers
+
+```agda
+module _
+  {l1 l2 : Level} (F : double-arrow l1 l2)
+  where
+
+  descent-data-coequalizer : (l3 : Level) → UU (l1 ⊔ l2 ⊔ lsuc l3)
+  descent-data-coequalizer l =
+    Σ ( codomain-double-arrow F → UU l)
+      ( λ PB →
+        (a : domain-double-arrow F) →
+        PB (left-map-double-arrow F a) ≃
+        PB (right-map-double-arrow F a))
+```
+
+### Components of descent data for coequalizers
+
+```agda
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  where
+
+  family-descent-data-coequalizer : codomain-double-arrow F → UU l3
+  family-descent-data-coequalizer = pr1 P
+
+  equiv-family-descent-data-coequalizer :
+    (a : domain-double-arrow F) →
+    family-descent-data-coequalizer (left-map-double-arrow F a) ≃
+    family-descent-data-coequalizer (right-map-double-arrow F a)
+  equiv-family-descent-data-coequalizer = pr2 P
+
+  map-family-descent-data-coequalizer :
+    (a : domain-double-arrow F) →
+    family-descent-data-coequalizer (left-map-double-arrow F a) →
+    family-descent-data-coequalizer (right-map-double-arrow F a)
+  map-family-descent-data-coequalizer a =
+    map-equiv (equiv-family-descent-data-coequalizer a)
+
+  is-equiv-map-family-descent-data-coequalizer :
+    (a : domain-double-arrow F) →
+    is-equiv (map-family-descent-data-coequalizer a)
+  is-equiv-map-family-descent-data-coequalizer s =
+    is-equiv-map-equiv (equiv-family-descent-data-coequalizer s)
+```
+
+### Descent data induced by families over coforks
+
+Given a cofork
+
+```text
+     g
+   ----->     e
+ A -----> B -----> X
+     f
+```
+
+and a type family `P : X → 𝒰`, we construct a descent datum: the family
+`PB : B → 𝒰` is obtained by composition `P ∘ e`, and the equivalence
+`PA : (a : A) → P(e(f(a))) ≃ P(e(g(a)))` is obtained by transporting along the
+coherence of the cofork.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} (c : cofork F X)
+  where
+
+  descent-data-family-cofork :
+    {l4 : Level} → (X → UU l4) → descent-data-coequalizer F l4
+  pr1 (descent-data-family-cofork P) =
+    P ∘ map-cofork c
+  pr2 (descent-data-family-cofork P) a =
+    equiv-tr P (coh-cofork c a)
+```
diff --git a/src/synthetic-homotopy-theory/descent-property-coequalizers.lagda.md b/src/synthetic-homotopy-theory/descent-property-coequalizers.lagda.md
new file mode 100644
index 0000000000..e1fb49ccef
--- /dev/null
+++ b/src/synthetic-homotopy-theory/descent-property-coequalizers.lagda.md
@@ -0,0 +1,145 @@
+# Descent property of coequalizers
+
+```agda
+module synthetic-homotopy-theory.descent-property-coequalizers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.commuting-triangles-of-maps
+open import foundation.contractible-maps
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.double-arrows
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.fibers-of-maps
+open import foundation.function-extensionality
+open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.identity-types
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.coforks
+open import synthetic-homotopy-theory.descent-data-coequalizers
+open import synthetic-homotopy-theory.equivalences-descent-data-coequalizers
+open import synthetic-homotopy-theory.universal-property-coequalizers
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "descent property" Disambiguation="coequalizers" Agda=uniqueness-descent-data-coequalizer}}
+of [coequalizers](synthetic-homotopy-theory.coequalizers.md) characterizes type
+families over coequalizers as
+[descent data](synthetic-homotopy-theory.descent-data-coequalizers.md) over the
+base [double arrow](foundation.double-arrows.md).
+
+Given a double arrow `f, g : A → B` and a
+[cofork](synthetic-homotopy-theory.coforks.md) with vertex `X`, there is a
+[commuting triangle](foundation.commuting-triangles-of-maps.md)
+
+```text
+          cofork-map
+  (X → 𝒰) ---------> cofork A 𝒰
+           \       /
+            \     /
+             \   /
+              ∨ ∨
+         descent-data A .
+```
+
+From [univalence](foundation-core.univalence.md) it follows that the right map
+is an equivalence. If `X` is a coequalizer of `f, g`, then we have that the top
+map is an equivalence, which imples that the left map is an equivalence.
+
+## Theorem
+
+```agda
+module _
+  {l1 l2 : Level} {F : double-arrow l1 l2}
+  where
+
+  equiv-descent-data-cofork :
+    {l3 : Level} → cofork F (UU l3) ≃ descent-data-coequalizer F l3
+  equiv-descent-data-cofork =
+    equiv-tot (λ P → equiv-Π-equiv-family (λ a → equiv-univalence))
+
+  descent-data-cofork :
+    {l3 : Level} → cofork F (UU l3) → descent-data-coequalizer F l3
+  descent-data-cofork =
+    map-equiv equiv-descent-data-cofork
+
+  is-equiv-descent-data-cofork :
+    {l3 : Level} → is-equiv (descent-data-cofork {l3})
+  is-equiv-descent-data-cofork =
+    is-equiv-map-equiv equiv-descent-data-cofork
+
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} (c : cofork F X)
+  where
+
+  triangle-descent-data-family-cofork :
+    {l4 : Level} →
+    coherence-triangle-maps
+      ( descent-data-family-cofork c)
+      ( descent-data-cofork)
+      ( cofork-map c {Y = UU l4})
+  triangle-descent-data-family-cofork P =
+    eq-pair-eq-fiber
+      ( eq-htpy (λ a → inv (compute-equiv-eq-ap (coh-cofork c a))))
+
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} {c : cofork F X}
+  (up-c : universal-property-coequalizer c)
+  where
+
+  is-equiv-descent-data-family-cofork :
+    {l4 : Level} →
+    is-equiv (descent-data-family-cofork c {l4})
+  is-equiv-descent-data-family-cofork {l4} =
+    is-equiv-left-map-triangle
+      ( descent-data-family-cofork c)
+      ( descent-data-cofork)
+      ( cofork-map c)
+      ( triangle-descent-data-family-cofork c)
+      ( up-c (UU l4))
+      ( is-equiv-descent-data-cofork)
+
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} {c : cofork F X}
+  (up-c : universal-property-coequalizer c)
+  (P : descent-data-coequalizer F l4)
+  where
+
+  abstract
+    uniqueness-descent-data-coequalizer :
+      is-contr
+        ( Σ ( X → UU l4)
+            ( λ Q →
+              equiv-descent-data-coequalizer
+                ( descent-data-family-cofork c Q)
+                ( P)))
+    uniqueness-descent-data-coequalizer =
+      is-contr-equiv'
+        ( fiber (descent-data-family-cofork c) P)
+        ( equiv-tot
+          ( λ Q →
+            extensionality-descent-data-coequalizer
+              ( descent-data-family-cofork c Q)
+              ( P)))
+        ( is-contr-map-is-equiv
+          ( is-equiv-descent-data-family-cofork up-c)
+          ( P))
+
+  family-cofork-descent-data-coequalizer : X → UU l4
+  family-cofork-descent-data-coequalizer =
+    pr1 (center uniqueness-descent-data-coequalizer)
+```
diff --git a/src/synthetic-homotopy-theory/equivalences-descent-data-coequalizers.lagda.md b/src/synthetic-homotopy-theory/equivalences-descent-data-coequalizers.lagda.md
new file mode 100644
index 0000000000..0c503789a2
--- /dev/null
+++ b/src/synthetic-homotopy-theory/equivalences-descent-data-coequalizers.lagda.md
@@ -0,0 +1,200 @@
+# Equivalences of descent data for coequalizers
+
+```agda
+module synthetic-homotopy-theory.equivalences-descent-data-coequalizers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.double-arrows
+open import foundation.equality-dependent-function-types
+open import foundation.equivalence-extensionality
+open import foundation.equivalences
+open import foundation.families-of-equivalences
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.structure-identity-principle
+open import foundation.torsorial-type-families
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.descent-data-coequalizers
+open import synthetic-homotopy-theory.morphisms-descent-data-coequalizers
+```
+
+</details>
+
+## Idea
+
+## Definitions
+
+### Equivalences of descent data for coequalizers
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  (Q : descent-data-coequalizer F l4)
+  where
+
+  equiv-descent-data-coequalizer : UU (l1 ⊔ l2 ⊔ l3 ⊔ l3 ⊔ l4)
+  equiv-descent-data-coequalizer =
+    Σ ( fam-equiv
+        ( family-descent-data-coequalizer P)
+        ( family-descent-data-coequalizer Q))
+      ( λ e →
+        (a : domain-double-arrow F) →
+        coherence-square-maps
+          ( map-equiv (e (left-map-double-arrow F a)))
+          ( map-family-descent-data-coequalizer P a)
+          ( map-family-descent-data-coequalizer Q a)
+          ( map-equiv (e (right-map-double-arrow F a))))
+
+  module _
+    (e : equiv-descent-data-coequalizer)
+    where
+
+    equiv-equiv-descent-data-coequalizer :
+      (b : codomain-double-arrow F) →
+      family-descent-data-coequalizer P b ≃
+      family-descent-data-coequalizer Q b
+    equiv-equiv-descent-data-coequalizer = pr1 e
+
+    map-equiv-descent-data-coequalizer :
+      (b : codomain-double-arrow F) →
+      family-descent-data-coequalizer P b →
+      family-descent-data-coequalizer Q b
+    map-equiv-descent-data-coequalizer =
+      map-fam-equiv equiv-equiv-descent-data-coequalizer
+
+    is-equiv-map-equiv-descent-data-coequalizer :
+      (b : codomain-double-arrow F) →
+      is-equiv (map-equiv-descent-data-coequalizer b)
+    is-equiv-map-equiv-descent-data-coequalizer =
+      is-equiv-map-fam-equiv equiv-equiv-descent-data-coequalizer
+
+    coherence-equiv-descent-data-coequalizer :
+      (a : domain-double-arrow F) →
+      coherence-square-maps
+        ( map-equiv-descent-data-coequalizer (left-map-double-arrow F a))
+        ( map-family-descent-data-coequalizer P a)
+        ( map-family-descent-data-coequalizer Q a)
+        ( map-equiv-descent-data-coequalizer (right-map-double-arrow F a))
+    coherence-equiv-descent-data-coequalizer = pr2 e
+
+    hom-equiv-descent-data-coequalizer : hom-descent-data-coequalizer P Q
+    pr1 hom-equiv-descent-data-coequalizer =
+      map-equiv-descent-data-coequalizer
+    pr2 hom-equiv-descent-data-coequalizer =
+      coherence-equiv-descent-data-coequalizer
+```
+
+### The identity equivalence of descent data for coequalizers
+
+```agda
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  where
+
+  id-equiv-descent-data-coequalizer : equiv-descent-data-coequalizer P P
+  pr1 id-equiv-descent-data-coequalizer b = id-equiv
+  pr2 id-equiv-descent-data-coequalizer a = refl-htpy
+```
+
+### Inverses of equivalences of descent data for coequalizers
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  {P : descent-data-coequalizer F l3}
+  {Q : descent-data-coequalizer F l4}
+  where
+
+  inv-equiv-descent-data-coequalizer :
+    equiv-descent-data-coequalizer P Q → equiv-descent-data-coequalizer Q P
+  pr1 (inv-equiv-descent-data-coequalizer e) b =
+    inv-equiv (equiv-equiv-descent-data-coequalizer P Q e b)
+  pr2 (inv-equiv-descent-data-coequalizer e) a =
+    horizontal-inv-equiv-coherence-square-maps
+      ( equiv-equiv-descent-data-coequalizer P Q e (left-map-double-arrow F a))
+      ( map-family-descent-data-coequalizer P a)
+      ( map-family-descent-data-coequalizer Q a)
+      ( equiv-equiv-descent-data-coequalizer P Q e (right-map-double-arrow F a))
+      ( coherence-equiv-descent-data-coequalizer P Q e a)
+```
+
+## Properties
+
+### Characterization of identity types of descent data for coequalizers
+
+```agda
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  where
+
+  equiv-eq-descent-data-coequalizer :
+    (Q : descent-data-coequalizer F l3) →
+    P ＝ Q → equiv-descent-data-coequalizer P Q
+  equiv-eq-descent-data-coequalizer .P refl =
+    id-equiv-descent-data-coequalizer P
+
+  abstract
+    is-torsorial-equiv-descent-data-coequalizer :
+      is-torsorial (equiv-descent-data-coequalizer {l4 = l3} P)
+    is-torsorial-equiv-descent-data-coequalizer =
+      is-torsorial-Eq-structure
+        ( is-torsorial-Eq-Π
+          ( λ b → is-torsorial-equiv (family-descent-data-coequalizer P b)))
+        ( family-descent-data-coequalizer P , λ b → id-equiv)
+        ( is-torsorial-Eq-Π
+          ( λ a →
+            is-torsorial-htpy-equiv
+              ( equiv-family-descent-data-coequalizer P a)))
+
+    is-equiv-equiv-eq-descent-data-coequalizer :
+      (Q : descent-data-coequalizer F l3) →
+      is-equiv (equiv-eq-descent-data-coequalizer Q)
+    is-equiv-equiv-eq-descent-data-coequalizer =
+      fundamental-theorem-id
+        ( is-torsorial-equiv-descent-data-coequalizer)
+        ( equiv-eq-descent-data-coequalizer)
+
+  extensionality-descent-data-coequalizer :
+    (Q : descent-data-coequalizer F l3) →
+    (P ＝ Q) ≃ equiv-descent-data-coequalizer P Q
+  pr1 (extensionality-descent-data-coequalizer Q) =
+    equiv-eq-descent-data-coequalizer Q
+  pr2 (extensionality-descent-data-coequalizer Q) =
+    is-equiv-equiv-eq-descent-data-coequalizer Q
+
+  eq-equiv-descent-data-coequalizer :
+    (Q : descent-data-coequalizer F l3) →
+    equiv-descent-data-coequalizer P Q → P ＝ Q
+  eq-equiv-descent-data-coequalizer Q =
+    map-inv-equiv (extensionality-descent-data-coequalizer Q)
+```
+
+### Morphisms of descent data for coequalizers which are equivalences are equivalences
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  {P : descent-data-coequalizer F l3}
+  {Q : descent-data-coequalizer F l4}
+  where
+
+  equiv-hom-descent-data-coequalizer :
+    (h : hom-descent-data-coequalizer P Q) →
+    is-fiberwise-equiv (map-hom-descent-data-coequalizer P Q h) →
+    equiv-descent-data-coequalizer P Q
+  pr1 (equiv-hom-descent-data-coequalizer h is-equiv-map) b =
+    map-hom-descent-data-coequalizer P Q h b , is-equiv-map b
+  pr2 (equiv-hom-descent-data-coequalizer h _) =
+    coherence-hom-descent-data-coequalizer P Q h
+```
diff --git a/src/synthetic-homotopy-theory/morphisms-descent-data-coequalizers.lagda.md b/src/synthetic-homotopy-theory/morphisms-descent-data-coequalizers.lagda.md
new file mode 100644
index 0000000000..737f995e6c
--- /dev/null
+++ b/src/synthetic-homotopy-theory/morphisms-descent-data-coequalizers.lagda.md
@@ -0,0 +1,228 @@
+# Morphisms of descent data for coequalizers
+
+```agda
+module synthetic-homotopy-theory.morphisms-descent-data-coequalizers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.double-arrows
+open import foundation.equality-dependent-function-types
+open import foundation.equivalences
+open import foundation.function-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.structure-identity-principle
+open import foundation.torsorial-type-families
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import synthetic-homotopy-theory.descent-data-coequalizers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "morphism of descent data" Disambiguation="coequalizers" Agda=hom-descent-data-coequalizer}}
+between `(PB, PA)` and `(QB, QA)` is a fiberwise map `h : (b : B) → PB b → QB b`
+equipped with a family of homotopies
+
+```text
+             h (f a)
+   PB (f a) ---------> QB (f a)
+       |                   |
+  PA a |                   | QA a
+       |                   |
+       ∨                   ∨
+   PB (g a) ---------> QB (g a) .
+             h (g a)
+```
+
+## Definitions
+
+### Morphisms of descent data for coequalizers
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  (Q : descent-data-coequalizer F l4)
+  where
+
+  hom-descent-data-coequalizer : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  hom-descent-data-coequalizer =
+    Σ ( (b : codomain-double-arrow F) →
+        family-descent-data-coequalizer P b →
+        family-descent-data-coequalizer Q b)
+      ( λ h →
+        ( a : domain-double-arrow F) →
+        coherence-square-maps
+          ( h (left-map-double-arrow F a))
+          ( map-family-descent-data-coequalizer P a)
+          ( map-family-descent-data-coequalizer Q a)
+          ( h (right-map-double-arrow F a)))
+
+  module _
+    (h : hom-descent-data-coequalizer)
+    where
+
+    map-hom-descent-data-coequalizer :
+      (a : codomain-double-arrow F) →
+      family-descent-data-coequalizer P a →
+      family-descent-data-coequalizer Q a
+    map-hom-descent-data-coequalizer = pr1 h
+
+    coherence-hom-descent-data-coequalizer :
+      (a : domain-double-arrow F) →
+      coherence-square-maps
+        ( map-hom-descent-data-coequalizer (left-map-double-arrow F a))
+        ( map-family-descent-data-coequalizer P a)
+        ( map-family-descent-data-coequalizer Q a)
+        ( map-hom-descent-data-coequalizer (right-map-double-arrow F a))
+    coherence-hom-descent-data-coequalizer = pr2 h
+```
+
+### The identity morphism of descent data for coequalizers
+
+```agda
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  where
+
+  id-hom-descent-data-coequalizer : hom-descent-data-coequalizer P P
+  pr1 id-hom-descent-data-coequalizer a = id
+  pr2 id-hom-descent-data-coequalizer s = refl-htpy
+```
+
+### Composition of morphisms of descent dat afor coequalizers
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  (Q : descent-data-coequalizer F l4)
+  (R : descent-data-coequalizer F l5)
+  (g : hom-descent-data-coequalizer Q R)
+  (f : hom-descent-data-coequalizer P Q)
+  where
+
+  comp-hom-descent-data-coequalizer : hom-descent-data-coequalizer P R
+  pr1 comp-hom-descent-data-coequalizer b =
+    map-hom-descent-data-coequalizer Q R g b ∘
+    map-hom-descent-data-coequalizer P Q f b
+  pr2 comp-hom-descent-data-coequalizer a =
+    pasting-horizontal-coherence-square-maps
+      ( map-hom-descent-data-coequalizer P Q f (left-map-double-arrow F a))
+      ( map-hom-descent-data-coequalizer Q R g (left-map-double-arrow F a))
+      ( map-family-descent-data-coequalizer P a)
+      ( map-family-descent-data-coequalizer Q a)
+      ( map-family-descent-data-coequalizer R a)
+      ( map-hom-descent-data-coequalizer P Q f (right-map-double-arrow F a))
+      ( map-hom-descent-data-coequalizer Q R g (right-map-double-arrow F a))
+      ( coherence-hom-descent-data-coequalizer P Q f a)
+      ( coherence-hom-descent-data-coequalizer Q R g a)
+```
+
+### Homotopies between morphisms of descent data for coequalizers
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  (Q : descent-data-coequalizer F l4)
+  (f g : hom-descent-data-coequalizer P Q)
+  where
+
+  htpy-hom-descent-data-coequalizer : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  htpy-hom-descent-data-coequalizer =
+    Σ ( (b : codomain-double-arrow F) →
+        map-hom-descent-data-coequalizer P Q f b ~
+        map-hom-descent-data-coequalizer P Q g b)
+      ( λ H →
+        (a : domain-double-arrow F) →
+        ( ( coherence-hom-descent-data-coequalizer P Q f a) ∙h
+          ( ( map-family-descent-data-coequalizer Q a) ·l
+            ( H (left-map-double-arrow F a)))) ~
+        ( ( H (right-map-double-arrow F a)) ·r
+          ( map-family-descent-data-coequalizer P a)) ∙h
+        ( coherence-hom-descent-data-coequalizer P Q g a))
+```
+
+### The reflexive homotopy between morphisms of descent data for coequalizers
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  (Q : descent-data-coequalizer F l4)
+  (f : hom-descent-data-coequalizer P Q)
+  where
+
+  refl-htpy-hom-descent-data-coequalizer :
+    htpy-hom-descent-data-coequalizer P Q f f
+  pr1 refl-htpy-hom-descent-data-coequalizer b = refl-htpy
+  pr2 refl-htpy-hom-descent-data-coequalizer a = right-unit-htpy
+```
+
+## Properties
+
+### Characterizing the identity type of morphisms of descent data for coequalizers
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  (Q : descent-data-coequalizer F l4)
+  (f : hom-descent-data-coequalizer P Q)
+  where
+
+  htpy-eq-hom-descent-data-coequalizer :
+    (g : hom-descent-data-coequalizer P Q) →
+    (f ＝ g) → htpy-hom-descent-data-coequalizer P Q f g
+  htpy-eq-hom-descent-data-coequalizer .f refl =
+    refl-htpy-hom-descent-data-coequalizer P Q f
+
+  abstract
+    is-torsorial-htpy-hom-descent-data-coequalizer :
+      is-torsorial (htpy-hom-descent-data-coequalizer P Q f)
+    is-torsorial-htpy-hom-descent-data-coequalizer =
+      is-torsorial-Eq-structure
+        ( is-torsorial-Eq-Π
+          ( λ b →
+            is-torsorial-htpy (map-hom-descent-data-coequalizer P Q f b)))
+        ( map-hom-descent-data-coequalizer P Q f , λ b → refl-htpy)
+        ( is-torsorial-Eq-Π
+          ( λ a →
+            is-torsorial-htpy
+              ( coherence-hom-descent-data-coequalizer P Q f a ∙h refl-htpy)))
+
+  is-equiv-htpy-eq-hom-descent-data-coequalizer :
+    (g : hom-descent-data-coequalizer P Q) →
+    is-equiv (htpy-eq-hom-descent-data-coequalizer g)
+  is-equiv-htpy-eq-hom-descent-data-coequalizer =
+    fundamental-theorem-id
+      ( is-torsorial-htpy-hom-descent-data-coequalizer)
+      ( htpy-eq-hom-descent-data-coequalizer)
+
+  extensionality-hom-descent-data-coequalizer :
+    (g : hom-descent-data-coequalizer P Q) →
+    (f ＝ g) ≃ htpy-hom-descent-data-coequalizer P Q f g
+  pr1 (extensionality-hom-descent-data-coequalizer g) =
+    htpy-eq-hom-descent-data-coequalizer g
+  pr2 (extensionality-hom-descent-data-coequalizer g) =
+    is-equiv-htpy-eq-hom-descent-data-coequalizer g
+
+  eq-htpy-hom-descent-data-coequalizer :
+    (g : hom-descent-data-coequalizer P Q) →
+    htpy-hom-descent-data-coequalizer P Q f g → f ＝ g
+  eq-htpy-hom-descent-data-coequalizer g =
+    map-inv-equiv (extensionality-hom-descent-data-coequalizer g)
+```

From feecee07e109fa09e16af25b3fc13176062c51b8 Mon Sep 17 00:00:00 2001
From: VojtechStep <vojtechstepancik@outlook.com>
Date: Fri, 17 May 2024 16:42:57 +0200
Subject: [PATCH 03/10] Families with descent data for coequalizers

---
 src/synthetic-homotopy-theory.lagda.md        |   1 +
 .../descent-property-coequalizers.lagda.md    |  10 ++
 ...amilies-descent-data-coequalizers.lagda.md | 140 ++++++++++++++++++
 3 files changed, 151 insertions(+)
 create mode 100644 src/synthetic-homotopy-theory/families-descent-data-coequalizers.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index ba1fbc4726..88b491eb97 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -60,6 +60,7 @@ open import synthetic-homotopy-theory.equivalences-coforks-under-equivalences-do
 open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams public
 open import synthetic-homotopy-theory.equivalences-descent-data-coequalizers public
 open import synthetic-homotopy-theory.equivalences-sequential-diagrams public
+open import synthetic-homotopy-theory.families-descent-data-coequalizers public
 open import synthetic-homotopy-theory.families-descent-data-sequential-colimits public
 open import synthetic-homotopy-theory.flattening-lemma-coequalizers public
 open import synthetic-homotopy-theory.flattening-lemma-pushouts public
diff --git a/src/synthetic-homotopy-theory/descent-property-coequalizers.lagda.md b/src/synthetic-homotopy-theory/descent-property-coequalizers.lagda.md
index e1fb49ccef..55353814bd 100644
--- a/src/synthetic-homotopy-theory/descent-property-coequalizers.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-property-coequalizers.lagda.md
@@ -25,6 +25,7 @@ open import foundation.universe-levels
 open import synthetic-homotopy-theory.coforks
 open import synthetic-homotopy-theory.descent-data-coequalizers
 open import synthetic-homotopy-theory.equivalences-descent-data-coequalizers
+open import synthetic-homotopy-theory.families-descent-data-coequalizers
 open import synthetic-homotopy-theory.universal-property-coequalizers
 ```
 
@@ -142,4 +143,13 @@ module _
   family-cofork-descent-data-coequalizer : X → UU l4
   family-cofork-descent-data-coequalizer =
     pr1 (center uniqueness-descent-data-coequalizer)
+
+  family-with-descent-data-coequalizer-descent-data-coequalizer :
+    family-with-descent-data-coequalizer c l4
+  pr1 family-with-descent-data-coequalizer-descent-data-coequalizer =
+    family-cofork-descent-data-coequalizer
+  pr1 (pr2 family-with-descent-data-coequalizer-descent-data-coequalizer) =
+    P
+  pr2 (pr2 family-with-descent-data-coequalizer-descent-data-coequalizer) =
+    pr2 (center uniqueness-descent-data-coequalizer)
 ```
diff --git a/src/synthetic-homotopy-theory/families-descent-data-coequalizers.lagda.md b/src/synthetic-homotopy-theory/families-descent-data-coequalizers.lagda.md
new file mode 100644
index 0000000000..a6d46da339
--- /dev/null
+++ b/src/synthetic-homotopy-theory/families-descent-data-coequalizers.lagda.md
@@ -0,0 +1,140 @@
+# Families with descent data for coequalizers
+
+```agda
+module synthetic-homotopy-theory.families-descent-data-coequalizers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.double-arrows
+open import foundation.equivalences
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.coforks
+open import synthetic-homotopy-theory.descent-data-coequalizers
+open import synthetic-homotopy-theory.equivalences-descent-data-coequalizers
+```
+
+</details>
+
+## Idea
+
+## Definitions
+
+### Type families over a cofork equipped with corresponding descent data for coequalizers
+
+```agda
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} (c : cofork F X)
+  where
+
+  family-with-descent-data-coequalizer :
+    (l4 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4)
+  family-with-descent-data-coequalizer l4 =
+    Σ ( X → UU l4)
+      ( λ P →
+        Σ ( descent-data-coequalizer F l4)
+          ( λ Q →
+            equiv-descent-data-coequalizer
+              ( descent-data-family-cofork c P)
+              ( Q)))
+```
+
+### Components of a type family with corresponding descent data
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} {c : cofork F X}
+  (P : family-with-descent-data-coequalizer c l4)
+  where
+
+  family-cofork-family-with-descent-data-coequalizer : X → UU l4
+  family-cofork-family-with-descent-data-coequalizer = pr1 P
+
+  descent-data-family-with-descent-data-coequalizer :
+    descent-data-coequalizer F l4
+  descent-data-family-with-descent-data-coequalizer = pr1 (pr2 P)
+
+  family-family-with-descent-data-coequalizer :
+    codomain-double-arrow F → UU l4
+  family-family-with-descent-data-coequalizer =
+    family-descent-data-coequalizer
+      ( descent-data-family-with-descent-data-coequalizer)
+
+  equiv-family-family-with-descent-data-coequalizer :
+    (a : domain-double-arrow F) →
+    family-family-with-descent-data-coequalizer (left-map-double-arrow F a) ≃
+    family-family-with-descent-data-coequalizer (right-map-double-arrow F a)
+  equiv-family-family-with-descent-data-coequalizer =
+    equiv-family-descent-data-coequalizer
+      ( descent-data-family-with-descent-data-coequalizer)
+
+  map-family-family-with-descent-data-coequalizer :
+    (a : domain-double-arrow F) →
+    family-family-with-descent-data-coequalizer (left-map-double-arrow F a) →
+    family-family-with-descent-data-coequalizer (right-map-double-arrow F a)
+  map-family-family-with-descent-data-coequalizer =
+    map-family-descent-data-coequalizer
+      ( descent-data-family-with-descent-data-coequalizer)
+
+  equiv-descent-data-family-with-descent-data-coequalizer :
+    equiv-descent-data-coequalizer
+      ( descent-data-family-cofork c
+        ( family-cofork-family-with-descent-data-coequalizer))
+      ( descent-data-family-with-descent-data-coequalizer)
+  equiv-descent-data-family-with-descent-data-coequalizer = pr2 (pr2 P)
+
+  equiv-family-with-descent-data-coequalizer :
+    (a : codomain-double-arrow F) →
+    family-cofork-family-with-descent-data-coequalizer (map-cofork c a) ≃
+    family-family-with-descent-data-coequalizer a
+  equiv-family-with-descent-data-coequalizer =
+    equiv-equiv-descent-data-coequalizer
+      ( descent-data-family-cofork c
+        ( family-cofork-family-with-descent-data-coequalizer))
+      ( descent-data-family-with-descent-data-coequalizer)
+      ( equiv-descent-data-family-with-descent-data-coequalizer)
+
+  map-family-with-descent-data-coequalizer :
+    (a : codomain-double-arrow F) →
+    family-cofork-family-with-descent-data-coequalizer (map-cofork c a) →
+    family-family-with-descent-data-coequalizer a
+  map-family-with-descent-data-coequalizer =
+    map-equiv-descent-data-coequalizer
+      ( descent-data-family-cofork c
+        ( family-cofork-family-with-descent-data-coequalizer))
+      ( descent-data-family-with-descent-data-coequalizer)
+      ( equiv-descent-data-family-with-descent-data-coequalizer)
+
+  is-equiv-map-family-with-descent-data-coequalizer :
+    (a : codomain-double-arrow F) →
+    is-equiv (map-family-with-descent-data-coequalizer a)
+  is-equiv-map-family-with-descent-data-coequalizer =
+    is-equiv-map-equiv-descent-data-coequalizer
+      ( descent-data-family-cofork c
+        ( family-cofork-family-with-descent-data-coequalizer))
+      ( descent-data-family-with-descent-data-coequalizer)
+      ( equiv-descent-data-family-with-descent-data-coequalizer)
+
+  coherence-family-with-descent-data-coequalizer :
+    (a : domain-double-arrow F) →
+    coherence-square-maps
+      ( map-family-with-descent-data-coequalizer (left-map-double-arrow F a))
+      ( tr
+        ( family-cofork-family-with-descent-data-coequalizer)
+        ( coh-cofork c a))
+      ( map-family-family-with-descent-data-coequalizer a)
+      ( map-family-with-descent-data-coequalizer (right-map-double-arrow F a))
+  coherence-family-with-descent-data-coequalizer =
+    coherence-equiv-descent-data-coequalizer
+      ( descent-data-family-cofork c
+        ( family-cofork-family-with-descent-data-coequalizer))
+      ( descent-data-family-with-descent-data-coequalizer)
+      ( equiv-descent-data-family-with-descent-data-coequalizer)
+```

From cbd46b29adcfac18821ea3c2a9605fddd29091bc Mon Sep 17 00:00:00 2001
From: VojtechStep <vojtechstepancik@outlook.com>
Date: Fri, 17 May 2024 17:09:10 +0200
Subject: [PATCH 04/10] Descent data for families of functions over
 coequalizers

---
 src/synthetic-homotopy-theory.lagda.md        |   1 +
 ...ta-coequalizers-function-families.lagda.md | 124 ++++++++++++++++++
 2 files changed, 125 insertions(+)
 create mode 100644 src/synthetic-homotopy-theory/descent-data-coequalizers-function-families.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 88b491eb97..a87cd8001a 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -49,6 +49,7 @@ open import synthetic-homotopy-theory.descent-circle-equivalence-types public
 open import synthetic-homotopy-theory.descent-circle-function-types public
 open import synthetic-homotopy-theory.descent-circle-subtypes public
 open import synthetic-homotopy-theory.descent-data-coequalizers public
+open import synthetic-homotopy-theory.descent-data-coequalizers-function-families public
 open import synthetic-homotopy-theory.descent-data-sequential-colimits public
 open import synthetic-homotopy-theory.descent-property-coequalizers public
 open import synthetic-homotopy-theory.descent-property-sequential-colimits public
diff --git a/src/synthetic-homotopy-theory/descent-data-coequalizers-function-families.lagda.md b/src/synthetic-homotopy-theory/descent-data-coequalizers-function-families.lagda.md
new file mode 100644
index 0000000000..1f85e804c2
--- /dev/null
+++ b/src/synthetic-homotopy-theory/descent-data-coequalizers-function-families.lagda.md
@@ -0,0 +1,124 @@
+# Descent data for families of functions over coequalizers
+
+```agda
+module synthetic-homotopy-theory.descent-data-coequalizers-function-families 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.double-arrows
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.homotopy-algebra
+open import foundation.identity-types
+open import foundation.postcomposition-functions
+open import foundation.transport-along-identifications
+open import foundation.universal-property-equivalences
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import synthetic-homotopy-theory.coforks
+open import synthetic-homotopy-theory.descent-data-coequalizers
+open import synthetic-homotopy-theory.equivalences-descent-data-coequalizers
+open import synthetic-homotopy-theory.families-descent-data-coequalizers
+```
+
+</details>
+
+## Idea
+
+## Definitions
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} {c : cofork F X}
+  (P : family-with-descent-data-coequalizer c l4)
+  (Q : family-with-descent-data-coequalizer c l5)
+  where
+
+  family-cofork-family-with-descent-data-coequalizer-function-family :
+    X → UU (l4 ⊔ l5)
+  family-cofork-family-with-descent-data-coequalizer-function-family x =
+    family-cofork-family-with-descent-data-coequalizer P x →
+    family-cofork-family-with-descent-data-coequalizer Q x
+
+  descent-data-coequalizer-function-family :
+    descent-data-coequalizer F (l4 ⊔ l5)
+  pr1 descent-data-coequalizer-function-family b =
+    family-family-with-descent-data-coequalizer P b →
+    family-family-with-descent-data-coequalizer Q b
+  pr2 descent-data-coequalizer-function-family a =
+    ( equiv-postcomp
+      ( family-family-with-descent-data-coequalizer P
+        ( right-map-double-arrow F a))
+      ( equiv-family-family-with-descent-data-coequalizer Q a)) ∘e
+    ( equiv-precomp
+      ( inv-equiv (equiv-family-family-with-descent-data-coequalizer P a))
+      ( family-family-with-descent-data-coequalizer Q
+        ( left-map-double-arrow F a)))
+
+  equiv-equiv-descent-data-coequalizer-function-family :
+    (b : codomain-double-arrow F) →
+    ( family-cofork-family-with-descent-data-coequalizer P (map-cofork c b) →
+      family-cofork-family-with-descent-data-coequalizer Q (map-cofork c b)) ≃
+    ( family-family-with-descent-data-coequalizer P b →
+      family-family-with-descent-data-coequalizer Q b)
+  equiv-equiv-descent-data-coequalizer-function-family b =
+    ( equiv-postcomp
+      ( family-family-with-descent-data-coequalizer P b)
+      ( equiv-family-with-descent-data-coequalizer Q b)) ∘e
+    ( equiv-precomp
+      ( inv-equiv (equiv-family-with-descent-data-coequalizer P b))
+      ( family-cofork-family-with-descent-data-coequalizer Q (map-cofork c b)))
+
+  equiv-descent-data-coequalizer-function-family :
+    equiv-descent-data-coequalizer
+      ( descent-data-family-cofork c
+        ( family-cofork-family-with-descent-data-coequalizer-function-family))
+      ( descent-data-coequalizer-function-family)
+  pr1 equiv-descent-data-coequalizer-function-family =
+    equiv-equiv-descent-data-coequalizer-function-family
+  pr2 equiv-descent-data-coequalizer-function-family a f =
+    ( ap
+      ( λ g →
+        ( map-family-with-descent-data-coequalizer Q
+          ( right-map-double-arrow F a)) ∘
+        ( g) ∘
+        ( map-inv-equiv
+          ( equiv-family-with-descent-data-coequalizer P
+            ( right-map-double-arrow F a))))
+      ( tr-function-type
+        ( family-cofork-family-with-descent-data-coequalizer P)
+        ( family-cofork-family-with-descent-data-coequalizer Q)
+        ( coh-cofork c a)
+        ( f))) ∙
+    ( eq-htpy
+      ( horizontal-concat-htpy
+        ( coherence-family-with-descent-data-coequalizer Q a ·r f)
+        ( coherence-square-maps-inv-equiv
+          ( equiv-tr
+            ( family-cofork-family-with-descent-data-coequalizer P)
+            ( coh-cofork c a))
+          ( equiv-family-with-descent-data-coequalizer P
+            ( left-map-double-arrow F a))
+          ( equiv-family-with-descent-data-coequalizer P
+            ( right-map-double-arrow F a))
+          ( equiv-family-family-with-descent-data-coequalizer P a)
+          ( inv-htpy (coherence-family-with-descent-data-coequalizer P a)))))
+
+  family-with-descent-data-coequalizer-function-family :
+    family-with-descent-data-coequalizer c (l4 ⊔ l5)
+  pr1 family-with-descent-data-coequalizer-function-family =
+    family-cofork-family-with-descent-data-coequalizer-function-family
+  pr1 (pr2 family-with-descent-data-coequalizer-function-family) =
+    descent-data-coequalizer-function-family
+  pr2 (pr2 family-with-descent-data-coequalizer-function-family) =
+    equiv-descent-data-coequalizer-function-family
+```

From db9b2fdbffce9c5fada118adfdab9fb5c958ecd4 Mon Sep 17 00:00:00 2001
From: VojtechStep <vojtechstepancik@outlook.com>
Date: Fri, 17 May 2024 17:56:07 +0200
Subject: [PATCH 05/10] Sections of descent data for coequalizers

---
 src/synthetic-homotopy-theory.lagda.md        |   1 +
 ...ections-descent-data-coequalizers.lagda.md | 127 ++++++++++++++++++
 2 files changed, 128 insertions(+)
 create mode 100644 src/synthetic-homotopy-theory/sections-descent-data-coequalizers.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index a87cd8001a..f97f8476e1 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -104,6 +104,7 @@ open import synthetic-homotopy-theory.recursion-principle-pushouts public
 open import synthetic-homotopy-theory.retracts-of-sequential-diagrams public
 open import synthetic-homotopy-theory.rewriting-pushouts public
 open import synthetic-homotopy-theory.sections-descent-circle public
+open import synthetic-homotopy-theory.sections-descent-data-coequalizers public
 open import synthetic-homotopy-theory.sequential-colimits public
 open import synthetic-homotopy-theory.sequential-diagrams public
 open import synthetic-homotopy-theory.sequentially-compact-types public
diff --git a/src/synthetic-homotopy-theory/sections-descent-data-coequalizers.lagda.md b/src/synthetic-homotopy-theory/sections-descent-data-coequalizers.lagda.md
new file mode 100644
index 0000000000..cd83f5188d
--- /dev/null
+++ b/src/synthetic-homotopy-theory/sections-descent-data-coequalizers.lagda.md
@@ -0,0 +1,127 @@
+# Sections of descent data for coequalizers
+
+```agda
+module synthetic-homotopy-theory.sections-descent-data-coequalizers 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-triangles-of-maps
+open import foundation.dependent-pair-types
+open import foundation.double-arrows
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.coforks
+open import synthetic-homotopy-theory.dependent-coforks
+open import synthetic-homotopy-theory.dependent-universal-property-coequalizers
+open import synthetic-homotopy-theory.descent-data-coequalizers
+open import synthetic-homotopy-theory.families-descent-data-coequalizers
+open import synthetic-homotopy-theory.universal-property-coequalizers
+```
+
+</details>
+
+## Idea
+
+## Definitions
+
+```agda
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  where
+
+  section-descent-data-coequalizer : UU (l1 ⊔ l2 ⊔ l3)
+  section-descent-data-coequalizer =
+    Σ ( (b : codomain-double-arrow F) → family-descent-data-coequalizer P b)
+      ( λ s →
+        (a : domain-double-arrow F) →
+        map-family-descent-data-coequalizer P a
+          ( s (left-map-double-arrow F a)) ＝
+        s (right-map-double-arrow F a))
+```
+
+## Properties
+
+### Sections of families over a coequalizer correspond to sections of the corresponding descent data
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} {c : cofork F X}
+  (P : family-with-descent-data-coequalizer c l4)
+  where
+
+  section-descent-data-section-family-cofork :
+    ((x : X) → family-cofork-family-with-descent-data-coequalizer P x) →
+    section-descent-data-coequalizer
+      ( descent-data-family-with-descent-data-coequalizer P)
+  pr1 (section-descent-data-section-family-cofork f) b =
+    map-family-with-descent-data-coequalizer P b (f (map-cofork c b))
+  pr2 (section-descent-data-section-family-cofork f) a =
+    ( inv
+      ( coherence-family-with-descent-data-coequalizer P a
+        ( f (map-cofork c (left-map-double-arrow F a))))) ∙
+    ( ap
+      ( map-family-with-descent-data-coequalizer P (right-map-double-arrow F a))
+      ( apd f (coh-cofork c a)))
+
+  equiv-section-descent-data-dependent-cofork :
+    dependent-cofork c
+      ( family-cofork-family-with-descent-data-coequalizer P) ≃
+    section-descent-data-coequalizer
+      ( descent-data-family-with-descent-data-coequalizer P)
+  equiv-section-descent-data-dependent-cofork =
+    equiv-Σ _
+      ( equiv-Π-equiv-family (equiv-family-with-descent-data-coequalizer P))
+      ( λ s →
+        equiv-Π-equiv-family
+          ( λ a →
+            ( equiv-inv-concat
+              ( coherence-family-with-descent-data-coequalizer P a
+                ( s (left-map-double-arrow F a)))
+              ( _)) ∘e
+            ( equiv-ap-emb
+              ( emb-equiv
+                ( equiv-family-with-descent-data-coequalizer P
+                  ( right-map-double-arrow F a))))))
+
+  triangle-section-descent-data-dependent-cofork :
+    coherence-triangle-maps
+      ( section-descent-data-section-family-cofork)
+      ( map-equiv equiv-section-descent-data-dependent-cofork)
+      ( dependent-cofork-map c)
+  triangle-section-descent-data-dependent-cofork = refl-htpy
+
+  is-equiv-section-descent-data-section-family-cofork :
+    universal-property-coequalizer c →
+    is-equiv (section-descent-data-section-family-cofork)
+  is-equiv-section-descent-data-section-family-cofork up-c =
+    is-equiv-left-map-triangle
+      ( section-descent-data-section-family-cofork)
+      ( map-equiv equiv-section-descent-data-dependent-cofork)
+      ( dependent-cofork-map c)
+      ( triangle-section-descent-data-dependent-cofork)
+      ( dependent-universal-property-universal-property-coequalizer up-c
+        ( family-cofork-family-with-descent-data-coequalizer P))
+      ( is-equiv-map-equiv equiv-section-descent-data-dependent-cofork)
+
+  compute-section-family-cofork :
+    universal-property-coequalizer c →
+    ((x : X) → family-cofork-family-with-descent-data-coequalizer P x) ≃
+    section-descent-data-coequalizer
+      ( descent-data-family-with-descent-data-coequalizer P)
+  pr1 (compute-section-family-cofork _) =
+    section-descent-data-section-family-cofork
+  pr2 (compute-section-family-cofork up-c) =
+    is-equiv-section-descent-data-section-family-cofork up-c
+```

From 67ddf95767bac8363f12beb7305ff5ba7b00f0e7 Mon Sep 17 00:00:00 2001
From: VojtechStep <vojtechstepancik@outlook.com>
Date: Fri, 17 May 2024 17:56:22 +0200
Subject: [PATCH 06/10] Characterize sections of function types over
 coequalizers

---
 .../commuting-triangles-of-maps.lagda.md      | 20 ++++++++++------
 ...ta-coequalizers-function-families.lagda.md | 24 +++++++++++++++++++
 2 files changed, 37 insertions(+), 7 deletions(-)

diff --git a/src/foundation/commuting-triangles-of-maps.lagda.md b/src/foundation/commuting-triangles-of-maps.lagda.md
index 55d8859dee..02cec10c81 100644
--- a/src/foundation/commuting-triangles-of-maps.lagda.md
+++ b/src/foundation/commuting-triangles-of-maps.lagda.md
@@ -55,6 +55,18 @@ module _
   (left : A → X) (right : B → X) (e : A ≃ B)
   where
 
+  equiv-coherence-triangle-maps-inv-top' :
+    coherence-triangle-maps left right (map-equiv e) ≃
+    coherence-triangle-maps' right left (map-inv-equiv e)
+  equiv-coherence-triangle-maps-inv-top' =
+    equiv-Π
+      ( λ b → left (map-inv-equiv e b) ＝ right b)
+      ( e)
+      ( λ a →
+        equiv-concat
+          ( ap left (is-retraction-map-inv-equiv e a))
+          ( right (map-equiv e a)))
+
   equiv-coherence-triangle-maps-inv-top :
     coherence-triangle-maps left right (map-equiv e) ≃
     coherence-triangle-maps right left (map-inv-equiv e)
@@ -62,13 +74,7 @@ module _
     ( equiv-inv-htpy
       ( left ∘ (map-inv-equiv e))
       ( right)) ∘e
-    ( equiv-Π
-      ( λ b → left (map-inv-equiv e b) ＝ right b)
-      ( e)
-      ( λ a →
-        equiv-concat
-          ( ap left (is-retraction-map-inv-equiv e a))
-          ( right (map-equiv e a))))
+    ( equiv-coherence-triangle-maps-inv-top')
 
   coherence-triangle-maps-inv-top :
     coherence-triangle-maps left right (map-equiv e) →
diff --git a/src/synthetic-homotopy-theory/descent-data-coequalizers-function-families.lagda.md b/src/synthetic-homotopy-theory/descent-data-coequalizers-function-families.lagda.md
index 1f85e804c2..a3151d46fe 100644
--- a/src/synthetic-homotopy-theory/descent-data-coequalizers-function-families.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-data-coequalizers-function-families.lagda.md
@@ -9,11 +9,14 @@ module synthetic-homotopy-theory.descent-data-coequalizers-function-families whe
 ```agda
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-squares-of-maps
+open import foundation.commuting-triangles-of-maps
 open import foundation.dependent-pair-types
 open import foundation.double-arrows
 open import foundation.equivalences
 open import foundation.function-extensionality
 open import foundation.function-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
 open import foundation.homotopy-algebra
 open import foundation.identity-types
@@ -27,6 +30,8 @@ open import synthetic-homotopy-theory.coforks
 open import synthetic-homotopy-theory.descent-data-coequalizers
 open import synthetic-homotopy-theory.equivalences-descent-data-coequalizers
 open import synthetic-homotopy-theory.families-descent-data-coequalizers
+open import synthetic-homotopy-theory.morphisms-descent-data-coequalizers
+open import synthetic-homotopy-theory.sections-descent-data-coequalizers
 ```
 
 </details>
@@ -121,4 +126,23 @@ module _
     descent-data-coequalizer-function-family
   pr2 (pr2 family-with-descent-data-coequalizer-function-family) =
     equiv-descent-data-coequalizer-function-family
+
+  compute-section-family-cofork-function-family :
+    section-descent-data-coequalizer descent-data-coequalizer-function-family ≃
+    hom-descent-data-coequalizer
+      ( descent-data-family-with-descent-data-coequalizer P)
+      ( descent-data-family-with-descent-data-coequalizer Q)
+  compute-section-family-cofork-function-family =
+    equiv-tot
+      ( λ h →
+        equiv-Π-equiv-family
+          ( λ a →
+            ( equiv-inv-htpy _ _) ∘e
+            ( inv-equiv
+              ( equiv-coherence-triangle-maps-inv-top'
+                ( ( map-family-family-with-descent-data-coequalizer Q a) ∘
+                  ( h (left-map-double-arrow F a)))
+                ( h (right-map-double-arrow F a))
+                ( equiv-family-family-with-descent-data-coequalizer P a))) ∘e
+            ( equiv-funext)))
 ```

From ea3636fd209c1f8fdc37aab910f9d728c0eed1b3 Mon Sep 17 00:00:00 2001
From: VojtechStep <vojtechstepancik@outlook.com>
Date: Sat, 18 May 2024 13:11:18 +0200
Subject: [PATCH 07/10] Transport in a family of equivalence types

---
 src/foundation/equivalences.lagda.md | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md
index 0a3a32779f..d4a268f785 100644
--- a/src/foundation/equivalences.lagda.md
+++ b/src/foundation/equivalences.lagda.md
@@ -16,6 +16,7 @@ open import foundation.equivalence-extensionality
 open import foundation.function-extensionality
 open import foundation.functoriality-fibers-of-maps
 open import foundation.logical-equivalences
+open import foundation.transport-along-identifications
 open import foundation.transposition-identifications-along-equivalences
 open import foundation.truncated-maps
 open import foundation.universal-property-equivalences
@@ -572,6 +573,19 @@ pr1 (equiv-precomp-equiv e C) = _∘e e
 pr2 (equiv-precomp-equiv e C) = is-equiv-precomp-equiv-equiv e
 ```
 
+### Computing transport in a family of equivalence types
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
+  where
+
+  tr-equiv-type :
+    {x y : A} (p : x ＝ y) (e : B x ≃ C x) →
+    tr (λ x → B x ≃ C x) p e ＝ equiv-tr C p ∘e e ∘e equiv-tr B (inv p)
+  tr-equiv-type refl e = eq-htpy-equiv refl-htpy
+```
+
 ### A cospan in which one of the legs is an equivalence is a pullback if and only if the corresponding map on the cone is an equivalence
 
 ```agda

From 4aa1d2f58653d848d43f4b72b0a713218f405f2d Mon Sep 17 00:00:00 2001
From: VojtechStep <vojtechstepancik@outlook.com>
Date: Sat, 18 May 2024 13:33:53 +0200
Subject: [PATCH 08/10] Descent data for families of functions over
 coequalizers

---
 src/synthetic-homotopy-theory.lagda.md        |   1 +
 ...coequalizers-equivalence-families.lagda.md | 147 ++++++++++++++++++
 2 files changed, 148 insertions(+)
 create mode 100644 src/synthetic-homotopy-theory/descent-data-coequalizers-equivalence-families.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index f97f8476e1..beb0fd0ca1 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -49,6 +49,7 @@ open import synthetic-homotopy-theory.descent-circle-equivalence-types public
 open import synthetic-homotopy-theory.descent-circle-function-types public
 open import synthetic-homotopy-theory.descent-circle-subtypes public
 open import synthetic-homotopy-theory.descent-data-coequalizers public
+open import synthetic-homotopy-theory.descent-data-coequalizers-equivalence-families public
 open import synthetic-homotopy-theory.descent-data-coequalizers-function-families public
 open import synthetic-homotopy-theory.descent-data-sequential-colimits public
 open import synthetic-homotopy-theory.descent-property-coequalizers public
diff --git a/src/synthetic-homotopy-theory/descent-data-coequalizers-equivalence-families.lagda.md b/src/synthetic-homotopy-theory/descent-data-coequalizers-equivalence-families.lagda.md
new file mode 100644
index 0000000000..bb6eb44d20
--- /dev/null
+++ b/src/synthetic-homotopy-theory/descent-data-coequalizers-equivalence-families.lagda.md
@@ -0,0 +1,147 @@
+# Descent data for families of equivalences over coequalizers
+
+```agda
+module synthetic-homotopy-theory.descent-data-coequalizers-equivalence-families where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-maps
+open import foundation.commuting-triangles-of-maps
+open import foundation.dependent-pair-types
+open import foundation.double-arrows
+open import foundation.equivalence-extensionality
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.homotopy-algebra
+open import foundation.identity-types
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import synthetic-homotopy-theory.coforks
+open import synthetic-homotopy-theory.descent-data-coequalizers
+open import synthetic-homotopy-theory.equivalences-descent-data-coequalizers
+open import synthetic-homotopy-theory.families-descent-data-coequalizers
+open import synthetic-homotopy-theory.sections-descent-data-coequalizers
+```
+
+</details>
+
+## Idea
+
+## Definitions
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} {c : cofork F X}
+  (P : family-with-descent-data-coequalizer c l4)
+  (Q : family-with-descent-data-coequalizer c l5)
+  where
+
+  family-cofork-family-with-descent-data-coequalizer-equivalence-family :
+    X → UU (l4 ⊔ l5)
+  family-cofork-family-with-descent-data-coequalizer-equivalence-family x =
+    family-cofork-family-with-descent-data-coequalizer P x ≃
+    family-cofork-family-with-descent-data-coequalizer Q x
+
+  descent-data-coequalizer-equivalence-family :
+    descent-data-coequalizer F (l4 ⊔ l5)
+  pr1 descent-data-coequalizer-equivalence-family b =
+    family-family-with-descent-data-coequalizer P b ≃
+    family-family-with-descent-data-coequalizer Q b
+  pr2 descent-data-coequalizer-equivalence-family a =
+    ( equiv-postcomp-equiv
+      ( equiv-family-family-with-descent-data-coequalizer Q a)
+      ( family-family-with-descent-data-coequalizer P
+        ( right-map-double-arrow F a))) ∘e
+    ( equiv-precomp-equiv
+      ( inv-equiv (equiv-family-family-with-descent-data-coequalizer P a))
+      ( family-family-with-descent-data-coequalizer Q
+        ( left-map-double-arrow F a)))
+
+  equiv-equiv-descent-data-coequalizer-equivalence-family :
+    (b : codomain-double-arrow F) →
+    ( family-cofork-family-with-descent-data-coequalizer P (map-cofork c b) ≃
+      family-cofork-family-with-descent-data-coequalizer Q (map-cofork c b)) ≃
+    ( family-family-with-descent-data-coequalizer P b ≃
+      family-family-with-descent-data-coequalizer Q b)
+  equiv-equiv-descent-data-coequalizer-equivalence-family b =
+    ( equiv-postcomp-equiv
+      ( equiv-family-with-descent-data-coequalizer Q b)
+      ( family-family-with-descent-data-coequalizer P b)) ∘e
+    ( equiv-precomp-equiv
+      ( inv-equiv (equiv-family-with-descent-data-coequalizer P b))
+      ( family-cofork-family-with-descent-data-coequalizer Q (map-cofork c b)))
+
+  equiv-descent-data-coequalizer-equivalence-family :
+    equiv-descent-data-coequalizer
+      ( descent-data-family-cofork c
+        ( family-cofork-family-with-descent-data-coequalizer-equivalence-family))
+      ( descent-data-coequalizer-equivalence-family)
+  pr1 equiv-descent-data-coequalizer-equivalence-family =
+    equiv-equiv-descent-data-coequalizer-equivalence-family
+  pr2 equiv-descent-data-coequalizer-equivalence-family a e =
+    ( ap
+      ( λ f →
+        ( equiv-family-with-descent-data-coequalizer Q
+          ( right-map-double-arrow F a)) ∘e
+        ( f) ∘e
+        ( inv-equiv
+          ( equiv-family-with-descent-data-coequalizer P
+            ( right-map-double-arrow F a))))
+      ( tr-equiv-type
+        ( family-cofork-family-with-descent-data-coequalizer P)
+        ( family-cofork-family-with-descent-data-coequalizer Q)
+        ( coh-cofork c a)
+        ( e))) ∙
+    ( eq-htpy-equiv
+      ( horizontal-concat-htpy
+        ( coherence-family-with-descent-data-coequalizer Q a ·r map-equiv e)
+        ( coherence-square-maps-inv-equiv
+          ( equiv-tr
+            ( family-cofork-family-with-descent-data-coequalizer P)
+            ( coh-cofork c a))
+          ( equiv-family-with-descent-data-coequalizer P
+            ( left-map-double-arrow F a))
+          ( equiv-family-with-descent-data-coequalizer P
+            ( right-map-double-arrow F a))
+          ( equiv-family-family-with-descent-data-coequalizer P a)
+          ( inv-htpy (coherence-family-with-descent-data-coequalizer P a)))))
+
+  family-with-descent-data-coequalizer-equivalence-family :
+    family-with-descent-data-coequalizer c (l4 ⊔ l5)
+  pr1 family-with-descent-data-coequalizer-equivalence-family =
+    family-cofork-family-with-descent-data-coequalizer-equivalence-family
+  pr1 (pr2 family-with-descent-data-coequalizer-equivalence-family) =
+    descent-data-coequalizer-equivalence-family
+  pr2 (pr2 family-with-descent-data-coequalizer-equivalence-family) =
+    equiv-descent-data-coequalizer-equivalence-family
+
+  compute-section-family-cofork-equivalence-family :
+    section-descent-data-coequalizer
+      ( descent-data-coequalizer-equivalence-family) ≃
+    equiv-descent-data-coequalizer
+      ( descent-data-family-with-descent-data-coequalizer P)
+      ( descent-data-family-with-descent-data-coequalizer Q)
+  compute-section-family-cofork-equivalence-family =
+    equiv-tot
+      ( λ e →
+        equiv-Π-equiv-family
+          ( λ a →
+            ( equiv-inv-htpy _ _) ∘e
+            ( inv-equiv
+              ( equiv-coherence-triangle-maps-inv-top'
+                ( ( map-family-family-with-descent-data-coequalizer Q a) ∘
+                  ( map-equiv (e (left-map-double-arrow F a))))
+                ( map-equiv (e (right-map-double-arrow F a)))
+                ( equiv-family-family-with-descent-data-coequalizer P a))) ∘e
+            ( extensionality-equiv _ _)))
+```

From 37d1cd6afec1dedb2d994125868fb346499a28a1 Mon Sep 17 00:00:00 2001
From: VojtechStep <vojtechstepancik@outlook.com>
Date: Sat, 18 May 2024 16:03:58 +0200
Subject: [PATCH 09/10] Flattening of coequalizers with descent data

---
 .../flattening-lemma-coequalizers.lagda.md    | 175 ++++++++++++++++++
 1 file changed, 175 insertions(+)

diff --git a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
index b04f7516c4..924621232f 100644
--- a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
+++ b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md
@@ -1,6 +1,7 @@
 # The flattening lemma for coequalizers
 
 ```agda
+{-# OPTIONS --lossy-unification #-}
 module synthetic-homotopy-theory.flattening-lemma-coequalizers where
 ```
 
@@ -8,10 +9,13 @@ module synthetic-homotopy-theory.flattening-lemma-coequalizers where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.commuting-triangles-of-identifications
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.double-arrows
+open import foundation.equality-dependent-pair-types
 open import foundation.equivalences
+open import foundation.equivalences-double-arrows
 open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
@@ -19,9 +23,14 @@ open import foundation.identity-types
 open import foundation.transport-along-identifications
 open import foundation.type-arithmetic-coproduct-types
 open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+open import foundation.whiskering-identifications-concatenation
 
 open import synthetic-homotopy-theory.coforks
 open import synthetic-homotopy-theory.dependent-universal-property-coequalizers
+open import synthetic-homotopy-theory.descent-data-coequalizers
+open import synthetic-homotopy-theory.equivalences-coforks-under-equivalences-double-arrows
+open import synthetic-homotopy-theory.equivalences-descent-data-coequalizers
 open import synthetic-homotopy-theory.flattening-lemma-pushouts
 open import synthetic-homotopy-theory.universal-property-coequalizers
 open import synthetic-homotopy-theory.universal-property-pushouts
@@ -105,6 +114,65 @@ module _
     universal-property-coequalizer (cofork-flattening-lemma-coequalizer)
 ```
 
+### The statement of the flattening lemma for coequalizers, phrased using descent data
+
+The above statement of the flattening lemma works with a provided type family
+over the coequalizer. We can instead accept a definition of this family via
+descent data.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  where
+
+  double-arrow-flattening-lemma-descent-data-coequalizer :
+    double-arrow (l1 ⊔ l3) (l2 ⊔ l3)
+  double-arrow-flattening-lemma-descent-data-coequalizer =
+    make-double-arrow
+      ( map-Σ-map-base
+        ( left-map-double-arrow F)
+        ( family-descent-data-coequalizer P))
+      ( map-Σ
+        ( family-descent-data-coequalizer P)
+        ( right-map-double-arrow F)
+        ( map-family-descent-data-coequalizer P))
+
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} (c : cofork F X)
+  (P : descent-data-coequalizer F l4)
+  (Q : X → UU l4)
+  (e : equiv-descent-data-coequalizer P (descent-data-family-cofork c Q))
+  where
+
+  cofork-flattening-lemma-descent-coequalizer :
+    cofork
+      ( double-arrow-flattening-lemma-descent-data-coequalizer P)
+      ( Σ X Q)
+  pr1 cofork-flattening-lemma-descent-coequalizer =
+    map-Σ Q
+      ( map-cofork c)
+      ( map-equiv-descent-data-coequalizer P (descent-data-family-cofork c Q) e)
+  pr2 cofork-flattening-lemma-descent-coequalizer =
+    coherence-square-maps-Σ Q
+      ( map-family-descent-data-coequalizer P)
+      ( λ a → id)
+      ( map-equiv-descent-data-coequalizer P (descent-data-family-cofork c Q) e)
+      ( map-equiv-descent-data-coequalizer P (descent-data-family-cofork c Q) e)
+      ( λ a →
+        inv-htpy
+          ( coherence-equiv-descent-data-coequalizer P
+            ( descent-data-family-cofork c Q)
+            ( e)
+            ( a)))
+
+  flattening-lemma-descent-data-coequalizer-statement : UUω
+  flattening-lemma-descent-data-coequalizer-statement =
+    universal-property-coequalizer c →
+    universal-property-coequalizer cofork-flattening-lemma-descent-coequalizer
+```
+
 ## Properties
 
 ### Proof of the flattening lemma for coequalizers
@@ -204,3 +272,110 @@ module _
             ( dependent-universal-property-pushout-dependent-universal-property-coequalizer
               ( dup-coequalizer))))
 ```
+
+### Proof of the descent data statement of the flattening lemma for coequalizers
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} {c : cofork F X}
+  (P : descent-data-coequalizer F l4)
+  (Q : X → UU l4)
+  (e : equiv-descent-data-coequalizer P (descent-data-family-cofork c Q))
+  where
+
+  equiv-double-arrow-flattening-lemma-descent-data-coequalizer :
+    equiv-double-arrow
+      ( double-arrow-flattening-lemma-descent-data-coequalizer P)
+      ( double-arrow-flattening-lemma-coequalizer F Q c)
+  pr1 equiv-double-arrow-flattening-lemma-descent-data-coequalizer =
+    equiv-tot
+      ( ( equiv-equiv-descent-data-coequalizer P
+          ( descent-data-family-cofork c Q)
+          ( e)) ∘
+        ( left-map-double-arrow F))
+  pr1 (pr2 equiv-double-arrow-flattening-lemma-descent-data-coequalizer) =
+    equiv-tot
+      ( equiv-equiv-descent-data-coequalizer P
+        ( descent-data-family-cofork c Q)
+        ( e))
+  pr1 (pr2 (pr2 equiv-double-arrow-flattening-lemma-descent-data-coequalizer)) =
+    refl-htpy
+  pr2 (pr2 (pr2 equiv-double-arrow-flattening-lemma-descent-data-coequalizer)) =
+    coherence-square-maps-Σ
+      ( Q ∘ map-cofork c)
+      ( map-equiv-descent-data-coequalizer
+        ( P)
+        ( descent-data-family-cofork c Q)
+        ( e) ∘ left-map-double-arrow F)
+      ( map-family-descent-data-coequalizer P)
+      ( λ a → tr Q (coh-cofork c a))
+      ( map-equiv-descent-data-coequalizer
+        ( P)
+        ( descent-data-family-cofork c Q)
+        ( e))
+      ( coherence-equiv-descent-data-coequalizer P
+        ( descent-data-family-cofork c Q)
+        ( e))
+
+  equiv-cofork-equiv-double-arrow-flattening-lemma-descent-data-coequalizer :
+    equiv-cofork-equiv-double-arrow
+      ( cofork-flattening-lemma-descent-coequalizer c P Q e)
+      ( cofork-flattening-lemma-coequalizer F Q c)
+      ( equiv-double-arrow-flattening-lemma-descent-data-coequalizer)
+  pr1
+    equiv-cofork-equiv-double-arrow-flattening-lemma-descent-data-coequalizer =
+    id-equiv
+  pr1
+    ( pr2
+        equiv-cofork-equiv-double-arrow-flattening-lemma-descent-data-coequalizer)
+    = refl-htpy
+  pr2
+    ( pr2
+      equiv-cofork-equiv-double-arrow-flattening-lemma-descent-data-coequalizer)
+    ( a , p) =
+    inv
+      ( ( left-whisker-concat _
+          ( compute-ap-map-Σ-map-base-eq-pair-Σ
+            ( map-cofork c)
+            ( Q)
+            ( refl)
+            ( coherence-equiv-descent-data-coequalizer P
+              ( descent-data-family-cofork c Q)
+              ( e)
+              ( a)
+              ( p)))) ∙
+        ( right-whisker-concat
+          ( ( right-unit) ∙
+            ( ap-id _) ∙
+            ( triangle-eq-pair-Σ Q (coh-cofork c a) _))
+          ( eq-pair-Σ refl
+            ( coherence-equiv-descent-data-coequalizer P
+              ( descent-data-family-cofork c Q)
+              ( e)
+              ( a)
+              ( p)))) ∙
+        ( ( left-whisker-concat-coherence-triangle-identifications'
+            ( eq-pair-Σ (coh-cofork c a) refl)
+            ( _)
+            ( _)
+            ( _)
+            ( left-inv-htpy-left-whisker
+              ( pair (map-cofork c (right-map-double-arrow F a)))
+              ( coherence-equiv-descent-data-coequalizer P
+                ( descent-data-family-cofork c Q)
+                ( e)
+                ( a))
+              ( p))) ∙
+          ( right-unit)))
+
+  abstract
+    flattening-lemma-descent-data-coequalizer :
+      flattening-lemma-descent-data-coequalizer-statement c P Q e
+    flattening-lemma-descent-data-coequalizer up-c =
+      universal-property-coequalizer-equiv-cofork-equiv-double-arrow
+        ( equiv-double-arrow-flattening-lemma-descent-data-coequalizer)
+        ( equiv-cofork-equiv-double-arrow-flattening-lemma-descent-data-coequalizer)
+        ( flattening-lemma-coequalizer F Q c
+          ( dependent-universal-property-universal-property-coequalizer up-c))
+```

From 2598dbb42fa82989157bd87fbf1d2fccdd1d474c Mon Sep 17 00:00:00 2001
From: VojtechStep <vojtechstepancik@outlook.com>
Date: Sun, 19 May 2024 00:41:50 +0200
Subject: [PATCH 10/10] Induction principle of identity types of coequalizers

---
 references.bib                                |  13 +
 src/synthetic-homotopy-theory.lagda.md        |   1 +
 ...ciple-identity-types-coequalizers.lagda.md | 392 ++++++++++++++++++
 3 files changed, 406 insertions(+)
 create mode 100644 src/synthetic-homotopy-theory/induction-principle-identity-types-coequalizers.lagda.md

diff --git a/references.bib b/references.bib
index 7f75bb02cd..3037943650 100644
--- a/references.bib
+++ b/references.bib
@@ -251,6 +251,19 @@ @online{GGMS24
   keywords    = {Computer Science - Logic in Computer Science,Mathematics - Logic}
 }
 
+@inproceedings{KvR21,
+  title =        {Path spaces of higher inductive types in homotopy type theory},
+  author =       {Kraus, Nicolai and von Raumer, Jakob},
+  year =         {2021},
+  publisher =    {IEEE Press},
+  abstract =     {The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. This result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman [1]), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman [2]). We provide a formalization of the main technical results in the proof assistant Lean.},
+  booktitle =    {Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science},
+  articleno =    {7},
+  numpages =     {13},
+  location =     {Vancouver, Canada},
+  series =       {LICS '19}
+}
+
 @article{KECA17,
   title       = {{Notions of Anonymous Existence in {{Martin-L\"of}} Type Theory}},
   author      = {Nicolai Kraus and Martín Escardó and Thierry Coquand and Thorsten Altenkirch},
diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index beb0fd0ca1..bb09b6713e 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -73,6 +73,7 @@ open import synthetic-homotopy-theory.functoriality-sequential-colimits public
 open import synthetic-homotopy-theory.functoriality-suspensions public
 open import synthetic-homotopy-theory.groups-of-loops-in-1-types public
 open import synthetic-homotopy-theory.hatchers-acyclic-type public
+open import synthetic-homotopy-theory.induction-principle-identity-types-coequalizers public
 open import synthetic-homotopy-theory.induction-principle-pushouts public
 open import synthetic-homotopy-theory.infinite-complex-projective-space public
 open import synthetic-homotopy-theory.infinite-cyclic-types public
diff --git a/src/synthetic-homotopy-theory/induction-principle-identity-types-coequalizers.lagda.md b/src/synthetic-homotopy-theory/induction-principle-identity-types-coequalizers.lagda.md
new file mode 100644
index 0000000000..7189f2e795
--- /dev/null
+++ b/src/synthetic-homotopy-theory/induction-principle-identity-types-coequalizers.lagda.md
@@ -0,0 +1,392 @@
+# The induction principle of identity types of coequalizers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+module synthetic-homotopy-theory.induction-principle-identity-types-coequalizers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.double-arrows
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.singleton-induction
+open import foundation.torsorial-type-families
+open import foundation.transport-along-identifications
+open import foundation.universal-property-identity-types
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.coforks
+open import synthetic-homotopy-theory.descent-data-coequalizers
+open import synthetic-homotopy-theory.descent-data-coequalizers-equivalence-families
+open import synthetic-homotopy-theory.descent-data-coequalizers-function-families
+open import synthetic-homotopy-theory.descent-property-coequalizers
+open import synthetic-homotopy-theory.equivalences-descent-data-coequalizers
+open import synthetic-homotopy-theory.families-descent-data-coequalizers
+open import synthetic-homotopy-theory.flattening-lemma-coequalizers
+open import synthetic-homotopy-theory.morphisms-descent-data-coequalizers
+open import synthetic-homotopy-theory.sections-descent-data-coequalizers
+open import synthetic-homotopy-theory.universal-property-coequalizers
+```
+
+</details>
+
+## Idea
+
+The formalization is inspired by {{#cite KvR21}}, but uses the dependent
+induction principle instead of recursion and uniqueness (i.e. initiality), and
+doesn't use wild categories for the arguments.
+
+## Definitions
+
+### The induction principle of descent data for identity types of coequalizers
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  (Q : descent-data-coequalizer F l4)
+  where
+
+  ev-point-hom-descent-data-coequalizer :
+    {b : codomain-double-arrow F} (p : family-descent-data-coequalizer P b) →
+    hom-descent-data-coequalizer P Q →
+    family-descent-data-coequalizer Q b
+  ev-point-hom-descent-data-coequalizer p h =
+    map-hom-descent-data-coequalizer P Q h _ p
+
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  (P : descent-data-coequalizer F l3)
+  {b₀ : codomain-double-arrow F}
+  (p₀ : family-descent-data-coequalizer P b₀)
+  where
+
+  induction-principle-descent-data-identity-type-coequalizer : UUω
+  induction-principle-descent-data-identity-type-coequalizer =
+    {l : Level}
+    (Q :
+      descent-data-coequalizer
+        ( double-arrow-flattening-lemma-descent-data-coequalizer P)
+        ( l)) →
+    (q₀ : family-descent-data-coequalizer Q (b₀ , p₀)) →
+    Σ ( section-descent-data-coequalizer Q)
+      ( λ s → pr1 s (b₀ , p₀) ＝ q₀)
+```
+
+### Canonical descent data for identity types of coequalizers
+
+```agda
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} (c : cofork F X)
+  (x₀ : X)
+  where
+
+  descent-data-coequalizer-identity-type :
+    descent-data-coequalizer F l3
+  pr1 descent-data-coequalizer-identity-type b =
+    x₀ ＝ map-cofork c b
+  pr2 descent-data-coequalizer-identity-type a =
+    equiv-concat' x₀ (coh-cofork c a)
+
+  equiv-descent-data-coequalizer-identity-type :
+    equiv-descent-data-coequalizer
+      ( descent-data-family-cofork c
+        ( λ x → x₀ ＝ x))
+      ( descent-data-coequalizer-identity-type)
+  pr1 equiv-descent-data-coequalizer-identity-type _ =
+    id-equiv
+  pr2 equiv-descent-data-coequalizer-identity-type a =
+    tr-Id-right (coh-cofork c a)
+
+  family-with-descent-data-coequalizer-identity-type :
+    family-with-descent-data-coequalizer c l3
+  pr1 family-with-descent-data-coequalizer-identity-type x =
+    x₀ ＝ x
+  pr1 (pr2 family-with-descent-data-coequalizer-identity-type) =
+    descent-data-coequalizer-identity-type
+  pr2 (pr2 family-with-descent-data-coequalizer-identity-type) =
+    equiv-descent-data-coequalizer-identity-type
+```
+
+## Properties
+
+### The canonical descent data for identity types of coequalizers satisfies the induction principle
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} {c : cofork F X}
+  (b₀ : codomain-double-arrow F)
+  (Q : family-with-descent-data-coequalizer c l4)
+  where
+
+  pentagon-ev-point-hom-descent-data-coequalizer :
+    ( ( map-family-with-descent-data-coequalizer Q b₀) ∘
+      ( ev-refl
+        ( map-cofork c b₀)
+        { B =
+          λ x _ → family-cofork-family-with-descent-data-coequalizer Q x})) ~
+    ( ( ev-point-hom-descent-data-coequalizer
+        ( descent-data-coequalizer-identity-type c (map-cofork c b₀))
+        ( descent-data-family-with-descent-data-coequalizer Q)
+        ( refl)) ∘
+      ( map-equiv
+        ( compute-section-family-cofork-function-family
+          ( family-with-descent-data-coequalizer-identity-type c
+            ( map-cofork c b₀))
+          ( Q))) ∘
+      ( section-descent-data-section-family-cofork
+        ( family-with-descent-data-coequalizer-function-family
+          ( family-with-descent-data-coequalizer-identity-type c
+            ( map-cofork c b₀))
+          ( Q))))
+  pentagon-ev-point-hom-descent-data-coequalizer = refl-htpy
+
+module _
+  {l1 l2 l3 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} {c : cofork F X}
+  (up-c : universal-property-coequalizer c)
+  (b₀ : codomain-double-arrow F)
+  where
+
+  is-equiv-ev-point-hom-descent-data-coequalizer-identity-type :
+    {l4 : Level} (Q : family-with-descent-data-coequalizer c l4) →
+    is-equiv
+      ( ev-point-hom-descent-data-coequalizer
+        ( descent-data-coequalizer-identity-type c (map-cofork c b₀))
+        ( descent-data-family-with-descent-data-coequalizer Q)
+        ( refl))
+  is-equiv-ev-point-hom-descent-data-coequalizer-identity-type Q =
+    is-equiv-right-map-triangle
+      ( ( map-family-with-descent-data-coequalizer Q b₀) ∘
+        ( ev-refl
+          ( map-cofork c b₀)
+          { B =
+            λ x _ → family-cofork-family-with-descent-data-coequalizer Q x}))
+      ( ev-point-hom-descent-data-coequalizer
+        ( descent-data-coequalizer-identity-type c (map-cofork c b₀))
+        ( descent-data-family-with-descent-data-coequalizer Q)
+        ( refl))
+      ( ( map-equiv
+          ( compute-section-family-cofork-function-family
+            ( family-with-descent-data-coequalizer-identity-type c
+              ( map-cofork c b₀))
+            ( Q))) ∘
+        ( section-descent-data-section-family-cofork
+          ( family-with-descent-data-coequalizer-function-family
+            ( family-with-descent-data-coequalizer-identity-type c
+              ( map-cofork c b₀))
+            ( Q))))
+      ( pentagon-ev-point-hom-descent-data-coequalizer b₀ Q)
+      ( is-equiv-comp _ _
+        ( is-equiv-ev-refl (map-cofork c b₀))
+        ( is-equiv-map-family-with-descent-data-coequalizer Q b₀))
+      ( is-equiv-comp _ _
+        ( is-equiv-section-descent-data-section-family-cofork _ up-c)
+        ( is-equiv-map-equiv
+          ( compute-section-family-cofork-function-family _ _)))
+
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} {c : cofork F X}
+  (up-c : universal-property-coequalizer c)
+  (b₀ : codomain-double-arrow F)
+  where
+
+  induction-principle-identity-type-descent-data-coequalizer-identity-type :
+    induction-principle-descent-data-identity-type-coequalizer
+      ( descent-data-coequalizer-identity-type c (map-cofork c b₀))
+      ( refl)
+  induction-principle-identity-type-descent-data-coequalizer-identity-type
+    Q q₀ =
+    ( ( λ b →
+        map-hom-descent-data-coequalizer _ _
+          ( map-inv-is-equiv is-equiv-ev-point-Q q₀)
+          ( b)
+          ( eq-is-contr (is-torsorial-Id (map-cofork c b₀)))) ,
+      ( λ (a , p) →
+        inv
+          ( ( ap
+              ( map-hom-descent-data-coequalizer _ _
+                ( map-inv-is-equiv is-equiv-ev-point-Q q₀)
+                ( right-map-double-arrow F a , p ∙ coh-cofork c a))
+              ( eq-is-contr
+                ( is-prop-is-contr (is-torsorial-Id (map-cofork c b₀)) _ _))) ∙
+            ( coherence-hom-descent-data-coequalizer _ _
+              ( map-inv-is-equiv is-equiv-ev-point-Q q₀)
+              ( a , p)
+              ( eq-is-contr (is-torsorial-Id (map-cofork c b₀))))))) ,
+    ( ( ap
+        ( map-hom-descent-data-coequalizer _ _
+          ( map-inv-is-equiv is-equiv-ev-point-Q q₀)
+          ( b₀ , refl))
+        ( left-inv _)) ∙
+      ( is-section-map-inv-is-equiv is-equiv-ev-point-Q q₀))
+    where
+      cofork-flattening :
+        cofork
+          ( double-arrow-flattening-lemma-descent-data-coequalizer
+            ( descent-data-coequalizer-identity-type c (map-cofork c b₀)))
+          ( Σ X (λ x → map-cofork c b₀ ＝ x))
+      cofork-flattening =
+        cofork-flattening-lemma-descent-coequalizer c
+          ( descent-data-coequalizer-identity-type c (map-cofork c b₀))
+          ( λ x → map-cofork c b₀ ＝ x)
+          ( inv-equiv-descent-data-coequalizer
+            ( equiv-descent-data-coequalizer-identity-type c
+              ( map-cofork c b₀)))
+      up-flattening : universal-property-coequalizer cofork-flattening
+      up-flattening =
+        flattening-lemma-descent-data-coequalizer
+          ( descent-data-coequalizer-identity-type c (map-cofork c b₀))
+          ( λ x → map-cofork c b₀ ＝ x)
+          ( inv-equiv-descent-data-coequalizer
+            ( equiv-descent-data-coequalizer-identity-type c
+              ( map-cofork c b₀)))
+          ( up-c)
+      is-equiv-ev-point-Q :
+        is-equiv
+          ( ev-point-hom-descent-data-coequalizer
+            ( descent-data-coequalizer-identity-type
+              ( cofork-flattening)
+              ( map-cofork cofork-flattening (b₀ , refl)))
+            ( descent-data-family-with-descent-data-coequalizer
+              ( family-with-descent-data-coequalizer-descent-data-coequalizer
+                ( up-flattening)
+              ( Q)))
+            ( refl))
+      is-equiv-ev-point-Q =
+        is-equiv-ev-point-hom-descent-data-coequalizer-identity-type
+          ( up-flattening)
+          ( b₀ , refl)
+          ( family-with-descent-data-coequalizer-descent-data-coequalizer
+            ( flattening-lemma-descent-data-coequalizer
+              ( descent-data-coequalizer-identity-type c (map-cofork c b₀))
+              ( λ x → map-cofork c b₀ ＝ x)
+              ( inv-equiv-descent-data-coequalizer
+                ( equiv-descent-data-coequalizer-identity-type c
+                  ( map-cofork c b₀)))
+              ( up-c))
+            ( Q))
+```
+
+## Theorem
+
+This should eventually be unique uniqueness, i.e. the type of equivalences out
+of the descent data for the identity type such that the equivalence sends `refl`
+to `p₀` should be contractible, not just inhabited.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2}
+  {X : UU l3} {c : cofork F X}
+  (up-c : universal-property-coequalizer c)
+  (P : family-with-descent-data-coequalizer c l4)
+  {b₀ : codomain-double-arrow F}
+  (p₀ : family-family-with-descent-data-coequalizer P b₀)
+  where
+
+  map-compute-identity-type-coequalizer :
+    (x : X) → (map-cofork c b₀ ＝ x) →
+    family-cofork-family-with-descent-data-coequalizer P x
+  map-compute-identity-type-coequalizer .(map-cofork c b₀) refl =
+    map-inv-equiv (equiv-family-with-descent-data-coequalizer P b₀) p₀
+
+  module _
+    (ip-P :
+      induction-principle-descent-data-identity-type-coequalizer
+        ( descent-data-family-with-descent-data-coequalizer P)
+        ( p₀))
+    where
+
+    ind-singleton-induction-principle-descent-data-identity-type-coequalizer :
+      {l : Level} →
+      (Q : Σ X (family-cofork-family-with-descent-data-coequalizer P) → UU l) →
+      (q₀ :
+        Q ( ( map-cofork c b₀) ,
+            ( map-inv-equiv
+              ( equiv-family-with-descent-data-coequalizer P b₀)
+              ( p₀)))) →
+      (x : Σ X (family-cofork-family-with-descent-data-coequalizer P)) → Q x
+    ind-singleton-induction-principle-descent-data-identity-type-coequalizer
+      {l} Q q₀ =
+      map-inv-is-equiv
+        ( is-equiv-section-descent-data-section-family-cofork
+          ( Q , Q-descent-data , id-equiv-descent-data-coequalizer _)
+          ( flattening-lemma-descent-data-coequalizer
+            ( descent-data-family-with-descent-data-coequalizer P)
+            ( family-cofork-family-with-descent-data-coequalizer P)
+            ( inv-equiv-descent-data-coequalizer
+              ( equiv-descent-data-family-with-descent-data-coequalizer P))
+            ( up-c)))
+        ( pr1 (ip-P Q-descent-data q₀))
+      where
+        Q-descent-data :
+          descent-data-coequalizer
+            ( double-arrow-flattening-lemma-descent-data-coequalizer
+              ( descent-data-family-with-descent-data-coequalizer P))
+            ( l)
+        Q-descent-data =
+          descent-data-family-cofork
+            ( cofork-flattening-lemma-descent-coequalizer c
+              ( descent-data-family-with-descent-data-coequalizer P)
+              ( family-cofork-family-with-descent-data-coequalizer P)
+              ( inv-equiv-descent-data-coequalizer
+                ( equiv-descent-data-family-with-descent-data-coequalizer P)))
+            ( Q)
+
+    is-equiv-map-compute-identity-type-coequalizer :
+      (x : X) → is-equiv (map-compute-identity-type-coequalizer x)
+    is-equiv-map-compute-identity-type-coequalizer =
+      fundamental-theorem-id
+        ( is-contr-ind-singleton _ _
+          ( ind-singleton-induction-principle-descent-data-identity-type-coequalizer))
+        ( map-compute-identity-type-coequalizer)
+
+    compute-identity-type-coequalizer :
+      (x : X) →
+      (map-cofork c b₀ ＝ x) ≃
+      family-cofork-family-with-descent-data-coequalizer P x
+    pr1 (compute-identity-type-coequalizer x) =
+      map-compute-identity-type-coequalizer x
+    pr2 (compute-identity-type-coequalizer x) =
+      is-equiv-map-compute-identity-type-coequalizer x
+
+    abstract
+      uniqueness-induction-principle-identity-type-coequalizer :
+        equiv-descent-data-coequalizer
+          ( descent-data-coequalizer-identity-type c (map-cofork c b₀))
+          ( descent-data-family-with-descent-data-coequalizer P)
+      uniqueness-induction-principle-identity-type-coequalizer =
+        map-equiv
+          ( compute-section-family-cofork-equivalence-family
+            ( family-with-descent-data-coequalizer-identity-type c
+              ( map-cofork c b₀))
+            ( P))
+          ( section-descent-data-section-family-cofork
+            ( family-with-descent-data-coequalizer-equivalence-family
+              ( family-with-descent-data-coequalizer-identity-type c
+                ( map-cofork c b₀))
+              ( P))
+            ( compute-identity-type-coequalizer))
+
+      compute-uniqueness-induction-principle-identity-type-coequalizer :
+        map-equiv-descent-data-coequalizer _ _
+          ( uniqueness-induction-principle-identity-type-coequalizer)
+          ( b₀)
+          ( refl) ＝
+        p₀
+      compute-uniqueness-induction-principle-identity-type-coequalizer =
+        is-section-map-inv-equiv
+          ( equiv-family-with-descent-data-coequalizer P b₀)
+          ( p₀)
+```