open import Cat.Diagram.Coequaliser.RegularEpi open import Cat.Diagram.Coequaliser open import Cat.Prelude import Cat.Reasoning as Cr module Data.Set.Surjection where

Here we prove that surjective maps are exactly the regular
epimorphisms in the category of sets: Really, we prove that
surjections are regular epimorphisms (this is straightforward), then we
prove that every epimorphism is a
surjection (this takes a detour). Putting these together, we get
*every epimorphism is regular* as a corollary.

## Surjections are epic🔗

This is the straightforward direction: We know (since
${{\mathbf{Sets}}}$
has pullbacks) that if a morphism is going to be a regular epimorphism,
then it must be an *effective* epimorphism, too: so if it is to
coequalise any morphisms, it certainly coequalises its kernel pair.

surjective→regular-epi : ∀ {ℓ} (c d : n-Type ℓ 2) (f : ∣ c ∣ → ∣ d ∣) → (∀ x → ∥ fibre f x ∥) → is-regular-epi (Sets ℓ) {c} {d} f surjective→regular-epi c _ f x .r = el! (Σ ∣ c ∣ λ x → Σ ∣ c ∣ λ y → f x ≡ f y) surjective→regular-epi _ _ f x .arr₁ = λ (y , _ , _) → y surjective→regular-epi _ _ f x .arr₂ = λ (_ , y , _) → y

That’s our choice of cofork: it remains to show that $f$ coequalises this. Given any map $e' : c \to F$, element $x : d$, mere fibre $f^*(x)$, and proof $p$ that $e'$ is constant on the kernel pair of $f$ (i.e. that it also coequalises the kernel pair cofork), we can construct an element of $F$: since $e'$ is suitably constant, we can use the elimination principle for $\| f^*x \| \to F$, since $F$ is a set.

surjective→regular-epi c d f surj .has-is-coeq = coeqs where go : ∀ {F} (e′ : ∣ c ∣ → ∣ F ∣) p (x : ∣ d ∣) → ∥ fibre f x ∥ → ∣ F ∣ go e′ p x = ∥-∥-rec-set (λ x → e′ (x .fst)) (λ x y → p $ₚ (x .fst , y .fst , x .snd ∙ sym (y .snd))) hlevel!

After a small amount of computation to move the witnesses of surjectivity out of the way, we get what we wanted.

coeqs : is-coequaliser (Sets _) _ _ _ coeqs .coequal i (x , y , p) = p i coeqs .coequalise {F} {e′} p x = go {F = F} e′ p x (surj x) coeqs .universal {F} {e′} {p = p} = funext λ x → ∥-∥-elim {P = λ e → go {F} e′ p (f x) e ≡ e′ x} (λ x → hlevel!) (λ e → p $ₚ (e .fst , x , e .snd)) (surj (f x)) coeqs .unique {F} {e′} {p} {colim} comm = funext λ a → ∥-∥-elim {P = λ e → colim a ≡ go {F} e′ p a e} (λ x → hlevel!) (λ x → sym (comm $ₚ x .fst ∙ ap colim (x .snd))) (surj a)

# Epis are surjective🔗

Now *this* is the hard direction. Our proof follows (Rijke and
Spitters 2015, sec. 2.9), so if the exposition below doesn’t
make a lot of sense, be sure to check their paper, too. We define a
higher inductive type standing for the *cofibre* of
$f$,
also known as the *mapping cone*. Strictly speaking, this is the
homotopy pushout

but Cubical Agda makes it very convenient to define a purpose-built HIT in-line. We use the names “tip”, “base”, and “cone” to evoke the construction of a cone in solid geometry: the tip is.. the tip, the base is the circle, and the cone is the triangular side which we have rotated around the vertical axis.

data Cofibre {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} (f : A → B) : Type (ℓ ⊔ ℓ′) where tip : Cofibre f base : B → Cofibre f cone : ∀ a → tip ≡ base (f a)

What’s important here is that if a map
$f$
has connected cofibre, then it is a surjection — so our proof that epis
are surjective will factor through showing that epis have connected
cofibres^{1}.

connected-cofibre→surjective : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} (f : A → B) → is-contr ∥ Cofibre f ∥₀ → ∀ x → ∥ fibre f x ∥ connected-cofibre→surjective {A = A} {B = B} f conn x = transport cen (lift tt) where

