module Cat.Diagram.Colimit.Coequaliser {o h} (C : Precategory o h) where

We establish the correspondence between Coequaliser and the Colimit of a parallel arrows diagram.

is-coequaliser→is-colimit
:  {e} (F : Functor ·⇉· C) {coequ : Hom (F .F₀ true) e}
(coeq : is-coequaliser C (forkl F) (forkr F) coequ)
is-colimit {C = C} F e (Cofork→Cocone F (is-coequaliser.coequal coeq))
is-coequaliser→is-colimit {e} F {coequ} is-coeq =
to-is-colimitp mc λ where
{true}  refl
{false}  refl
where
module is-coeq = is-coequaliser is-coeq
open make-is-colimit

mc : make-is-colimit F e
mc .ψ true = coequ
mc .ψ false = coequ  forkl F
mc .commutes {true} {true} tt = elimr (F .F-id)
mc .commutes {false} {true} true = sym (is-coeq .coequal)
mc .commutes {false} {true} false = refl
mc .commutes {false} {false} tt = elimr (F .F-id)
mc .universal eta p =
is-coeq.universal (p {false} {true} false  sym (p {false} {true} true))
mc .factors {true} eta p =
is-coeq.factors
mc .factors {false} eta p =
pulll is-coeq.factors  p {false} {true} false
mc .unique eta p other q =
is-coeq.unique (q true)

is-colimit→is-coequaliser
:  (F : Functor ·⇉· C) {K : Functor ⊤Cat C}
{eta : F => K F∘ !F}
is-lan !F F K eta
is-coequaliser C (forkl F) (forkr F) (eta .η true)
is-colimit→is-coequaliser F {K} {eta} colim = co where
module colim = is-colimit colim

parallel
:  {x}  Hom (F .F₀ true) x
(j : Bool)  Hom (F .F₀ j) x
parallel e' true = e'
parallel e' false = e'  forkl F

parallel-commutes
:  {x} {e' : Hom (F .F₀ true) x}
e'  forkl F  e'  forkr F
i j  (h : ·⇉· .Precategory.Hom i j)
parallel e' j  F .F₁ {i} {j} h  parallel e' i
parallel-commutes p true true tt = elimr (F .F-id)
parallel-commutes p false true true = sym p
parallel-commutes p false true false = refl
parallel-commutes p false false tt = elimr (F .F-id)

co : is-coequaliser C (forkl F) (forkr F) (eta .η true)
co .coequal =
eta .is-natural false true false  sym (eta .is-natural false true true)
co .universal {e' = e'} p =
colim.universal (parallel e')  {i} {j} h  parallel-commutes p i j h)
co .factors = colim.factors {j = true} _ _
co .unique {p = p} {colim = other} q =
colim.unique _ _ _ λ where
true  q
false
ap (other ∘_) (introl (K .F-id)  sym (eta .is-natural false true true))
·· pulll q
·· sym p

Coequaliser→Colimit :  {F : Functor ·⇉· C}  Coequaliser C (forkl F) (forkr F)  Colimit F
Coequaliser→Colimit {F = F} coeq = to-colimit (is-coequaliser→is-colimit F (has-is-coeq coeq))

Colimit→Coequaliser :  {a b} {f g : Hom a b}  Colimit {C = C} (Fork f g)  Coequaliser C f g
Colimit→Coequaliser colim .coapex = _
Colimit→Coequaliser colim .coeq = _
Colimit→Coequaliser {f = f} {g} colim .has-is-coeq =
is-colimit→is-coequaliser (Fork f g) (Colimit.has-colimit colim)