open import Cat.Diagram.Coequaliser.RegularEpi
open import Cat.Diagram.Coequaliser
open import Cat.Prelude

open import Homotopy.Connectedness

import Cat.Reasoning as Cr

module Data.Set.Surjection where

open is-coequaliser
open is-regular-epi
open Coequaliser


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 hlevel! (λ x → e' (x .fst))
(λ x y → p $ₚ (x .fst , y .fst , x .snd ∙ sym (y .snd)))  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 .universal {F} {e'} p x = go {F = F} e' p x (surj x) coeqs .factors {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 → ap colim (sym (x .snd)) ∙ comm $ₚ x .fst) (surj a)  # Epis are surjective🔗 Now this is the hard direction. Our proof follows , 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 cofibres1. connected-cofibre→surjective : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) → is-connected (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-connected (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


1. note that all of these types are propositions, so we have a bunch of equivalences↩︎

2. by which we mean it is an epimorphism — it needn’t be like the Odyssey↩︎

3. and yes, we did write “an epic morphism” just to make the joke↩︎