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

EqualisersπŸ”—

The equaliser of two maps f,g:A→Bf, g : A \to B, when it exists, represents the largest subobject of AA where ff and gg 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
    universal : βˆ€ {F} {eβ€² : Hom F A} (p : f ∘ eβ€² ≑ g ∘ eβ€²) β†’ Hom F E
    factors   : βˆ€ {F} {eβ€² : Hom F A} {p : f ∘ eβ€² ≑ g ∘ eβ€²} β†’ equ ∘ universal p ≑ eβ€²
    unique
      : βˆ€ {F} {eβ€² : Hom F A} {p : f ∘ eβ€² ≑ g ∘ eβ€²} {other : Hom F E}
      β†’ equ ∘ other ≑ eβ€²
      β†’ other ≑ universal 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}  {o1 o2 : Hom F E}
    β†’ f ∘ eβ€² ≑ g ∘ eβ€²
    β†’ equ ∘ o1 ≑ eβ€²
    β†’ equ ∘ o2 ≑ eβ€²
    β†’ o1 ≑ o2
  uniqueβ‚‚ 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 =
  uniqueβ‚‚ (extendl equal) p refl
  where open is-equaliser equalises

Categories with all equalisersπŸ”—

We also define a helper module for working with categories that have equalisers of all parallel pairs of morphisms.

has-equalisers : Type _
has-equalisers = βˆ€ {a b} (f g : Hom a b) β†’ Equaliser f g

module Equalisers (all-equalisers : has-equalisers) where
  module equaliser {a b} (f g : Hom a b) = Equaliser (all-equalisers f g)

  Equ : βˆ€ {a b} (f g : Hom a b) β†’ Ob
  Equ = equaliser.apex