open import Cat.Diagram.Pullback.Properties
open import Cat.Instances.Sets.Complete
open import Cat.Morphism.Factorisation
open import Cat.Morphism.Strong.Epi
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🔗

open Factorisation
open is-regular

We can prove that the category of $\mathbf{Sets}$ is regular by investigating the relationship between surjections, regular epimorphisms, and arbitrary epimorphisms. Fortunately, they all coincide, and we already know that $\mathbf{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\twoheadrightarrow \mathrm{im}(f)$ and an embedding $\mathrm{im}(f)\hookrightarrow b\text{.}$

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₂)