Rebase infrastructure for coequalizers to double arrows (#1098)

In anticipation of #885. The proof of the universal property of
coequalizers being preserved by equivalences of coforks got a bit
unwieldy, but it should become more conceptual once morphisms and
equivalences of cocones under spans are integrated (for now they exist
only in the other PR).

src/foundation.lagda.md

@@ -128,6 +128,7 @@ open import foundation.discrete-relaxed-sigma-decompositions public
 open import foundation.discrete-sigma-decompositions public
 open import foundation.discrete-types public
 open import foundation.disjunction public
+open import foundation.double-arrows public
 open import foundation.double-negation public
 open import foundation.double-negation-modality public
 open import foundation.double-powersets public
@@ -152,6 +153,7 @@ open import foundation.equivalence-relations public
 open import foundation.equivalences public
 open import foundation.equivalences-arrows public
 open import foundation.equivalences-cospans public
+open import foundation.equivalences-double-arrows public
 open import foundation.equivalences-inverse-sequential-diagrams public
 open import foundation.equivalences-maybe public
 open import foundation.equivalences-span-diagrams public
@@ -248,6 +250,7 @@ open import foundation.morphisms-arrows public
 open import foundation.morphisms-binary-relations public
 open import foundation.morphisms-cospan-diagrams public
 open import foundation.morphisms-cospans public
+open import foundation.morphisms-double-arrows public
 open import foundation.morphisms-inverse-sequential-diagrams public
 open import foundation.morphisms-span-diagrams public
 open import foundation.morphisms-spans public

src/foundation/double-arrows.lagda.md

@@ -0,0 +1,81 @@
+# Double arrows
+
+```agda
+module foundation.double-arrows where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A {{#concept "double arrow" Disambiguation="between types" Agda=double-arrow}}
+is a [pair](foundation.dependent-pair-types.md) of types `A`, `B`
+[equipped](foundation.structure.md) with a pair of
+[maps](foundation.function-types.md) `f, g : A → B`.
+
+We draw a double arrow as
+
+```text
+     A
+    | |
+  f | | g
+    | |
+    ∨ ∨
+     B
+```
+
+where `f` is the first map in the structure and `g` is the second map in the
+structure. We also call `f` the _left map_ and `g` the _right map_. By
+convention, [homotopies](foundation-core.homotopies.md) go from left to right.
+
+## Definitions
+
+### Double arrows
+
+```agda
+double-arrow : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+double-arrow l1 l2 = Σ (UU l1) (λ A → Σ (UU l2) (λ B → (A → B) × (A → B)))
+
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  (f : A → B) (g : A → B)
+  where
+
+  make-double-arrow : double-arrow l1 l2
+  make-double-arrow = (A , B , f , g)
+
+  {-# INLINE make-double-arrow #-}
+```
+
+### Components of a double arrow
+
+```agda
+module _
+  {l1 l2 : Level} (a : double-arrow l1 l2)
+  where
+
+  domain-double-arrow : UU l1
+  domain-double-arrow = pr1 a
+
+  codomain-double-arrow : UU l2
+  codomain-double-arrow = pr1 (pr2 a)
+
+  left-map-double-arrow : domain-double-arrow → codomain-double-arrow
+  left-map-double-arrow = pr1 (pr2 (pr2 a))
+
+  right-map-double-arrow : domain-double-arrow → codomain-double-arrow
+  right-map-double-arrow = pr2 (pr2 (pr2 a))
+```
+
+## See also
+
+- Colimits of double arrows are
+  [coequalizers](synthetic-homotopy-theory.coequalizers.md)

src/foundation/equivalences-double-arrows.lagda.md

@@ -0,0 +1,225 @@
+# Equivalences of double arrows
+
+```agda
+module foundation.equivalences-double-arrows where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+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.equivalences-arrows
+open import foundation.homotopies
+open import foundation.morphisms-double-arrows
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An
+{{#concept "equivalence of double arrows" Disambiguation="between types" Agda=equiv-double-arrow}}
+from a [double arrow](foundation.double-arrows.md) `f, g : A → B` to a double
+arrow `h, k : X → Y` is a pair of
+[equivalences](foundation-core.equivalences.md) `i : A ≃ X` and `j : B ≃ Y`,
+such that the squares
+
+```text
+           i                   i
+     A --------> X       A --------> X
+     |     ≃     |       |     ≃     |
+   f |           | h   g |           | k
+     |           |       |           |
+     ∨     ≃     ∨       ∨     ≃     ∨
+     B --------> Y       B --------> Y
+           j                   j
+```
+
+[commute](foundation-core.commuting-squares-of-maps.md). The equivalence `i` is
+referred to as the _domain equivalence_, and the `j` as the _codomain
+equivalence_.
+
+Alternatively, an equivalence of double arrows is a pair of
+[equivalences of arrows](foundation.equivalences-arrows.md) `f ≃ h` and `g ≃ k`
+that share the underlying maps.
+
+## Definitions
+
+### Equivalences of double arrows
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (a : double-arrow l1 l2) (a' : double-arrow l3 l4)
+  where
+
+  left-coherence-equiv-double-arrow :
+    (domain-double-arrow a ≃ domain-double-arrow a') →
+    (codomain-double-arrow a ≃ codomain-double-arrow a') →
+    UU (l1 ⊔ l4)
+  left-coherence-equiv-double-arrow eA eB =
+    left-coherence-hom-double-arrow a a' (map-equiv eA) (map-equiv eB)
+
+  right-coherence-equiv-double-arrow :
+    (domain-double-arrow a ≃ domain-double-arrow a') →
+    (codomain-double-arrow a ≃ codomain-double-arrow a') →
+    UU (l1 ⊔ l4)
+  right-coherence-equiv-double-arrow eA eB =
+    right-coherence-hom-double-arrow a a' (map-equiv eA) (map-equiv eB)
+
+  equiv-double-arrow :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  equiv-double-arrow =
+    Σ ( domain-double-arrow a ≃ domain-double-arrow a')
+      ( λ eA →
+        Σ ( codomain-double-arrow a ≃ codomain-double-arrow a')
+          ( λ eB →
+            left-coherence-equiv-double-arrow eA eB ×
+            right-coherence-equiv-double-arrow eA eB))
+```
+
+### Components of an equivalence of double arrows
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (a : double-arrow l1 l2) (a' : double-arrow l3 l4)
+  (e : equiv-double-arrow a a')
+  where
+
+  domain-equiv-equiv-double-arrow :
+    domain-double-arrow a ≃ domain-double-arrow a'
+  domain-equiv-equiv-double-arrow = pr1 e
+
+  domain-map-equiv-double-arrow :
+    domain-double-arrow a → domain-double-arrow a'
+  domain-map-equiv-double-arrow = map-equiv domain-equiv-equiv-double-arrow
+
+  is-equiv-domain-map-equiv-double-arrow :
+    is-equiv domain-map-equiv-double-arrow
+  is-equiv-domain-map-equiv-double-arrow =
+    is-equiv-map-equiv domain-equiv-equiv-double-arrow
+
+  codomain-equiv-equiv-double-arrow :
+    codomain-double-arrow a ≃ codomain-double-arrow a'
+  codomain-equiv-equiv-double-arrow = pr1 (pr2 e)
+
+  codomain-map-equiv-double-arrow :
+    codomain-double-arrow a → codomain-double-arrow a'
+  codomain-map-equiv-double-arrow = map-equiv codomain-equiv-equiv-double-arrow
+
+  is-equiv-codomain-map-equiv-double-arrow :
+    is-equiv codomain-map-equiv-double-arrow
+  is-equiv-codomain-map-equiv-double-arrow =
+    is-equiv-map-equiv codomain-equiv-equiv-double-arrow
+
+  left-square-equiv-double-arrow :
+    left-coherence-equiv-double-arrow a a'
+      ( domain-equiv-equiv-double-arrow)
+      ( codomain-equiv-equiv-double-arrow)
+  left-square-equiv-double-arrow = pr1 (pr2 (pr2 e))
+
+  left-equiv-arrow-equiv-double-arrow :
+    equiv-arrow (left-map-double-arrow a) (left-map-double-arrow a')
+  pr1 left-equiv-arrow-equiv-double-arrow =
+    domain-equiv-equiv-double-arrow
+  pr1 (pr2 left-equiv-arrow-equiv-double-arrow) =
+    codomain-equiv-equiv-double-arrow
+  pr2 (pr2 left-equiv-arrow-equiv-double-arrow) =
+    left-square-equiv-double-arrow
+
+  right-square-equiv-double-arrow :
+    right-coherence-equiv-double-arrow a a'
+      ( domain-equiv-equiv-double-arrow)
+      ( codomain-equiv-equiv-double-arrow)
+  right-square-equiv-double-arrow = pr2 (pr2 (pr2 e))
+
+  right-equiv-arrow-equiv-double-arrow :
+    equiv-arrow (right-map-double-arrow a) (right-map-double-arrow a')
+  pr1 right-equiv-arrow-equiv-double-arrow =
+    domain-equiv-equiv-double-arrow
+  pr1 (pr2 right-equiv-arrow-equiv-double-arrow) =
+    codomain-equiv-equiv-double-arrow
+  pr2 (pr2 right-equiv-arrow-equiv-double-arrow) =
+    right-square-equiv-double-arrow
+
+  hom-double-arrow-equiv-double-arrow : hom-double-arrow a a'
+  pr1 hom-double-arrow-equiv-double-arrow =
+    domain-map-equiv-double-arrow
+  pr1 (pr2 hom-double-arrow-equiv-double-arrow) =
+    codomain-map-equiv-double-arrow
+  pr1 (pr2 (pr2 hom-double-arrow-equiv-double-arrow)) =
+    left-square-equiv-double-arrow
+  pr2 (pr2 (pr2 hom-double-arrow-equiv-double-arrow)) =
+    right-square-equiv-double-arrow
+```
+
+### The identity equivalence of double arrows
+
+```agda
+module _
+  {l1 l2 : Level} (a : double-arrow l1 l2)
+  where
+
+  id-equiv-double-arrow : equiv-double-arrow a a
+  pr1 id-equiv-double-arrow = id-equiv
+  pr1 (pr2 id-equiv-double-arrow) = id-equiv
+  pr2 (pr2 id-equiv-double-arrow) = (refl-htpy , refl-htpy)
+```
+
+### Composition of equivalences of double arrows
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  (a : double-arrow l1 l2) (b : double-arrow l3 l4) (c : double-arrow l5 l6)
+  (f : equiv-double-arrow b c) (e : equiv-double-arrow a b)
+  where
+
+  domain-equiv-comp-equiv-double-arrow :
+    domain-double-arrow a ≃ domain-double-arrow c
+  domain-equiv-comp-equiv-double-arrow =
+    domain-equiv-equiv-double-arrow b c f ∘e
+    domain-equiv-equiv-double-arrow a b e
+
+  codomain-equiv-comp-equiv-double-arrow :
+    codomain-double-arrow a ≃ codomain-double-arrow c
+  codomain-equiv-comp-equiv-double-arrow =
+    codomain-equiv-equiv-double-arrow b c f ∘e
+    codomain-equiv-equiv-double-arrow a b e
+
+  left-square-comp-equiv-double-arrow :
+    left-coherence-equiv-double-arrow a c
+      ( domain-equiv-comp-equiv-double-arrow)
+      ( codomain-equiv-comp-equiv-double-arrow)
+  left-square-comp-equiv-double-arrow =
+    coh-comp-equiv-arrow
+      ( left-map-double-arrow a)
+      ( left-map-double-arrow b)
+      ( left-map-double-arrow c)
+      ( left-equiv-arrow-equiv-double-arrow b c f)
+      ( left-equiv-arrow-equiv-double-arrow a b e)
+
+  right-square-comp-equiv-double-arrow :
+    right-coherence-equiv-double-arrow a c
+      ( domain-equiv-comp-equiv-double-arrow)
+      ( codomain-equiv-comp-equiv-double-arrow)
+  right-square-comp-equiv-double-arrow =
+    coh-comp-equiv-arrow
+      ( right-map-double-arrow a)
+      ( right-map-double-arrow b)
+      ( right-map-double-arrow c)
+      ( right-equiv-arrow-equiv-double-arrow b c f)
+      ( right-equiv-arrow-equiv-double-arrow a b e)
+
+  comp-equiv-double-arrow : equiv-double-arrow a c
+  pr1 comp-equiv-double-arrow = domain-equiv-comp-equiv-double-arrow
+  pr1 (pr2 comp-equiv-double-arrow) = codomain-equiv-comp-equiv-double-arrow
+  pr1 (pr2 (pr2 comp-equiv-double-arrow)) = left-square-comp-equiv-double-arrow
+  pr2 (pr2 (pr2 comp-equiv-double-arrow)) = right-square-comp-equiv-double-arrow
+```