module Cat.Diagram.Equaliser where


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 (o βŠ” β„“) where
      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'
        : βˆ€ {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 ∎
      : βˆ€ {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 (o βŠ” β„“) where
      {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:

    : βˆ€ {E} (equ : Hom E A)
    β†’ is-equaliser C 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 : βˆ€ {o β„“} β†’ Precategory o β„“ β†’ Type _
has-equalisers C = βˆ€ {a b} (f g : Hom a b) β†’ Equaliser C f g
  where open Precategory C

module Equalisers
  {o β„“}
  (C : Precategory o β„“)
  (all-equalisers : has-equalisers C)
  open Cat.Reasoning C
  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