open import Cat.Diagram.Coequaliser.RegularEpi
open import Cat.Diagram.Coequaliser
open import Cat.Morphism.StrongEpi
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


# Surjections between sets🔗

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 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 ∣)
→ is-surjective f
→ 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 coequalises this. Given any map element mere fibre and proof that is constant on the kernel pair of (i.e. that it also coequalises the kernel pair cofork), we can construct an element of since is suitably constant, we can use the elimination principle for since 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 2) (λ 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 1) (λ 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 1)
(λ x → ap colim (sym (x .snd)) ∙ comm $ₚ x .fst) (surj a)  surjective→strong-epi : ∀ {ℓ} (c d : n-Type ℓ 2) (f : ∣ c ∣ → ∣ d ∣) → is-surjective f → is-strong-epi (Sets ℓ) {c} {d} f surjective→strong-epi c d f f-surj = is-regular-epi→is-strong-epi (Sets _) f$
surjective→regular-epi c d f f-surj

surjective→epi
: ∀ {ℓ} (c d : n-Type ℓ 2) (f : ∣ c ∣ → ∣ d ∣)
→ is-surjective f
→ Cr.is-epic (Sets ℓ) {c} {d} f
surjective→epi c d f surj {c = x} =
is-regular-epi→is-epic (surjective→regular-epi c d f surj) {c = x}


# 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 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 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)
→ is-surjective f
connected-cofibre→surjective {A = A} {B = B} f conn x = transport cen (lift tt) where


We define a family of propositions over which maps tip to the unit proposition and the base point with coordinate to the fibre Since is a set, extends to a map

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

P' : ∥ Cofibre f ∥₀ → Prop _
P' = ∥-∥₀-elim (λ _ → hlevel 2) P


Letting be an element of the codomain, and since by assumption cofibre is connected, we have a path

so since the unit type is trivially inhabited, so is the fibre of over 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 is an epic morphism 2 3. We know that the set-truncation of 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 — we’ll show that Here’s where we use epimorphy: we have a homotopy namely the cone — and since we can write its left-hand-side as the composition of with a constant function, gives us a path — which, by the characterisation of paths in the set truncation, means we merely have  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 are regular, because they’re all surjections!

epi→surjective
: ∀ {ℓ} (c d : n-Type ℓ 2) (f : ∣ c ∣ → ∣ d ∣)
→ Cr.is-epic (Sets ℓ) {c} {d} f
→ is-surjective f
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↩︎