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 \twoheadrightarrow 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 \rightrightarrows 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 \xrightarrow{f} b \xleftarrow{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 = epi where
  module reg = is-regular-epi reg
  module kp = Pullback kp

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