open import Cat.Prelude

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

Coequalisers🔗

The coequaliser of two maps $f, g : A \to B$ (if it exists), represents the largest quotient object of $B$ that identifies $f$ and $g$.

record is-coequaliser {E} (f g : Hom A B) (coeq : Hom B E) : Type (o ⊔ ℓ) where
  field
    coequal    : coeq ∘ f ≡ coeq ∘ g
    coequalise : ∀ {F} {e′ : Hom B F} (p : e′ ∘ f ≡ e′ ∘ g) → Hom E F
    universal  : ∀ {F} {e′ : Hom B F} {p : e′ ∘ f ≡ e′ ∘ g}
               → coequalise p ∘ coeq ≡ e′

    unique     : ∀ {F} {e′ : Hom B F} {p : e′ ∘ f ≡ e′ ∘ g} {colim : Hom E F}
               → e′ ≡ colim ∘ coeq
               → colim ≡ coequalise p

  unique₂
    : ∀ {F} {e′ : Hom B F} {p : e′ ∘ f ≡ e′ ∘ g} {colim' colim'' : Hom E F}
    → e′ ≡ colim' ∘ coeq
    → e′ ≡ colim'' ∘ coeq
    → colim' ≡ colim''
  unique₂ {p = p} q r = unique {p = p} q ∙ sym (unique r)

  id-coequalise : id ≡ coequalise coequal
  id-coequalise = unique (sym (idl _))

There is also a convenient bundling of an coequalising arrow together with its codomain:

record Coequaliser (f g : Hom A B) : Type (o ⊔ ℓ) where
  field
    {coapex}  : Ob
    coeq      : Hom B coapex
    has-is-coeq : is-coequaliser f g coeq

  open is-coequaliser has-is-coeq public

Coequalisers are epic🔗

Dually to the situation with [equalisers], coequaliser arrows are always epic:

is-coequaliser→is-epic
  : ∀ {E} (coequ : Hom A E)
  → is-coequaliser f g coequ
  → is-epic coequ
is-coequaliser→is-epic {f = f} {g = g} equ equalises h i p =
  h                            ≡⟨ unique (sym p) ⟩≡
  coequalise (extendr coequal) ≡˘⟨ unique refl ⟩≡˘
  i                            ∎
  where open is-coequaliser equalises