module Cat.Diagram.Coequaliser where

Coequalisers🔗

The coequaliser of two maps (if it exists), represents the largest quotient object of that identifies and 

  record is-coequaliser {E} (f g : Hom A B) (coeq : Hom B E) : Type (o ⊔ ℓ) where
    field
      coequal    : coeq ∘ f ≡ coeq ∘ g
      universal  : ∀ {F} {e' : Hom B F} (p : e' ∘ f ≡ e' ∘ g) → Hom E F
      factors    : ∀ {F} {e' : Hom B F} {p : e' ∘ f ≡ e' ∘ g}
                 → universal p ∘ coeq ≡ e'

      unique     : ∀ {F} {e' : Hom B F} {p : e' ∘ f ≡ e' ∘ g} {other : Hom E F}
                 → other ∘ coeq ≡ e'
                 → other ≡ universal p

    uniqueâ‚‚
      : ∀ {F} {e' : Hom B F}  {o1 o2 : Hom E F}
      → (e' ∘ f ≡ e' ∘ g)
      → o1 ∘ coeq ≡ e'
      → o2 ∘ coeq ≡ e'
      → o1 ≡ o2
    unique₂ p q r = unique {p = p} q ∙ sym (unique r)

    id-coequalise : id ≡ universal coequal
    id-coequalise = unique (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
      coequ      : Hom B coapex
      has-is-coeq : is-coequaliser f g coequ

    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 C f g coequ
    → is-epic coequ
  is-coequaliser→is-epic {f = f} {g = g} equ equalises h i p =
    h                            ≡⟨ unique p ⟩
    universal (extendr coequal) ≡˘⟨ unique refl ⟩
    i                            ∎
    where open is-coequaliser equalises

  coequaliser-unique
    : ∀ {E E'} {c1 : Hom A E} {c2 : Hom A E'}
    → is-coequaliser C f g c1
    → is-coequaliser C f g c2
    → E ≅ E'
  coequaliser-unique {c1 = c1} {c2} co1 co2 =
    make-iso
      (co1 .universal {e' = c2} (co2 .coequal))
      (co2 .universal {e' = c1} (co1 .coequal))
      (unique₂ co2 (co2 .coequal) (pullr (co2 .factors) ∙ co1 .factors) (idl _))
      (unique₂ co1 (co1 .coequal) (pullr (co1 .factors) ∙ co2 .factors) (idl _))
    where open is-coequaliser

Categories with all coequalisers🔗

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

record Coequalisers {o ℓ} (C : Precategory o ℓ) : Type (o ⊔ ℓ) where
  no-eta-equality
  open Cat.Reasoning C
  field
    Coequ : ∀ {X Y} → Hom X Y → Hom X Y → Ob
    coequ : ∀ {X Y} → (f g : Hom X Y) → Hom Y (Coequ f g)
    coequal : ∀ {X Y} {f g : Hom X Y} → coequ f g ∘ f ≡ coequ f g ∘ g
    coequalise
      : ∀ {E X Y} {f g : Hom X Y}
      → (e' : Hom Y E)
      → e' ∘ f ≡ e' ∘ g
      → Hom (Coequ f g) E
    coequalise∘coequ
      : ∀ {E X Y} {f g : Hom X Y}
      → {e : Hom Y E} {p : e ∘ f ≡ e ∘ g}
      → coequalise e p ∘ coequ f g ≡ e
    coequalise-unique
      : ∀ {E X Y} {f g : Hom X Y}
      → {e : Hom Y E} {p : e ∘ f ≡ e ∘ g}
      → {other : Hom (Coequ f g) E}
      → other ∘ coequ f g ≡ e
      → other ≡ coequalise e p