open import Cat.Prelude

import Cat.Reasoning
module Cat.Diagram.Coequaliser where
module _ {o β„“} (C : Precategory o β„“) where
  open Cat.Reasoning C
  private variable
    A B : Ob
    f g h : Hom A B

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} {colim : Hom E F}
                 β†’ colim ∘ coeq ≑ e'
                 β†’ colim ≑ 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
      coeq      : Hom B coapex
      has-is-coeq : is-coequaliser f g coeq

    open is-coequaliser has-is-coeq public

Coequalisers are epicπŸ”—

Dually to the situation with equalisers, coequaliser arrows are always epic.

module _ {o β„“} {C : Precategory o β„“} where
  open Cat.Reasoning C
  private variable
    A B : Ob
    f g h : Hom A B
  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 module for working with categories that have coequalisers of all parallel pairs of morphisms.

has-coequalisers : βˆ€ {o β„“} β†’ Precategory o β„“ β†’ Type _
has-coequalisers C = βˆ€ {a b} (f g : Hom a b) β†’ Coequaliser C f g
  where open Precategory C

module Coequalisers
  {o β„“}
  (C : Precategory o β„“)
  (all-coequalisers : has-coequalisers C)
  where
  open Cat.Reasoning C
  module coequaliser {a b} (f g : Hom a b) = Coequaliser (all-coequalisers f g)

  Coequ : βˆ€ {a b} (f g : Hom a b) β†’ Ob
  Coequ = coequaliser.coapex