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 Sets\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.

  : ∀ {ℓ} (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 ff coequalises this. Given any map e′:c→Fe' : c \to F, element x:dx : d, mere fibre f∗(x)f^*(x), and proof pp that e′e' is constant on the kernel pair of ff (i.e. that it also coequalises the kernel pair cofork), we can construct an element of FF: since e′e' is suitably constant, we can use the elimination principle for ∥f∗x∥→F\| f^*x \| \to F, since FF 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)))

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 (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 ff, 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 ff has connected cofibre, then it is a surjection — so our proof that epis are surjective will factor through showing that epis have connected cofibres1.

  : ∀ {ℓ ℓ′} {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 PP of propositions over Cofibre(f)\mathrm{Cofibre}(f) which maps tip to the unit proposition and the base point with coordinate xx to the fibre fxf^x. Since Prop\mathrm{Prop} is a set, PP extends to a map P′:∥Cofibre(f)∥0→PropP' : \| \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 xx be an element of the codomain, and since by assumption ff’s cofibre is connected, we have a path

⊤=P′(tip)=P′(basex)=∥fx∥, \top = P'(\mathrm{tip}) = P'(\mathrm{base}_x) = \| f^x \|\text{,}

so since the unit type is trivially inhabited, so is the fibre of ff over xx: ff 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 ff is an epic morphism 2 3. We know that the set-truncation of ff’s cofibre is inhabited (since every cofibre is inhabited), so it remains to show that any two points are merely equal.

  : ∀ {ℓ} (c d : n-Type ℓ 2) (f : ∣ c ∣ → ∣ d ∣)
  → (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)

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

    go : ∀ x → ∥ tip ≡ base x ∥
    go x = ∥-∥₀ (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 Sets\mathbf{Sets}-epimorphisms are regular, because they’re all surjections!

  : ∀ {ℓ} (c d : n-Type ℓ 2) (f : ∣ c ∣ → ∣ d ∣)
  → (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↩︎