open import Cat.Prelude

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

Coequalisers🔗

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

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