Split Surjectivity (#499)

# Description

Pulling some of my changes out of #375 in hopes of getting back to it at
some point. This PR defines split surjectivity, and also proves some
misc. lemmas about surjective maps. I've done some minor cleanup in some
of the base modules, and added some (hopefully useful!) equivalences.

## Checklist

Before submitting a merge request, please check the items below:

- [x] I've read [the contributing
guidelines](https://github.com/plt-amy/1lab/blob/main/CONTRIBUTING.md).
- [x] The imports of new modules have been sorted with
`support/sort-imports.hs` (or `nix run --experimental-features
nix-command -f . sort-imports`).
- [x] All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content,
and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title
with `chore:`.

Author: TOTBWF

src/1Lab/Classical.lagda.md

@@ -122,7 +122,7 @@ Surjections-split =
   ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → is-set A → is-set B
   → (f : A → B)
   → is-surjective f
-  → ∥ (∀ b → fibre f b) ∥
+  → is-split-surjective f
 ```
 
 We show that these two statements are logically equivalent^[they are also

src/1Lab/Equiv.lagda.md

@@ -71,8 +71,9 @@ Here in the 1Lab, we formalise three acceptable notions of equivalence:
 <!--
 ```agda
 private variable
-  ℓ₁ ℓ₂ : Level
-  A A' B B' C : Type ℓ₁
+  ℓ ℓ₁ ℓ₂ : Level
+  A A' B B' C : Type ℓ
+  P : A → Type ℓ
 ```
 -->
 
@@ -1094,6 +1095,58 @@ infix  3 _≃∎
 infix 21 _≃_
 
 syntax ≃⟨⟩-syntax x q p = x ≃⟨ p ⟩ q
+```
+-->
+
+## Some useful equivalences
+
+We can extend `subst`{.Agda} to an equivalence between `Σ[ y ∈ A ] (y ≡ x × P y)`
+and `P x` for every `x : A` and `P : A → Type`. In informal mathematical practice,
+applying this equivalence is sometimes called "contracting $y$ away", alluding to
+the [[contractibility of singletons]].
+
+```agda
+subst≃
+  : (x : A) → (Σ[ y ∈ A ] (y ≡ x × P y)) ≃ P x
+subst≃ {A = A} {P = P} x = Iso→Equiv (to , iso from invr invl)
+  where
+    to : Σ[ y ∈ A ] (y ≡ x × P y) → P x
+    to (y , y=x , py) = subst P y=x py
+
+    from : P x → Σ[ y ∈ A ] (y ≡ x × P y)
+    from px = x , refl , px
+
+    invr : is-right-inverse from to
+    invr = transport-refl
+
+    invl : is-left-inverse from to
+    invl (y , y=x , py) i =
+      (y=x (~ i)) ,
+      (λ j → y=x (~ i ∨ j)) ,
+      transp (λ j → P (y=x (~ i ∧ j))) i py
+```
+
+<!--
+```agda
+is-equiv≃fibre-is-contr
+  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
+  → {f : A → B}
+  → is-equiv f ≃ (∀ x → is-contr (fibre f x))
+is-equiv≃fibre-is-contr {f = f} =
+  prop-ext
+    (is-equiv-is-prop f)
+    (λ f g i x → is-contr-is-prop (f x) (g x) i)
+    is-eqv
+    (λ fib-contr → record { is-eqv = fib-contr })
+
+-- This ideally would go in 1Lab.HLevel, but we don't have equivalences
+-- defined that early in the bootrapping process.
+is-prop→is-contr-iff-inhabited
+  : ∀ {ℓ} {A : Type ℓ}
+  → is-prop A
+  → is-contr A ≃ A
+is-prop→is-contr-iff-inhabited A-prop =
+  prop-ext is-contr-is-prop A-prop centre (is-prop∙→is-contr A-prop)
 
 lift-inj
   : ∀ {ℓ ℓ'} {A : Type ℓ} {a b : A}

src/1Lab/Function/Surjection.lagda.md

@@ -4,7 +4,10 @@ open import 1Lab.Function.Embedding
 open import 1Lab.Reflection.HLevel
 open import 1Lab.HLevel.Closure
 open import 1Lab.Truncation
+open import 1Lab.Type.Sigma
+open import 1Lab.Univalence
 open import 1Lab.Inductive
+open import 1Lab.Type.Pi
 open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path
@@ -22,8 +25,10 @@ module 1Lab.Function.Surjection where
 <!--
 ```agda
 private variable
-  ℓ ℓ' : Level
+  ℓ ℓ' ℓ'' : Level
   A B C : Type ℓ
+  P Q : A → Type ℓ'
+  f g : A → B
 ```
 -->
 
@@ -95,6 +100,19 @@ is-equiv→is-surjective : {f : A → B} → is-equiv f → is-surjective f
 is-equiv→is-surjective eqv x = inc (eqv .is-eqv x .centre)
 ```
 
+Surjections also are closed under a weaker form of [[two-out-of-three]]:
+if $f \circ g$ is surjective, then $f$ must also be surjective.
+
+```agda
+is-surjective-cancelr
+  : {f : B → C} {g : A → B}
+  → is-surjective (f ∘ g)
+  → is-surjective f
+is-surjective-cancelr {g = g} fgs c = do
+  (fg*x , p) ← fgs c
+  pure (g fg*x , p)
+```
+
 <!--
 ```agda
 Equiv→Cover : A ≃ B → A ↠ B
@@ -140,3 +158,241 @@ injective-surjective→is-equiv! =
   injective-surjective→is-equiv (hlevel 2)
 ```
 -->
+
+## Surjectivity and images
+
+A map $f : A \to B$ is surjective if and only if the inclusion of the
+image of $f$ into $B$ is an [[equivalence]].
+
+```agda
+surjective-iff-image-equiv
+  : ∀ {f : A → B}
+  → is-surjective f ≃ is-equiv {A = image f} fst
+```
+
+First, note that the fibre of the inclusion of the image of $f$ at $b$
+is the [[propositional truncation]] of the fibre of $f$ at $b$, by
+construction. Asking for this inclusion to be an equivalence is the same as
+asking for those fibres to be [[contractible]], which thus amounts to
+asking for the fibres of $f$ to be [[merely]] inhabited, which is the
+definition of $f$ being surjective.
+
+```agda
+surjective-iff-image-equiv {A = A} {B = B} {f = f} =
+  Equiv.inverse $
+    is-equiv fst                            ≃⟨ is-equiv≃fibre-is-contr ⟩
+    (∀ b → is-contr (fibre fst b))          ≃⟨ Π-ap-cod (λ b → is-hlevel-ap 0 (Fibre-equiv _ _)) ⟩
+    (∀ b → is-contr (∃[ a ∈ A ] (f a ≡ b))) ≃⟨ Π-ap-cod (λ b → is-prop→is-contr-iff-inhabited (hlevel 1)) ⟩
+    (∀ b → ∃[ a ∈ A ] (f a ≡ b))            ≃⟨⟩
+    is-surjective f                         ≃∎
+```
+
+# Split surjective functions
+
+:::{.definition #surjective-splitting}
+A **surjective splitting** of a function $f : A \to B$ consists of a designated
+element of the fibre $f^*b$ for each $b : B$.
+:::
+
+```agda
+surjective-splitting : (A → B) → Type _
+surjective-splitting f = ∀ b → fibre f b
+```
+
+Note that unlike "being surjective", a surjective splitting of $f$ is a *structure*
+on $f$, not a property. This difference becomes particularly striking when we
+look at functions into [[contractible]] types: if $B$ is contractible,
+then the type of surjective splittings of a function $f : A \to B$ is equivalent to $A$.
+
+```agda
+private
+  split-surjective-is-structure
+    : (f : A → B)
+    → is-contr B
+    → surjective-splitting f ≃ A
+```
+
+First, recall that dependent functions $(a : A) \to B(a)$ out of a contractible type are
+equivalent to an element of $B$ at the centre of contraction, so $(b : B) \to f^*(b)$ is
+equivalent to an element of the fibre of $f$ at the centre of contraction of $B$. Moreover,
+the type of paths in $B$ is also contractible, so that fibre is equivalent to $A$.
+
+```agda
+  split-surjective-is-structure {A = A} f B-contr =
+    (∀ b → fibre f b)         ≃⟨ Π-contr-eqv B-contr ⟩
+    fibre f (B-contr .centre) ≃⟨ Σ-contr-snd (λ _ → Path-is-hlevel 0 B-contr) ⟩
+    A                         ≃∎
+```
+
+In light of this, we provide the following definition.
+
+:::{.definition #split-surjective}
+A function $f : A \to B$ is **split surjective** if there merely exists a
+surjective splitting of $f$.
+:::
+
+```agda
+is-split-surjective : (A → B) → Type _
+is-split-surjective f = ∥ surjective-splitting f ∥
+```
+
+Every split surjective map is surjective.
+
+```agda
+is-split-surjective→is-surjective : is-split-surjective f → is-surjective f
+is-split-surjective→is-surjective f-split-surj b = do
+  f-splitting ← f-split-surj
+  pure (f-splitting b)
+```
+
+Note that we do not have a converse to this constructively: the statement that
+every surjective function between [[sets]] splits is [[equivalent to the axiom of choice|axiom-of-choice]]!
+
+## Split surjective functions and sections
+
+The type of surjective splittings of a function $f : A \to B$ is equivalent
+to the type of sections of $f$, i.e. functions $s : B \to A$ with $f \circ s = \id$.
+
+```agda
+section≃surjective-splitting
+  : (f : A → B)
+  → (Σ[ s ∈ (B → A) ] is-right-inverse s f) ≃ surjective-splitting f
+```
+
+Somewhat surprisingly, this is an immediate consequence of the fact that
+sigma types distribute over pi types!
+
+```agda
+section≃surjective-splitting {A = A} {B = B} f =
+  (Σ[ s ∈ (B → A) ] ((x : B) → f (s x) ≡ x)) ≃˘⟨ Σ-Π-distrib ⟩
+  ((b : B) → Σ[ a ∈ A ] f a ≡ b)             ≃⟨⟩
+  surjective-splitting f                     ≃∎
+```
+
+This means that a function $f$ is split surjective if and only if there
+[[merely]] exists some section of $f$.
+
+```agda
+exists-section-iff-split-surjective
+  : (f : A → B)
+  → (∃[ s ∈ (B → A) ] is-right-inverse s f) ≃ is-split-surjective f
+exists-section-iff-split-surjective f =
+  ∥-∥-ap (section≃surjective-splitting f)
+```
+
+## Closure properties of split surjective functions
+
+Like their non-split counterparts, split surjective functions are closed under composition.
+
+```agda
+∘-surjective-splitting : ∘-closed surjective-splitting
+∘-is-split-surjective : ∘-closed is-split-surjective
+```
+
+<details>
+<summary> The proof is essentially identical to the non-split case.
+</summary>
+
+```agda
+∘-surjective-splitting {f = f} f-split g-split c =
+  let (f*c , p) = f-split c
+      (g*f*c , q) = g-split f*c
+  in g*f*c , ap f q ∙ p
+
+∘-is-split-surjective fs gs = ⦇ ∘-surjective-splitting fs gs ⦈
+```
+</details>
+
+Every equivalence can be equipped with a surjective splitting, and
+is thus split surjective.
+
+```agda
+is-equiv→surjective-splitting
+  : is-equiv f
+  → surjective-splitting f
+
+is-equiv→is-split-surjective
+  : is-equiv f
+  → is-split-surjective f
+```
+
+This follows immediately from the definition of equivalences: if the
+type of fibres is contractible, then we can pluck the element we need
+out of the centre of contraction!
+
+```agda
+is-equiv→surjective-splitting f-equiv b =
+  f-equiv .is-eqv b .centre
+
+is-equiv→is-split-surjective f-equiv =
+  pure (is-equiv→surjective-splitting f-equiv)
+```
+
+Split surjective functions also satisfy left two-out-of-three.
+
+```agda
+surjective-splitting-cancelr
+  : surjective-splitting (f ∘ g)
+  → surjective-splitting f
+
+is-split-surjective-cancelr
+  : is-split-surjective (f ∘ g)
+  → is-split-surjective f
+```
+
+<details>
+<summary>These proofs are also essentially identical to the non-split versions.
+</summary>
+
+```agda
+surjective-splitting-cancelr {g = g} fg-split c =
+  let (fg*c , p) = fg-split c
+  in g fg*c , p
+
+is-split-surjective-cancelr fg-split =
+  map surjective-splitting-cancelr fg-split
+```
+</details>
+
+A function is an equivalence if and only if it is a split-surjective
+[[embedding]].
+
+```agda
+embedding-split-surjective≃is-equiv
+  : {f : A → B}
+  → (is-embedding f × is-split-surjective f) ≃ is-equiv f
+embedding-split-surjective≃is-equiv {f = f} =
+  prop-ext!
+    (λ (f-emb , f-split-surj) →
+      embedding-surjective→is-equiv
+        f-emb
+        (is-split-surjective→is-surjective f-split-surj))
+    (λ f-equiv → is-equiv→is-embedding f-equiv , is-equiv→is-split-surjective f-equiv)
+```
+
+# Surjectivity and connectedness
+
+If $f : A \to B$ is a function out of a [[contractible]] type $A$,
+then $f$ is surjective if and only if $B$ is a [[pointed connected type]], where
+the basepoint of $B$ is given by $f$ applied to the centre of contraction of $A$.
+
+```agda
+contr-dom-surjective-iff-connected-cod
+  : ∀ {f : A → B}
+  → (A-contr : is-contr A)
+  → is-surjective f ≃ ((x : B) → ∥ x ≡ f (A-contr .centre) ∥)
+```
+
+To see this, note that the fibre of $f$ over $x$ is equivalent
+to the type of paths $x = f(a_{\bullet})$, where $a_{\bullet}$ is the centre
+of contraction of $A$.
+
+```agda
+contr-dom-surjective-iff-connected-cod {A = A} {B = B} {f = f} A-contr =
+  Π-ap-cod (λ b → ∥-∥-ap (Σ-contr-fst A-contr ∙e sym-equiv))
+```
+
+This correspondence is not a coincidence: surjective maps fit into
+a larger family of maps known as [[connected maps]]. In particular,
+a map is surjective exactly when it is (-1)-connected, and this lemma is
+a special case of `is-n-connected-point`{.Agda}.

src/1Lab/HLevel.lagda.md

@@ -730,6 +730,13 @@ SinglP-is-contr A a .paths (x , p) i = _ , λ j → fill A (∂ i) j λ where
 SinglP-is-prop : ∀ {ℓ} {A : I → Type ℓ} {a : A i0} → is-prop (SingletonP A a)
 SinglP-is-prop = is-contr→is-prop (SinglP-is-contr _ _)
 
+Single-is-contr : ∀ {x : A} → is-contr (Singleton x)
+Single-is-contr {x = x} .centre = x , refl
+Single-is-contr {x = x} .paths (y , p) i = p i , λ j → p (i ∧ j)
+
+Single-is-contr' : ∀ {x : A} → is-contr (Σ[ y ∈ A ] y ≡ x)
+Single-is-contr' {x = x} .centre = x , refl
+Single-is-contr' {x = x} .paths (y , p) i = p (~ i) , λ j → p (~ i ∨ j)
 
 is-prop→squarep
   : ∀ {B : I → I → Type ℓ} → ((i j : I) → is-prop (B i j))

src/1Lab/Truncation.lagda.md

@@ -12,6 +12,7 @@ open import 1Lab.HLevel.Closure
 open import 1Lab.Path.Reasoning
 open import 1Lab.Type.Sigma
 open import 1Lab.Inductive
+open import 1Lab.Type.Pi
 open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path