open import Cat.Prelude module Cat.Diagram.Equaliser {β ββ²} (C : Precategory β ββ²) where
Equalisersπ
The equaliser of two maps , when it exists, represents the largest subobject of where and 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