open import Cat.Prelude

module Cat.Diagram.Equaliser {â„“ â„“â€²} (C : Precategory â„“ â„“â€²) where


# EqualisersðŸ”—

The equaliser of two maps $f, g : A \to B$, when it exists, represents the largest subobject of $A$ where $f$ and $g$ agree. In this sense, the equaliser is the categorical generalisation of a solution set: The solution set of an equation in one variable is largest subset of the domain (i.e.Â what the variable ranges over) where the left- and right-hand-sides agree.

record is-equaliser {E} (f g : Hom A B) (equ : Hom E A) : Type (â„“ âŠ” â„“â€²) where
field
equal     : f âˆ˜ equ â‰¡ g âˆ˜ equ
limiting  : âˆ€ {F} {eâ€² : Hom F A} (p : f âˆ˜ eâ€² â‰¡ g âˆ˜ eâ€²) â†’ Hom F E
universal : âˆ€ {F} {eâ€² : Hom F A} {p : f âˆ˜ eâ€² â‰¡ g âˆ˜ eâ€²} â†’ equ âˆ˜ limiting p â‰¡ eâ€²
unique
: âˆ€ {F} {eâ€² : Hom F A} {p : f âˆ˜ eâ€² â‰¡ g âˆ˜ eâ€²} {lim' : Hom F E}
â†’ eâ€² â‰¡ equ âˆ˜ lim'
â†’ lim' â‰¡ limiting p

equal-âˆ˜ : f âˆ˜ equ âˆ˜ h â‰¡ g âˆ˜ equ âˆ˜ h
equal-âˆ˜ {h = h} =
f âˆ˜ equ âˆ˜ h â‰¡âŸ¨ extendl equal âŸ©â‰¡
g âˆ˜ equ âˆ˜ h âˆŽ

uniqueâ‚‚
: âˆ€ {F} {eâ€² : Hom F A} {p : f âˆ˜ eâ€² â‰¡ g âˆ˜ eâ€²} {lim' lim'' : Hom F E}
â†’ eâ€² â‰¡ equ âˆ˜ lim'
â†’ eâ€² â‰¡ equ âˆ˜ lim''
â†’ lim' â‰¡ lim''
uniqueâ‚‚ {p = p} q r = unique {p = p} q âˆ™ sym (unique r)


We can visualise the situation using the commutative diagram below:

There is also a convenient bundling of an equalising arrow together with its domain:

record Equaliser (f g : Hom A B) : Type (â„“ âŠ” â„“â€²) where
field
{apex}  : Ob
equ     : Hom apex A
has-is-eq : is-equaliser f g equ

open is-equaliser has-is-eq public


## Equalisers are monicðŸ”—

As a small initial application, we prove that equaliser arrows are always monic:

is-equaliserâ†’is-monic
: âˆ€ {E} (equ : Hom E A)
â†’ is-equaliser f g equ
â†’ is-monic equ
is-equaliserâ†’is-monic equ equalises g h p =
g                â‰¡âŸ¨ unique (sym p) âŸ©â‰¡
limiting equal-âˆ˜ â‰¡Ë˜âŸ¨ unique refl âŸ©â‰¡Ë˜
h âˆŽ
where open is-equaliser equalises