open import Cat.Prelude

module Cat.Diagram.Coequaliser {o β„“} (C : Precategory o β„“) where


open import Cat.Reasoning C
private variable
  A B : Ob
  f g h : Hom A B

CoequalisersπŸ”—

The coequaliser of two maps f,g:A→Bf, g : A \to B (if it exists), represents the largest quotient object of BB that identifies ff and gg.

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

is-coequaliser→is-epic
  : βˆ€ {E} (coequ : Hom A E)
  β†’ is-coequaliser 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 f g c1
  β†’ is-coequaliser 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