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

import Cat.Reasoning

module Cat.Diagram.Coequaliser.RegularEpi where

module _ {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 expresses as βa union of parts of possibly glued togetherβ.

The definition is also precisely dual: A map is a regular epimorphism if it is the coequaliser of some pair of arrows

  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 _ 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 may coequalise: Its kernel pair, that is, the pullback of 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 exists, then is also an effective epimorphism.

module _ {o β} {C : Precategory o β} where
open Cat.Reasoning C
private variable a b : Ob

  is-regular-epiβis-effective-epi
: β {a b} {f : Hom a b}
β Pullback C f f
β is-regular-epi C f
β is-effective-epi C 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 C 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