Coforks, coequalizers of types, their flattening lemma (UniMath#792)

This PR introduces coforks of parallel maps, the dependent and
non-dependent universal properties of coequalizers, the construction of
coequalizers from pushouts, and the flattening lemma for coequalizers,
asserting that sigmas commute with coequalizers.

This development mirrors the development of cocones and pushouts.

I also changed the statement of the flattening lemma for pushouts to one
that sounds more natural to me - we can construct a cocone of sigma
types from any cocone, not just a pushout; the previous definition
required the vertex to be a pushout in those definitions. Now the
statement is "if a cocone is a pushout, then the cocone derived from it
is a pushout too".

src/foundation.lagda.md

@@ -40,6 +40,7 @@ open import foundation.cartesian-product-types public
 open import foundation.cartesian-products-set-quotients public
 open import foundation.category-of-sets public
 open import foundation.choice-of-representatives-equivalence-relation public
+open import foundation.codiagonal-maps-of-types public
 open import foundation.coherently-invertible-maps public
 open import foundation.commuting-3-simplices-of-homotopies public
 open import foundation.commuting-3-simplices-of-maps public

src/foundation/codiagonal-maps-of-types.lagda.md

@@ -0,0 +1,32 @@
+# Codiagonal maps of types
+
+```agda
+module foundation.codiagonal-maps-of-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import foundation-core.coproduct-types
+```
+
+</details>
+
+## Idea
+
+The codiagonal map `∇ : A + A → A` of `A` is the map that projects `A + A` onto
+`A`.
+
+## Definitions
+
+```agda
+module _
+  { l1 : Level} (A : UU l1)
+  where
+
+  codiagonal : A + A → A
+  codiagonal (inl a) = a
+  codiagonal (inr a) = a
+```

src/synthetic-homotopy-theory.lagda.md

@@ -14,11 +14,15 @@ open import synthetic-homotopy-theory.cavallos-trick public
 open import synthetic-homotopy-theory.circle public
 open import synthetic-homotopy-theory.cocones-under-spans public
 open import synthetic-homotopy-theory.cocones-under-spans-of-pointed-types public
+open import synthetic-homotopy-theory.coequalizers public
 open import synthetic-homotopy-theory.cofibers public
+open import synthetic-homotopy-theory.coforks public
 open import synthetic-homotopy-theory.conjugation-loops public
 open import synthetic-homotopy-theory.dependent-cocones-under-spans public
+open import synthetic-homotopy-theory.dependent-coforks public
 open import synthetic-homotopy-theory.dependent-pullback-property-pushouts public
 open import synthetic-homotopy-theory.dependent-suspension-structures public
+open import synthetic-homotopy-theory.dependent-universal-property-coequalizers public
 open import synthetic-homotopy-theory.dependent-universal-property-pushouts public
 open import synthetic-homotopy-theory.dependent-universal-property-suspensions public
 open import synthetic-homotopy-theory.descent-circle public
@@ -28,6 +32,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.double-loop-spaces public
+open import synthetic-homotopy-theory.flattening-lemma-coequalizers public
 open import synthetic-homotopy-theory.flattening-lemma-pushouts public
 open import synthetic-homotopy-theory.free-loops public
 open import synthetic-homotopy-theory.functoriality-loop-spaces public
@@ -58,6 +63,7 @@ open import synthetic-homotopy-theory.suspensions-of-types public
 open import synthetic-homotopy-theory.triple-loop-spaces public
 open import synthetic-homotopy-theory.universal-cover-circle public
 open import synthetic-homotopy-theory.universal-property-circle public
+open import synthetic-homotopy-theory.universal-property-coequalizers public
 open import synthetic-homotopy-theory.universal-property-pushouts public
 open import synthetic-homotopy-theory.universal-property-suspensions public
 open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types public

src/synthetic-homotopy-theory/coequalizers.lagda.md

@@ -0,0 +1,119 @@
+# Coequalizers
+
+```agda
+module synthetic-homotopy-theory.coequalizers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.codiagonal-maps-of-types
+open import foundation.coproduct-types
+open import foundation.equivalences
+open import foundation.identity-types
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.coforks
+open import synthetic-homotopy-theory.dependent-cocones-under-spans
+open import synthetic-homotopy-theory.dependent-coforks
+open import synthetic-homotopy-theory.dependent-universal-property-coequalizers
+open import synthetic-homotopy-theory.pushouts
+open import synthetic-homotopy-theory.universal-property-coequalizers
+```
+
+</details>
+
+## Idea
+
+The **coequalizer** of a parallel pair `f, g : A → B` is the colimiting
+[cofork](synthetic-homotopy-theory.coforks.md), i.e. a cofork with the
+[universal property of coequalizers](synthetic-homotopy-theory.universal-property-coequalizers.md).
+
+## Properties
+
+### All parallel pairs admit a coequalizer
+
+The **canonical coequalizer** may be obtained as a
+[pushout](synthetic-homotopy-theory.pushouts.md) of the span
+
+```text
+     ∇         [f,g]
+A <----- A + A -----> B
+```
+
+where the left map is the
+[codiagonal map](foundation.codiagonal-maps-of-types.md), sending `inl(a)` and
+`inr(a)` to `a`, and the right map is defined by the universal property of
+[coproducts](foundation.coproduct-types.md) to send `inl(a)` to `f(a)` and
+`inr(a)` to `g(a)`.
+
+The pushout thus constructed will consist of a copy of `B`, a copy of `A`, and
+for every point `a` of `A` there will be a path from `f(a)` to `a` and to
+`g(a)`, which corresponds to having a copy of `B` with paths connecting every
+`f(a)` to `g(a)`.
+
+The construction from pushouts itself is an implementation detail, which is why
+the definition is marked abstract.
+
+```agda
+module _
+  { l1 l2 : Level} {A : UU l1} {B : UU l2} (f g : A → B)
+  where
+
+  abstract
+    canonical-coequalizer : UU (l1 ⊔ l2)
+    canonical-coequalizer =
+      pushout (codiagonal A) (ind-coprod (λ _ → B) f g)
+
+    cofork-canonical-coequalizer : cofork f g canonical-coequalizer
+    cofork-canonical-coequalizer =
+      cofork-cocone-codiagonal f g
+        ( cocone-pushout (codiagonal A) (ind-coprod (λ _ → B) f g))
+
+    dup-canonical-coequalizer :
+      { l : Level} →
+      dependent-universal-property-coequalizer l f g
+        ( cofork-canonical-coequalizer)
+    dup-canonical-coequalizer P =
+      is-equiv-comp-htpy
+        ( dependent-cofork-map f g cofork-canonical-coequalizer)
+        ( dependent-cofork-dependent-cocone-codiagonal f g
+          ( cofork-canonical-coequalizer)
+          ( P))
+        ( dependent-cocone-map
+          ( codiagonal A)
+          ( ind-coprod (λ _ → B) f g)
+          ( cocone-codiagonal-cofork f g cofork-canonical-coequalizer)
+          ( P))
+        ( triangle-dependent-cofork-dependent-cocone-codiagonal f g
+          ( cofork-canonical-coequalizer)
+          ( P))
+        ( tr
+          ( λ c →
+            is-equiv
+              ( dependent-cocone-map
+                ( codiagonal A)
+                ( ind-coprod (λ _ → B) f g)
+                ( c)
+                ( P)))
+          ( inv
+            ( is-retraction-map-inv-is-equiv
+              ( is-equiv-cofork-cocone-codiagonal f g)
+              ( cocone-pushout (codiagonal A) (ind-coprod (λ _ → B) f g))))
+          ( dependent-up-pushout
+            ( codiagonal A)
+            ( ind-coprod (λ _ → B) f g)
+            ( P)))
+        ( is-equiv-dependent-cofork-dependent-cocone-codiagonal f g
+          ( cofork-canonical-coequalizer)
+          ( P))
+
+    up-canonical-coequalizer :
+      { l : Level} →
+      universal-property-coequalizer l f g cofork-canonical-coequalizer
+    up-canonical-coequalizer =
+      universal-property-dependent-universal-property-coequalizer f g
+        ( cofork-canonical-coequalizer)
+        ( dup-canonical-coequalizer)
+```