Merge branch 'master' into functor-categories

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