diff --git a/src/1Lab/Classical.lagda.md b/src/1Lab/Classical.lagda.md
index 8e457f380..6407b053e 100644
--- a/src/1Lab/Classical.lagda.md
+++ b/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
diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md
index d71e53c1b..63d8d2919 100644
--- a/src/1Lab/Equiv.lagda.md
+++ b/src/1Lab/Equiv.lagda.md
@@ -71,8 +71,9 @@ Here in the 1Lab, we formalise three acceptable notions of equivalence:
 <!--
 ```agda
 private variable
-  ℓ₁ ℓ₂ : Level
+  ℓ ℓ₁ ℓ₂ : Level
   A B C : Type ℓ₁
+  P : A → Type ℓ
 ```
 -->
 
@@ -1087,6 +1088,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}
diff --git a/src/1Lab/Function/Surjection.lagda.md b/src/1Lab/Function/Surjection.lagda.md
index abf1aa928..660005af5 100644
--- a/src/1Lab/Function/Surjection.lagda.md
+++ b/src/1Lab/Function/Surjection.lagda.md
@@ -4,7 +4,10 @@ open import 1Lab.Function.Embedding
 open import 1Lab.Reflection.HLevel
 open import 1Lab.HIT.Truncation
 open import 1Lab.HLevel.Closure
+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
 ```
 -->
 
@@ -99,6 +104,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
@@ -144,3 +162,248 @@ 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))          ≃⟨ Π-cod≃ (λ b → is-hlevel-ap 0 (Fibre-equiv _ _)) ⟩
+    (∀ b → is-contr (∃[ a ∈ A ] (f a ≡ b))) ≃⟨ Π-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) ≃⟨ Σ-contract (λ _ → 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
+  : surjective-splitting f
+  → surjective-splitting g
+  → surjective-splitting (f ∘ g)
+
+∘-is-split-surjective
+  : is-split-surjective f
+  → is-split-surjective g
+  → is-split-surjective (f ∘ g)
+```
+
+<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 =
+  Π-cod≃ (λ b → ∥-∥-ap (Σ-contr-eqv 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}.
diff --git a/src/1Lab/HIT/Truncation.lagda.md b/src/1Lab/HIT/Truncation.lagda.md
index 53962a1b7..8c5c1bdca 100644
--- a/src/1Lab/HIT/Truncation.lagda.md
+++ b/src/1Lab/HIT/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
@@ -154,6 +155,13 @@ truncation extends to a functor:
 ∥-∥-map f (squash x y i) = squash (∥-∥-map f x) (∥-∥-map f y) i
 ```
 
+This means that propositional truncation preserves equivalences.
+
+```agda
+∥-∥-ap : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A ≃ B → ∥ A ∥ ≃ ∥ B ∥
+∥-∥-ap f = prop-ext! (∥-∥-map (Equiv.to f)) (∥-∥-map (Equiv.from f))
+```
+
 <!--
 ```agda
 ∥-∥-map₂ : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
diff --git a/src/1Lab/HLevel.lagda.md b/src/1Lab/HLevel.lagda.md
index d4d8cc647..72f57e983 100644
--- a/src/1Lab/HLevel.lagda.md
+++ b/src/1Lab/HLevel.lagda.md
@@ -694,6 +694,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))
diff --git a/src/1Lab/HLevel/Closure.lagda.md b/src/1Lab/HLevel/Closure.lagda.md
index 7ba31a220..0c299c3be 100644
--- a/src/1Lab/HLevel/Closure.lagda.md
+++ b/src/1Lab/HLevel/Closure.lagda.md
@@ -166,6 +166,18 @@ Equiv→is-hlevel : (n : Nat) → (B ≃ A) → is-hlevel A n → is-hlevel B n
 Equiv→is-hlevel n f = equiv→is-hlevel n _ (Equiv.inverse f .snd)
 ```
 
+<!--
+```agda
+is-hlevel-ap : ∀ n → A ≃ B → is-hlevel A n ≃ is-hlevel B n
+is-hlevel-ap n f =
+  prop-ext
+    (is-hlevel-is-prop n)
+    (is-hlevel-is-prop n)
+    (Equiv→is-hlevel n (f e⁻¹))
+    (Equiv→is-hlevel n f)
+```
+-->
+
 ## Functions into n-types
 
 We can now prove that the $n$-types are closed under all type formers
diff --git a/src/1Lab/Type/Sigma.lagda.md b/src/1Lab/Type/Sigma.lagda.md
index 85f77911a..f1ef51d9c 100644
--- a/src/1Lab/Type/Sigma.lagda.md
+++ b/src/1Lab/Type/Sigma.lagda.md
@@ -17,6 +17,7 @@ private variable
   ℓ ℓ₁ : Level
   A A' X X' Y Y' Z Z' : Type ℓ
   B P Q : A → Type ℓ
+  C : (x : A) → B x → Type ℓ
 ```
 -->
 
