open import Cat.Diagram.Pullback.Properties open import Cat.Instances.Sets.Complete open import Cat.Morphism.Factorisation open import Cat.Morphism.StrongEpi open import Cat.Diagram.Pullback open import Cat.Instances.Sets open import Cat.Prelude open import Cat.Regular open import Data.Set.Surjection module Cat.Regular.Instances.Sets where

# Sets is regularπ

We can prove that the category of
$Sets$
is regular by investigating the relationship between surjections,
regular epimorphisms, and arbitrary epimorphisms. Fortunately, they
*all* coincide, and we already know that
$Sets$
is finitely
complete, so it only remains to show that morphisms have an epi-mono
factorisation, and that epimorphy is stable under pullbacks.

Sets-regular : β {β} β is-regular (Sets β) Sets-regular .has-is-lex = Sets-finitely-complete

For the factorisation, we go with the pre-existing notion of `image`

, not only because weβre
trying to compute an *image* factorisation, but because there is
a natural surjection
$aβim(f)$
and an embedding
$im(f)βͺb.$

Sets-regular .factor {a} {b} f = Ξ» where .mediating β el! (image f) .mediate x β (f x) , inc (x , refl) .forget β fst .mediateβE β inc (is-regular-epiβis-strong-epi (Sets _) {a} {el! (image f)} _ (surjectiveβregular-epi _ _ _ Ξ» { (x , y) β β₯-β₯-rec squash (Ξ» { (pre , p) β inc (pre , Ξ£-prop-path! p) }) y })) .forgetβM β inc (embeddingβmonic (Subset-proj-embedding (Ξ» _ β squash))) .factors β refl

It additionally suffices to verify this only for our choice of pullbacks (rather than arbitrary pullback squares), for which the following calculation does perfectly:

Sets-regular .stable = canonically-stable (Ξ» {a} {b} β is-strong-epi (Sets _) {a} {b}) Sets-is-category Sets-pullbacks Ξ» {a} {b} {c} f g (f-epi , _) β let remβ : is-surjective f remβ = epiβsurjective a b f Ξ» {c} β f-epi {c} T : Set _ T = Sets-pullbacks {A = c} {a} {b} g f .Pullback.apex pb : β£ T β£ β β£ c β£ pb = Sets-pullbacks {A = c} {a} {b} g f .Pullback.pβ remβ : is-surjective pb remβ x = do (f^*fx , p) β remβ (g x) pure ((x , f^*fx , sym p) , refl) in is-regular-epiβis-strong-epi (Sets _) {a = el! _} {c} _ (surjectiveβregular-epi _ _ _ remβ)