We define a family $P$ of propositions over ${\mathrm{Cofibre}}(f)$ which maps tip to the unit proposition and the base point with coordinate $x$ to the fibre $f^x$. Since ${\mathrm{Prop}}$ is a set, $P$ extends to a map $P' : \| {\mathrm{Cofibre}}(f) \|_0 \to {\mathrm{Prop}}$.

P : Cofibre f → Prop _ P tip = el (Lift _ ⊤) hlevel! P (base x) = el ∥ fibre f x ∥ hlevel! P (cone a i) = n-ua {X = el (Lift _ ⊤) hlevel!} {Y = el ∥ fibre f (f a) ∥ hlevel!} (prop-ext hlevel! hlevel! (λ _ → inc (a , refl)) λ _ → lift tt) i P′ : ∥ Cofibre f ∥₀ → Prop _ P′ = ∥-∥₀-elim (λ _ → hlevel!) P

Letting $x$ be an element of the codomain, and since by assumption $f$’s cofibre is connected, we have a path

$\top = P'({\mathrm{tip}}) = P'({\mathrm{base}}_x) = \| f^x \|\text{,}$

so since the unit type is trivially inhabited, so is the fibre of $f$ over $x$: $f$ is surjective.

cen : Lift _ ⊤ ≡ ∥ fibre f x ∥ cen = ap ∣_∣ (ap P′ (is-contr→is-prop conn (inc tip) (inc (base x))))

## Epis have connected cofibre🔗

Now suppose that
$f$
is an epic morphism ^{2} ^{3}. We know that the
set-truncation of
$f$’s
cofibre is inhabited (since every cofibre is inhabited), so it remains
to show that any two points are merely equal.

epi→connected-cofibre : ∀ {ℓ} (c d : n-Type ℓ 2) (f : ∣ c ∣ → ∣ d ∣) → Cr.is-epic (Sets ℓ) {c} {d} f → is-contr ∥ Cofibre f ∥₀ epi→connected-cofibre c d f epic = contr (inc tip) $ ∥-∥₀-elim (λ _ → is-prop→is-set (squash _ _)) λ w → ∥-∥₀-path.from (hom w) where

Let $x : d$ — we’ll show that $\| {\mathrm{tip}} = {\mathrm{base}}_x \|$. Here’s where we $f$’s epimorphy: we have a homotopy $| {\mathrm{tip}} | = | {\mathrm{base}}_{(f x)} |$, namely the cone — and since we can write its left-hand-side as the composition of $f$ with a constant function, $f$ gives us a path $| {\mathrm{tip}} | = | {\mathrm{base}}_x |$ — which, by the characterisation of paths in the set truncation, means we merely have $\| {\mathrm{tip}} = {\mathrm{base}}_x \|$.

go : ∀ x → ∥ tip ≡ base x ∥ go x = ∥-∥₀-path.to (p $ₚ x) where p = epic {c = el ∥ Cofibre f ∥₀ squash} (λ _ → inc tip) (λ x → inc (base x)) (funext λ x → ap ∥_∥₀.inc (cone x))

An appeal to induction over the cofibre completes the proof: Epimorphisms have connected cofibres. Note that the path case is discharged automatically since we’re mapping into a proposition.

hom : ∀ w → ∥ tip ≡ w ∥ hom tip = inc refl hom (base x) = go x hom (cone a i) = is-prop→pathp (λ i → ∥_∥.squash {A = tip ≡ cone a i}) (inc refl) (go (f a)) i

And, composing this with the previous step, we have what we originally set out to prove: all ${{\mathbf{Sets}}}$-epimorphisms are regular, because they’re all surjections!

epi→surjective : ∀ {ℓ} (c d : n-Type ℓ 2) (f : ∣ c ∣ → ∣ d ∣) → Cr.is-epic (Sets ℓ) {c} {d} f → ∀ x → ∥ fibre f x ∥ epi→surjective {ℓ} c d f epi x = connected-cofibre→surjective f (epi→connected-cofibre c d f (λ {x} → epi {x})) x

## References

- Rijke, Egbert, and Bas Spitters. 2015. “Sets in Homotopy Type
Theory.”
*Mathematical Structures in Computer Science*25 (5): 1172–202. https://doi.org/10.1017/s0960129514000553.