@@ -25,6 +26,26 @@ private variable
 This module contains properties of $\Sigma$ types, not necessarily
 organised in any way.
 
+## Universal property
+
+If we have a pair of maps $f : (x : A) \to B(x)$ and $g : (x : A) \to C(x, f(x))$,
+then there exists a unique universal map $\langle f , g \rangle : (x : A) \to \Sigma (B x) (C x)$
+that commutes with the projections. This is essentially a dependently
+typed version of the universal property of [[products]].
+
+```agda
+⟨_,_⟩ : (f : (x : A) → B x) → (g : (x : A) → C x (f x)) → (x : A) → Σ (B x) (C x)
+⟨ f , g ⟩ x = f x , g x
+
+⟨⟩-unique
+  : ∀ {f : (x : A) → B x} {g : (x : A) → C x (f x)}
+  → (h : (x : A) → Σ (B x) (C x))
+  → (p : fst ∘ h ≡ f)
+  → PathP (λ i → (x : A) → C x (p i x)) (snd ∘ h) g
+  → h ≡ ⟨ f , g ⟩
+⟨⟩-unique h p q i x = p i x , q i x
+```
+
 ## Groupoid structure
 
 The first thing we prove is that _paths in sigmas are sigmas of paths_.
@@ -121,19 +142,15 @@ they are included for completeness. </summary>
 Σ-assoc : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : (x : A) → B x → Type ℓ''}
         → (Σ[ x ∈ A ] Σ[ y ∈ B x ] C x y) ≃ (Σ[ x ∈ Σ _ B ] (C (x .fst) (x .snd)))
 Σ-assoc .fst (x , y , z) = (x , y) , z
-Σ-assoc .snd = is-iso→is-equiv λ where
-  .is-iso.from ((x , y) , z) → x , y , z
-  .is-iso.linv p → refl
-  .is-iso.rinv p → refl
+Σ-assoc .snd .is-eqv ((x , y), z) = contr (fib .fst) (fib .snd)
+  where fib = strict-fibres _ ((x , y) , z)
 
 Σ-Π-distrib : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : (x : A) → B x → Type ℓ''}
             → ((x : A) → Σ[ y ∈ B x ] C x y)
             ≃ (Σ[ f ∈ ((x : A) → B x) ] ((x : A) → C x (f x)))
-Σ-Π-distrib .fst f = (λ x → f x .fst) , λ x → f x .snd
-Σ-Π-distrib .snd = is-iso→is-equiv λ where
-  .is-iso.from (f , r) x → f x , r x
-  .is-iso.linv p → refl
-  .is-iso.rinv p → refl
+Σ-Π-distrib .fst f = (fst ∘ f) , (snd ∘ f)
+Σ-Π-distrib .snd .is-eqv (f , r) = contr (fib .fst) (fib .snd)
+  where fib = strict-fibres (λ h → ⟨ h .fst , h .snd ⟩) (f , r)
 ```
 </details>
 
@@ -252,9 +269,6 @@ If `B` is a family of contractible types, then `Σ B ≃ A`:
 Σ-map₂ : ({x : A} → P x → Q x) → Σ _ P → Σ _ Q
 Σ-map₂ f (x , y) = (x , f y)
 
-⟨_,_⟩ : (X → Y) → (X → Z) → X → Y × Z
-⟨ f , g ⟩ x = f x , g x
-
 ×-map : (A → A') → (X → X') → A × X → A' × X'
 ×-map f g (x , y) = (f x , g y)
 
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index 3312ed96d..14b868d32 100644
--- a/src/Cat/Prelude.agda
+++ b/src/Cat/Prelude.agda
@@ -12,7 +12,7 @@ open import 1Lab.Prelude
            ; _∘⟨_ to _⊙⟨_
            ; _⟩∘_ to _⟩⊙_
            )
-  hiding (id ; map ; _↠_ ; ⟨_,_⟩)
+  hiding (id ; map ; _↠_ ; ⟨_,_⟩; ⟨⟩-unique)
   public
 
 open import Data.Set.Truncation public
diff --git a/src/Data/Fin/Properties.lagda.md b/src/Data/Fin/Properties.lagda.md
index 17d90ba35..213f4d1b4 100644
--- a/src/Data/Fin/Properties.lagda.md
+++ b/src/Data/Fin/Properties.lagda.md
@@ -262,8 +262,9 @@ _between_ finite sets) [[merely]] split:
 ```agda
 finite-surjection-split
   : ∀ {ℓ} {n} {B : Type ℓ}
