module Cat.Diagram.Coequaliser.RegularEpi where

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
    constructor reg-epi
      {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
      {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.

    : βˆ€ {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