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