-  → (f : B → Fin n) → is-surjective f
-  → ∥ (∀ x → fibre f x) ∥
+  → (f : B → Fin n) 
+  → is-surjective f
+  → is-split-surjective f
 finite-surjection-split f = finite-choice _
 ```
 
diff --git a/src/Data/Set/Projective.lagda.md b/src/Data/Set/Projective.lagda.md
index 73131df22..b36828daf 100644
--- a/src/Data/Set/Projective.lagda.md
+++ b/src/Data/Set/Projective.lagda.md
@@ -4,7 +4,6 @@ description: |
 ---
 <!--
 ```agda
-open import 1Lab.Classical
 open import 1Lab.Prelude
 
 open import Data.Dec
@@ -28,7 +27,7 @@ private variable
 
 :::{.definition #set-projective}
 A type $A$ is **set-projective** if we can commute [[propositional truncation]]
-past $A$-indexed families.
+past $A$-indexed families of [[sets]].
 :::
 
 ```agda
@@ -46,22 +45,31 @@ $A$-indexed version of the [[axiom of choice]].
 If $A$ is a set, then $A$ is set-projective if and only if every
 surjection $E \to A$ from a set $E$ splits.
 
+<!-- [TODO: Reed M, 19/05/2025]
+  This could be made into a more elegant argument via a chain of equivalences:
+  The crux is really that Fibre-equiv step!
+-->
+
 ```agda
+set-surjections-split : (A : Type ℓ) → (κ : Level) → Type _
+set-surjections-split {ℓ = ℓ} A κ =
+  ∀ (E : Type κ)
+  → is-set E
+  → (f : E → A)
+  → is-surjective f
+  → is-split-surjective f
+
 surjections-split→set-projective
-  : ∀ {ℓ ℓ'} {A : Type ℓ}
+  : ∀ {ℓ κ} {A : Type ℓ}
   → is-set A
-  → (∀ (E : Type (ℓ ⊔ ℓ')) → is-set E
-     → (f : E → A) → is-surjective f
-     → ∥ (∀ a → fibre f a) ∥)
-  → is-set-projective A (ℓ ⊔ ℓ')
+  → set-surjections-split A (ℓ ⊔ κ)
+  → is-set-projective A (ℓ ⊔ κ)
 
 sets-projective→surjections-split
-  : ∀ {ℓ ℓ'} {A : Type ℓ}
+  : ∀ {ℓ κ} {A : Type ℓ}
   → is-set A
-  → is-set-projective A (ℓ ⊔ ℓ')
-  → ∀ {E : Type ℓ'} → is-set E
-  → (f : E → A) → is-surjective f
-  → ∥ (∀ a → fibre f a) ∥
+  → is-set-projective A (ℓ ⊔ κ)
+  → set-surjections-split A (ℓ ⊔ κ)
 ```
 
 <details>
@@ -76,7 +84,7 @@ surjections-split→set-projective {A = A} A-set surj-split P P-set ∥P∥ =
     (surj-split (Σ[ x ∈ A ] (P x)) (Σ-is-hlevel 2 A-set P-set) fst λ x →
       ∥-∥-map (Equiv.from (Fibre-equiv P x)) (∥P∥ x))
 
-sets-projective→surjections-split A-set A-pro E-set f =
+sets-projective→surjections-split A-set A-pro E E-set f =
   A-pro (fibre f) (λ x → fibre-is-hlevel 2 E-set A-set f x)
 ```
 </details>
diff --git a/src/Homotopy/Connectedness.lagda.md b/src/Homotopy/Connectedness.lagda.md
index 4adef5ea8..9fa711ffd 100644
--- a/src/Homotopy/Connectedness.lagda.md
+++ b/src/Homotopy/Connectedness.lagda.md
@@ -77,7 +77,7 @@ is-n-connected-map f n = ∀ x → is-n-connected (fibre f x) n
 ```
 :::
 
-## Pointed connected types
+## Pointed connected types {defines="pointed-connected-type"}
 
 In the case of [[pointed types]], there is an equivalent definition of
 being connected that is sometimes easier to work with: a pointed type is