Split Surjectivity

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