open import Cat.Diagram.Coequaliser
open import Cat.Diagram.Pullback
open import Cat.Diagram.Initial
open import Cat.Prelude

import Cat.Reasoning

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

Regular epimorphismsπŸ”—

Dually to regular monomorphisms, which behave as embeddings, regular epimorphisms behave like covers: A regular epimorphism f:aβ† bf : a \epi b expresses bb as β€œa union of parts of aa, possibly glued together.”

The definition is also precisely dual: A map f:aβ†’bf : a \to b is a regular epimorphism if it is the coequaliser of some pair of arrows R⇉aR \tto a.

record is-regular-epi (f : Hom a b) : Type (o βŠ” β„“) where
  no-eta-equality
  constructor reg-epi
  field
    {r}           : Ob
    {arr₁} {arrβ‚‚} : Hom r a
    has-is-coeq   : is-coequaliser C arr₁ arrβ‚‚ f

  open is-coequaliser has-is-coeq public

From the definition we can directly conclude that regular epis are in fact epic:

  is-regular-epi→is-epic : is-epic f
  is-regular-epi→is-epic = is-coequaliser→is-epic C _ has-is-coeq

open is-regular-epi using (is-regular-epi→is-epic) public

Effective episπŸ”—

Again by duality, we have a pair of canonical choices of maps which ff may coequalise: Its kernel pair, that is, the pullback of ff along itself. An epimorphism which coequalises its kernel pair is called an effective epi, and effective epis are immediately seen to be regular epis:

record is-effective-epi (f : Hom a b) : Type (o βŠ” β„“) where
  no-eta-equality
  field
    {kernel}       : Ob
    p₁ pβ‚‚          : Hom kernel a
    is-kernel-pair : is-pullback C p₁ f pβ‚‚ f
    has-is-coeq    : is-coequaliser C p₁ pβ‚‚ f

  is-effective-epi→is-regular-epi : is-regular-epi f
  is-effective-epi→is-regular-epi = re where
    open is-regular-epi hiding (has-is-coeq)
    re : is-regular-epi f
    re .r = _
    re .arr₁ = _
    re .arrβ‚‚ = _
    re .is-regular-epi.has-is-coeq = has-is-coeq

If a regular epimorphism (a coequaliser) has a kernel pair, then it is also the coequaliser of its kernel pair. That is: If the pullback of aβ†’fb←faa \xto{f} b \xot{f} a exists, then ff is also an effective epimorphism.

is-regular-epi→is-effective-epi
  : βˆ€ {a b} {f : Hom a b}
  β†’ Pullback C f f
  β†’ is-regular-epi f
  β†’ is-effective-epi f
is-regular-epi→is-effective-epi {f = f} kp reg = eff where
  module reg = is-regular-epi reg
  module kp = Pullback kp

  open is-effective-epi
  open is-coequaliser
  eff : is-effective-epi f
  eff .kernel = kp.apex
  eff .p₁ = kp.p₁
  eff .pβ‚‚ = kp.pβ‚‚
  eff .is-kernel-pair = kp.has-is-pb
  eff .has-is-coeq .coequal = kp.square
  eff .has-is-coeq .coequalise {F = F} {eβ€²} p = reg.coequalise q where
    q : eβ€² ∘ reg.arr₁ ≑ eβ€² ∘ reg.arrβ‚‚
    q =
      eβ€² ∘ reg.arr₁                               β‰‘βŸ¨ ap (eβ€² ∘_) (sym kp.pβ‚‚βˆ˜limiting) βŸ©β‰‘
      eβ€² ∘ kp.pβ‚‚ ∘ kp.limiting (sym reg.coequal)  β‰‘βŸ¨ pulll (sym p) βŸ©β‰‘
      (eβ€² ∘ kp.p₁) ∘ kp.limiting _                β‰‘βŸ¨ pullr kp.pβ‚βˆ˜limiting βŸ©β‰‘
      eβ€² ∘ reg.arrβ‚‚                               ∎
  eff .has-is-coeq .universal = reg.universal
  eff .has-is-coeq .unique = reg.unique