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

open Cat.Reasoning C
private variable a b : Ob


# Regular epimorphismsπ

Dually to regular monomorphisms, which behave as embeddings, regular epimorphisms behave like covers: A regular epimorphism $f : a \twoheadrightarrow b$ expresses $b$ as βa union of parts of $a$, possibly glued togetherβ.

The definition is also precisely dual: A map $f : a \to b$ is a regular epimorphism if it is the coequaliser of some pair of arrows $R \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 $f$ may coequalise: Its kernel pair, that is, the pullback of $f$ 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 \xrightarrow{f} b \xleftarrow{f} a$ exists, then $f$ 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