diff --git a/src/foundation/connected-types.lagda.md b/src/foundation/connected-types.lagda.md
index 06cf448eef..160d65fa7d 100644
--- a/src/foundation/connected-types.lagda.md
+++ b/src/foundation/connected-types.lagda.md
@@ -271,3 +271,18 @@ module _
                 ( λ where refl → refl)
                 ( center (K a x)))))
 ```
+
+In particular, inhabited types are `-1`-connected; their identity types are
+`-2`-connected, as all types are. This characterizes the `-1`-connected types,
+i.e., `X` is `-1`-connected iff it's inhabited.
+
+```agda
+is-neg-one-connected-is-inhabited :
+  {l : Level} (A : UU l) → is-inhabited A → is-connected neg-one-𝕋 A
+is-neg-one-connected-is-inhabited A a =
+  is-connected-succ-is-connected-eq a (λ x y → is-neg-two-connected (x ＝ y))
+
+is-inhabited-is-neg-one-connected :
+  {l : Level} (A : UU l) → is-connected neg-one-𝕋 A → is-inhabited A
+is-inhabited-is-neg-one-connected A (a , _) = a
+```
diff --git a/src/foundation/sections.lagda.md b/src/foundation/sections.lagda.md
index 0c9cd52162..e28ca21460 100644
--- a/src/foundation/sections.lagda.md
+++ b/src/foundation/sections.lagda.md
@@ -20,6 +20,7 @@ open import foundation.whiskering-homotopies-composition
 
 open import foundation-core.contractible-types
 open import foundation-core.equivalences
+open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
@@ -187,4 +188,48 @@ is-injective-map-section-family :
   {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (b : (x : A) → B x) →
   is-injective (map-section-family b)
 is-injective-map-section-family b = ap pr1
+
+injection-map-section-family :
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (b : (x : A) → B x) →
+  injection A (Σ A B)
+pr1 (injection-map-section-family b) = map-section-family b
+pr2 (injection-map-section-family b) = is-injective-map-section-family b
+```
+
+### The space of sections of `f : A → B` is equivalent to the space of dependent maps `(b : B) → fiber f b`
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  section-dependent-fiber : section f → (b : B) → fiber f b
+  pr1 (section-dependent-fiber (g , s) b) = g b
+  pr2 (section-dependent-fiber (g , s) b) = s b
+
+  dependent-fiber-section : ((b : B) → fiber f b) → section f
+  pr1 (dependent-fiber-section g) b = pr1 (g b)
+  pr2 (dependent-fiber-section g) b = pr2 (g b)
+
+  equiv-section-dependent-fiber :
+    section f ≃ ((b : B) → fiber f b)
+  pr1 equiv-section-dependent-fiber = section-dependent-fiber
+  pr1 (pr1 (pr2 equiv-section-dependent-fiber)) = dependent-fiber-section
+  pr2 (pr1 (pr2 equiv-section-dependent-fiber)) = refl-htpy
+  pr1 (pr2 (pr2 equiv-section-dependent-fiber)) = dependent-fiber-section
+  pr2 (pr2 (pr2 equiv-section-dependent-fiber)) = refl-htpy
+```
+
+### Sections are injective
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  is-injective-is-section : (g : B → A) → is-section f g → is-injective g
+  is-injective-is-section g s {x} {y} eq = inv (s x) ∙ ap f eq ∙ s y
+
+  injection-section : section f → injection B A
+  injection-section (g , s) = (g , is-injective-is-section g s)
 ```
diff --git a/src/foundation/set-truncations.lagda.md b/src/foundation/set-truncations.lagda.md
index 154cc2d2b5..774c72c400 100644
--- a/src/foundation/set-truncations.lagda.md
+++ b/src/foundation/set-truncations.lagda.md
@@ -567,3 +567,18 @@ module _
   triangle-distributive-trunc-product-Set =
     pr2 (center distributive-trunc-product-Set)
 ```
+
+### `X` is empty iff its set truncation is empty
+
+```agda
+module _
+  {l : Level} {X : UU l}
+  where
+
+  is-empty-set-truncation-is-empty : is-empty (type-trunc-Set X) → is-empty X
+  is-empty-set-truncation-is-empty p x = p (unit-trunc-Set x)
+
+  set-truncation-is-empty-is-empty : is-empty X → is-empty (type-trunc-Set X)
+  set-truncation-is-empty-is-empty p x =
+    apply-universal-property-trunc-Set empty-Set x p
+```
diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md
index 969c1e7ade..2cbeb26a24 100644
--- a/src/foundation/surjective-maps.lagda.md
+++ b/src/foundation/surjective-maps.lagda.md
@@ -34,6 +34,7 @@ open import foundation.universe-levels
 open import foundation-core.cartesian-product-types
 open import foundation-core.constant-maps
 open import foundation-core.contractible-maps
+open import foundation-core.empty-types
 open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
@@ -871,6 +872,18 @@ module _
     is-inhabited-is-surjective (is-surjective-map-surjection f)
 ```
 
+### Empty types are closed under surjections
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (emp-A : is-empty A)
+  where
+
+  is-empty-surjection : A ↠ B → is-empty B
+  is-empty-surjection (f , p) b =
+    rec-trunc-Prop empty-Prop (λ (a , q) → emp-A a) (p b)
+```
+
 ### The type of surjections `A ↠ B` is equivalent to the type of families `P` of inhabited types over `B` equipped with an equivalence `A ≃ Σ B P`
 
 > This remains to be shown.
diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
index a37d589205..2e8e5a9c3c 100644
--- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
+++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
@@ -22,6 +22,7 @@ open import foundation.epimorphisms
 open import foundation.equivalences
 open import foundation.fibers-of-maps
 open import foundation.function-extensionality
+open import foundation.surjective-maps
 open import foundation.function-types
 open import foundation.functoriality-dependent-function-types
 open import foundation.functoriality-dependent-pair-types
@@ -127,6 +128,29 @@ module _
             ( ac b)))
 ```
 
+### Acyclic maps are surjective
+
+Hence, epimorphisms are surjective.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  abstract
+    is-surjective-is-acyclic-map : is-acyclic-map f → is-surjective f
+    is-surjective-is-acyclic-map ac x =
+      is-inhabited-is-acyclic
+        ( fiber f x)
+        ( ac x)
+
+    is-surjective-is-epimorphism : is-epimorphism f → is-surjective f
+    is-surjective-is-epimorphism epi x =
+      is-inhabited-is-acyclic
+        ( fiber f x)
+        ( is-acyclic-map-is-epimorphism f epi x)
+```
+
 ### A type is acyclic if and only if its terminal map is an acyclic map
 
 ```agda
diff --git a/src/synthetic-homotopy-theory/acyclic-types.lagda.md b/src/synthetic-homotopy-theory/acyclic-types.lagda.md
index cb83beef9d..15e3214912 100644
--- a/src/synthetic-homotopy-theory/acyclic-types.lagda.md
+++ b/src/synthetic-homotopy-theory/acyclic-types.lagda.md
@@ -7,8 +7,11 @@ module synthetic-homotopy-theory.acyclic-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.0-connected-types
 open import foundation.contractible-types
 open import foundation.equivalences
+open import foundation.inhabited-types
+open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.retracts-of-types
 open import foundation.unit-type
@@ -80,7 +83,16 @@ is-acyclic-unit = is-acyclic-is-contr unit is-contr-unit
 
 ### Acyclic types are inhabited
 
-> TODO
+**Proof.** `Σ X` is 0-connected if and only if `X` is inhabited, and contractible
+types are of course 0-connected. ∎
+
+```agda
+is-inhabited-is-acyclic : {l : Level} (A : UU l) → is-acyclic A → is-inhabited A
+is-inhabited-is-acyclic A ac =
+  is-inhabited-suspension-is-0-connected
+    ( A)
+    ( is-0-connected-is-contr (suspension A) ac)
+```
 
 ## See also
 
diff --git a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md
index 35f8ab47d9..4f5ffd36ae 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md
@@ -1,6 +1,8 @@
 # Suspensions of propositions
 
 ```agda
+{-# OPTIONS --lossy-unification #-}
+
 module synthetic-homotopy-theory.suspensions-of-propositions where
 ```
 
@@ -9,6 +11,7 @@ module synthetic-homotopy-theory.suspensions-of-propositions where
 ```agda
 open import foundation.booleans
 open import foundation.contractible-types
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.existential-quantification
@@ -19,6 +22,8 @@ open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
+open import foundation.set-truncations
+open import foundation.propositional-truncations
 open import foundation.subsingleton-induction
 open import foundation.surjective-maps
 open import foundation.torsorial-type-families
@@ -487,6 +492,205 @@ module _
         ( surjection-equiv equiv-bool-Fin-2))
 ```
 
+### The suspension of the propositional truncation is the set-truncation of the suspension
+
+```agda
+module _
+  {l : Level} (X : UU l)
+  where
+
+  suspension-structure-suspension-trunc-prop-trunc-set-suspension :
+    suspension-structure (type-trunc-Prop X) (type-trunc-Set (suspension X))
+  pr1 suspension-structure-suspension-trunc-prop-trunc-set-suspension =
+    unit-trunc-Set north-suspension
+  pr1 (pr2 suspension-structure-suspension-trunc-prop-trunc-set-suspension) =
+    unit-trunc-Set south-suspension
+  pr2 (pr2 suspension-structure-suspension-trunc-prop-trunc-set-suspension) =
+    rec-trunc-Prop
+      ( Id-Prop
+        ( trunc-Set (suspension X))
+        ( unit-trunc-Set north-suspension)
+        ( unit-trunc-Set south-suspension))
+      ( λ x → ap unit-trunc-Set (meridian-suspension x))
+
+  suspension-trunc-prop-trunc-set-suspension :
+    suspension (type-trunc-Prop X) → type-trunc-Set (suspension X)
+  suspension-trunc-prop-trunc-set-suspension =
+    cogap-suspension
+      ( suspension-structure-suspension-trunc-prop-trunc-set-suspension)
+
+  suspension-structure-trunc-set-suspension-suspension-trunc-prop :
+    suspension-structure X (suspension (type-trunc-Prop X))
+  pr1 suspension-structure-trunc-set-suspension-suspension-trunc-prop =
+    north-suspension
+  pr1 (pr2 suspension-structure-trunc-set-suspension-suspension-trunc-prop) =
+    south-suspension
+  pr2 (pr2 suspension-structure-trunc-set-suspension-suspension-trunc-prop) x =
+    meridian-suspension (unit-trunc-Prop x)
+
+  trunc-set-suspension-suspension-trunc-prop :
+    type-trunc-Set (suspension X) → suspension (type-trunc-Prop X)
+  trunc-set-suspension-suspension-trunc-prop =
+    map-universal-property-trunc-Set
+      ( suspension-set-Prop (trunc-Prop X))
+      ( cogap-suspension
+          suspension-structure-trunc-set-suspension-suspension-trunc-prop)
+
+  dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension :
+    dependent-suspension-structure
+      ( λ z →
+        ( trunc-set-suspension-suspension-trunc-prop ∘
+          suspension-trunc-prop-trunc-set-suspension)
+        ( z)
+        ＝ z)
+      ( suspension-structure-suspension (type-trunc-Prop X))
+  pr1 dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension =
+    ap
+      ( trunc-set-suspension-suspension-trunc-prop)
+      ( compute-north-cogap-suspension
+        ( suspension-structure-suspension-trunc-prop-trunc-set-suspension)) ∙
+    triangle-universal-property-trunc-Set
+      ( suspension-set-Prop (trunc-Prop X))
+      ( cogap-suspension
+        ( suspension-structure-trunc-set-suspension-suspension-trunc-prop))
+      ( north-suspension) ∙
+    compute-north-cogap-suspension
+      ( suspension-structure-trunc-set-suspension-suspension-trunc-prop)
+  pr1 (pr2 dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension) =
+    ap
+      ( trunc-set-suspension-suspension-trunc-prop)
+      ( compute-south-cogap-suspension
+        ( suspension-structure-suspension-trunc-prop-trunc-set-suspension)) ∙
+    triangle-universal-property-trunc-Set
+      ( suspension-set-Prop (trunc-Prop X))
+      ( cogap-suspension
+        ( suspension-structure-trunc-set-suspension-suspension-trunc-prop))
+      ( south-suspension) ∙
+    compute-south-cogap-suspension
+      ( suspension-structure-trunc-set-suspension-suspension-trunc-prop)
+  pr2 (pr2 dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension) _ =
+    eq-is-prop
+      ( is-set-suspension-Prop
+        ( trunc-Prop X)
+        ( ( trunc-set-suspension-suspension-trunc-prop ∘
+            suspension-trunc-prop-trunc-set-suspension)
+          ( south-suspension))
+        ( south-suspension))
+
+  dependent-suspension-structure-eq-type-trunc-set-suspension :
+    dependent-suspension-structure
+      (λ z → type-Set
+        (set-Prop
+          (Id-Prop
+            (trunc-Set (suspension X))
+            ( (suspension-trunc-prop-trunc-set-suspension ∘
+              trunc-set-suspension-suspension-trunc-prop)
+              (unit-trunc-Set z))
+            (unit-trunc-Set z))))
+      (suspension-structure-suspension X)
+  pr1 dependent-suspension-structure-eq-type-trunc-set-suspension =
+    ap
+      ( suspension-trunc-prop-trunc-set-suspension)
+      ( triangle-universal-property-trunc-Set
+        ( suspension-set-Prop (trunc-Prop X))
+        ( cogap-suspension
+          suspension-structure-trunc-set-suspension-suspension-trunc-prop)
+        ( north-suspension) ∙
+        ( compute-north-cogap-suspension
+          ( suspension-structure-trunc-set-suspension-suspension-trunc-prop))) ∙
+    compute-north-cogap-suspension
+      ( suspension-structure-suspension-trunc-prop-trunc-set-suspension)
+  pr1 (pr2 dependent-suspension-structure-eq-type-trunc-set-suspension) =
+    ap
+      ( suspension-trunc-prop-trunc-set-suspension)
+      ( triangle-universal-property-trunc-Set
+        ( suspension-set-Prop (trunc-Prop X))
+        ( cogap-suspension
+          suspension-structure-trunc-set-suspension-suspension-trunc-prop)
+        ( south-suspension) ∙
+        ( compute-south-cogap-suspension
+          ( suspension-structure-trunc-set-suspension-suspension-trunc-prop))) ∙
+    compute-south-cogap-suspension
+      ( suspension-structure-suspension-trunc-prop-trunc-set-suspension)
+  pr2 (pr2 dependent-suspension-structure-eq-type-trunc-set-suspension) x =
+    eq-is-prop
+      ( is-set-type-trunc-Set
+        ( ( suspension-trunc-prop-trunc-set-suspension ∘
+            trunc-set-suspension-suspension-trunc-prop)
+          ( unit-trunc-Set
+      ( south-suspension-structure
+        ( suspension-structure-suspension X))))
+        ( unit-trunc-Set
+          ( south-suspension-structure
+            ( suspension-structure-suspension X))))
+
+  eq-type-trunc-set-suspension :
+    (x : type-trunc-Set (suspension X)) →
+    ( suspension-trunc-prop-trunc-set-suspension ∘
+      trunc-set-suspension-suspension-trunc-prop)
+      x ＝
+    x
+  eq-type-trunc-set-suspension x =
+    function-dependent-universal-property-trunc-Set
+      ( λ y →
+        set-Prop
+          ( Id-Prop
+            ( trunc-Set (suspension X))
+            ( ( suspension-trunc-prop-trunc-set-suspension ∘
+                trunc-set-suspension-suspension-trunc-prop)
+              ( y))
+            ( y)))
+      ( dependent-cogap-suspension _
+        ( dependent-suspension-structure-eq-type-trunc-set-suspension))
+      ( x)
+
+  suspension-structure-eq-trunc-set-suspension :
+    (x : type-trunc-Set (suspension X)) →
+    suspension-structure
+      (X)
+      ((suspension-trunc-prop-trunc-set-suspension ∘
+        trunc-set-suspension-suspension-trunc-prop)
+        x ＝
+      x)
+  pr1 (suspension-structure-eq-trunc-set-suspension x) =
+    eq-type-trunc-set-suspension x
+  pr1 (pr2 (suspension-structure-eq-trunc-set-suspension x)) =
+    eq-type-trunc-set-suspension x
+  pr2 (pr2 (suspension-structure-eq-trunc-set-suspension x)) _ =
+    eq-is-prop
+      ( is-set-type-trunc-Set
+        ( ( suspension-trunc-prop-trunc-set-suspension ∘
+            trunc-set-suspension-suspension-trunc-prop)
+          ( x))
+        ( x))
+
+  is-equiv-suspension-trunc-prop-trunc-set-suspension :
+    is-equiv suspension-trunc-prop-trunc-set-suspension
+  pr1 (pr1 is-equiv-suspension-trunc-prop-trunc-set-suspension) =
+    trunc-set-suspension-suspension-trunc-prop
+  pr2 (pr1 is-equiv-suspension-trunc-prop-trunc-set-suspension) x =
+    apply-universal-property-trunc-Set
+      ( set-Prop
+        ( Id-Prop
+          ( trunc-Set (suspension X))
+          ( ( suspension-trunc-prop-trunc-set-suspension ∘
+              trunc-set-suspension-suspension-trunc-prop)
+            x)
+          ( x)))
+        ( x)
+        ( cogap-suspension (suspension-structure-eq-trunc-set-suspension x))
+  pr1 (pr2 is-equiv-suspension-trunc-prop-trunc-set-suspension) =
+    trunc-set-suspension-suspension-trunc-prop
+  pr2 (pr2 is-equiv-suspension-trunc-prop-trunc-set-suspension) =
+    dependent-cogap-suspension
+      ( λ z →
+        ( trunc-set-suspension-suspension-trunc-prop ∘
+          suspension-trunc-prop-trunc-set-suspension)
+        ( z)
+        ＝ z)
+      ( dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension)
+```
+
 ## See also
 
 - Suspensions of propositions are used in the proof of
diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index b0d6084cbc..f59962a476 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -1,12 +1,17 @@
 # Suspensions of types
 
 ```agda
+{-# OPTIONS --lossy-unification --allow-unsolved-metas #-}
+
 module synthetic-homotopy-theory.suspensions-of-types where
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.0-connected-types
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.booleans
@@ -17,6 +22,8 @@ open import foundation.contractible-types
 open import foundation.dependent-identifications
 open import foundation.dependent-pair-types
 open import foundation.diagonal-maps-of-types
+open import foundation.double-negation
+open import foundation.empty-types
 open import foundation.equivalence-extensionality
 open import foundation.equivalences
 open import foundation.fibers-of-maps
@@ -26,13 +33,17 @@ open import foundation.functoriality-dependent-function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
 open import foundation.identity-types
-open import foundation.path-algebra
+open import foundation.inhabited-types
+open import foundation.mere-equality
+open import foundation.mere-equivalences
 open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.retractions
 open import foundation.sections
+open import foundation.set-truncations
 open import foundation.surjective-maps
 open import foundation.torsorial-type-families
+open import foundation.transport-along-equivalences
 open import foundation.transport-along-identifications
 open import foundation.truncated-types
 open import foundation.truncation-levels
@@ -41,6 +52,12 @@ open import foundation.unit-type
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
+open import foundation-core.coproduct-types
+open import foundation-core.negation
+open import foundation-core.sets
+
+open import logic.propositionally-decidable-types
+
 open import synthetic-homotopy-theory.cocones-under-spans
 open import synthetic-homotopy-theory.dependent-cocones-under-spans
 open import synthetic-homotopy-theory.dependent-suspension-structures
@@ -49,6 +66,12 @@ open import synthetic-homotopy-theory.pushouts
 open import synthetic-homotopy-theory.suspension-structures
 open import synthetic-homotopy-theory.universal-property-pushouts
 open import synthetic-homotopy-theory.universal-property-suspensions
+
+open import univalent-combinatorics.2-element-types
+open import univalent-combinatorics.counting
+open import univalent-combinatorics.finite-types
+open import univalent-combinatorics.finitely-enumerable-types
+open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>
@@ -64,7 +87,7 @@ type `X` is the [pushout](synthetic-homotopy-theory.pushouts.md) of the
 ```
 
 Suspensions play an important role in synthetic homotopy theory. For example,
-they star in the freudenthal suspension theorem and give us a definition of
+they star in the Freudenthal suspension theorem and give us a definition of
 [the spheres](synthetic-homotopy-theory.spheres.md).
 
 ## Definitions
@@ -92,6 +115,10 @@ meridian-suspension :
 meridian-suspension {X = X} =
   glue-pushout (terminal-map X) (terminal-map X)
 
+is-inhabited-suspension :
+  {l : Level} (X : UU l) → is-inhabited (suspension X)
+is-inhabited-suspension X = unit-trunc-Prop north-suspension
+
 suspension-structure-suspension :
   {l : Level} (X : UU l) → suspension-structure X (suspension X)
 pr1 (suspension-structure-suspension X) = north-suspension
@@ -552,6 +579,100 @@ module _
     is-surjective-map-surjection-bool-suspension
 ```
 
+This provides a
+[finite enumeration](univalent-combinatorics.finitely-enumerable-types.md) of
+`Σ X` by the canonical equivalence `bool ≃ Fin 2`.
+
+```agda
+  finite-enumeration-suspension : finite-enumeration (suspension X)
+  pr1 finite-enumeration-suspension = 2
+  pr2 finite-enumeration-suspension =
+    comp-surjection
+      ( surjection-bool-suspension)
+      ( surjection-equiv equiv-bool-Fin-2)
+```
+
+### The suspension of an empty type is the booleans
+
+```agda
+module _
+  {l : Level} (X : UU l) (emp : is-empty X)
+  where
+
+  suspension-structure-empty-bool : suspension-structure X bool
+  pr1 suspension-structure-empty-bool = true
+  pr1 (pr2 suspension-structure-empty-bool) = false
+  pr2 (pr2 suspension-structure-empty-bool) = ex-falso ∘ emp
+
+  inv-map-surjection-bool-suspension : suspension X → bool
+  inv-map-surjection-bool-suspension =
+    cogap-suspension suspension-structure-empty-bool
+
+  compute-true-suspension-empty-bool :
+    inv-map-surjection-bool-suspension north-suspension ＝ true
+  compute-true-suspension-empty-bool =
+    compute-north-cogap-suspension suspension-structure-empty-bool
+
+  compute-false-suspension-empty-bool :
+    inv-map-surjection-bool-suspension south-suspension ＝ false
+  compute-false-suspension-empty-bool =
+    compute-south-cogap-suspension suspension-structure-empty-bool
+
+  compute-north-suspension-empty-bool :
+    ( map-surjection-bool-suspension {X = X} ∘
+      inv-map-surjection-bool-suspension)
+        north-suspension
+    ＝ north-suspension
+  compute-north-suspension-empty-bool =
+    ap map-surjection-bool-suspension compute-true-suspension-empty-bool
+
+  compute-south-suspension-empty-bool :
+    ( map-surjection-bool-suspension {X = X} ∘
+      inv-map-surjection-bool-suspension)
+        south-suspension
+    ＝ south-suspension
+  compute-south-suspension-empty-bool =
+    ap map-surjection-bool-suspension compute-false-suspension-empty-bool
+
+  dependent-suspension-sutructure-surjection-bool-suspension :
+    dependent-suspension-structure
+      (λ z →
+        (map-surjection-bool-suspension ∘ inv-map-surjection-bool-suspension)
+        (z)
+        ＝ z)
+      (suspension-structure-suspension X)
+  pr1 dependent-suspension-sutructure-surjection-bool-suspension =
+    compute-north-suspension-empty-bool
+  pr1 (pr2 dependent-suspension-sutructure-surjection-bool-suspension) =
+    compute-south-suspension-empty-bool
+  pr2 (pr2 dependent-suspension-sutructure-surjection-bool-suspension) x =
+    ex-falso (emp x)
+
+  is-equiv-map-surjection-bool-suspension :
+    is-equiv map-surjection-bool-suspension
+  pr1 (pr1 is-equiv-map-surjection-bool-suspension) =
+    inv-map-surjection-bool-suspension
+  pr2 (pr1 is-equiv-map-surjection-bool-suspension) =
+    dependent-cogap-suspension
+      ( λ z →
+        ( map-surjection-bool-suspension ∘ inv-map-surjection-bool-suspension)
+        ( z)
+        ＝ z)
+      ( dependent-suspension-sutructure-surjection-bool-suspension)
+  pr1 (pr2 is-equiv-map-surjection-bool-suspension) =
+    inv-map-surjection-bool-suspension
+  pr2 (pr2 is-equiv-map-surjection-bool-suspension) true =
+    compute-true-suspension-empty-bool
+  pr2 (pr2 is-equiv-map-surjection-bool-suspension) false =
+    compute-false-suspension-empty-bool
+
+  equiv-map-surjection-bool-suspension :
+    bool ≃ suspension X
+  pr1 equiv-map-surjection-bool-suspension = map-surjection-bool-suspension
+  pr2 equiv-map-surjection-bool-suspension =
+    is-equiv-map-surjection-bool-suspension
+```
+
 ### The suspension of a contractible type is contractible
 
 ```agda
@@ -644,3 +765,126 @@ module _
               ( Y))
           ( is-equiv-id))
 ```
+
+### `Σ X` is 0-connected iff `X` is inhabited
+
+Note that `Σ empty ＝ bool` is _not_ `0`-connected.
+
+The forward direction is the subtle one. When `Σ X` is 0-connected, then in
+particular we [merely](foundation.mere-equality.md) have `p ∈ north ＝ south`;
+such identifications are inductively generated by `X`.
+
+```agda
+is-0-connected-suspension-is-inhabited :
+  {l : Level} (X : UU l) → is-inhabited X → is-0-connected (suspension X)
+is-0-connected-suspension-is-inhabited X x =
+  is-connected-succ-suspension-is-connected
+    ( is-neg-one-connected-is-inhabited X x)
+
+is-inhabited-is-0-connected-suspension :
+  {l : Level} (X : UU l) → is-0-connected (suspension X) → is-inhabited X
+is-inhabited-is-0-connected-suspension X ΣX-conn =
+  rec-trunc-Prop (is-inhabited-Prop X) (λ h → {!   !}) p
+    where
+    p : mere-eq (north-suspension {X = X}) (south-suspension {X = X})
+    p = mere-eq-is-0-connected ΣX-conn north-suspension south-suspension
+```
+
+In fact, the following are logically equivalent:
+
+- `X` is [inhabited or empty](logic.propositionally-decidable-types.md)
+- `trunc-Set (Σ X)` is [finite](univalent-combinatorics.finite-types.md)
+
+Note the relationship with this and
+[Diaconescu's theorem](foundation.diaconescus-theorem.md).
+
+**Proof.**
+
+(->): When `X` is empty, its suspension is the set `Fin 2`. When `X` is
+inhabited, its suspension is 0-connected, and 0-truncated 0-connected types are
+contractible and hence are `Fin 1`.
+
+(<-): Such a cardinality can only be 1 or 2 - suspensions are inhabited, say, by
+`north`, and the cardinality of a type finitely enumerated by `Fin 2 ＝ bool`
+can be no more than 2. When it's 1, i.e. when `trunc-Set (Σ X)` is contractible,
+well, this is the definition of 0-connectedness of `Σ X`, and therefore `X` is
+inhabited. When it's 2, i.e. when there are no identifications `north ＝ south`
+in `Σ X`, then `X` better have been empty. ∎
+
+```agda
+module _
+  {l : Level} (X : UU l)
+  where
+
+  trunc-suspension-is-contractible-is-pointed :
+    X → is-contr (type-trunc-Set (suspension X))
+  trunc-suspension-is-contractible-is-pointed x =
+    is-0-connected-suspension-is-inhabited X (unit-trunc-Prop x)
+
+  trunc-suspension-is-contractible-is-inhabited :
+    is-inhabited X → is-contr (type-trunc-Set (suspension X))
+  trunc-suspension-is-contractible-is-inhabited x =
+    rec-trunc-Prop
+      ( is-contr-Prop (type-trunc-Set (suspension X)))
+      ( trunc-suspension-is-contractible-is-pointed)
+      ( x)
+
+  is-finite-suspension-is-inhabited-or-empty :
+    is-inhabited-or-empty X → is-finite (type-trunc-Set (suspension X))
+  is-finite-suspension-is-inhabited-or-empty (inl x) =
+    is-finite-is-contr (trunc-suspension-is-contractible-is-inhabited x)
+  is-finite-suspension-is-inhabited-or-empty (inr x) =
+    is-finite-equiv
+      ( equiv-unit-trunc-set
+          ( suspension X ,
+            is-set-equiv
+              ( bool)
+              ( inv-equiv
+                ( equiv-map-surjection-bool-suspension X x))
+              ( is-set-bool)) ∘e
+        equiv-map-surjection-bool-suspension X x)
+      ( is-finite-bool)
+
+  is-empty-trunc-suspension-has-two-elements :
+    has-two-elements (type-trunc-Set (suspension X)) → is-empty X
+  is-empty-trunc-suspension-has-two-elements p x =
+    intro-double-negation
+      ( ap unit-trunc-Set (meridian-suspension x))
+      ( λ _ → is-not-one-two-ℕ (eq-cardinality p (unit-trunc-Prop eq)))
+        where
+        eq : Fin 1 ≃ type-trunc-Set (suspension X)
+        pr1 eq (inr star) = unit-trunc-Set north-suspension
+        pr1 (pr1 (pr2 eq)) _ = inr star
+        pr2 (pr1 (pr2 eq)) _ =
+          eq-is-contr (trunc-suspension-is-contractible-is-pointed x)
+        pr1 (pr2 (pr2 eq)) _ = inr star
+        pr2 (pr2 (pr2 eq)) (inr star) = refl
+
+  is-inhabited-or-empty-is-finite-suspension :
+    is-finite (type-trunc-Set (suspension X)) → is-inhabited-or-empty X
+  is-inhabited-or-empty-is-finite-suspension p with number-of-elements-is-finite p in eq
+  ... | 0 =
+    ex-falso
+      ( is-nonempty-is-inhabited
+        ( is-inhabited-suspension X)
+        ( is-empty-set-truncation-is-empty
+          ( is-empty-is-zero-number-of-elements-is-finite p eq)))
+  ... | 1 =
+    inl
+      ( is-inhabited-is-0-connected-suspension
+        ( X)
+        ( is-contr-is-one-number-of-elements-is-finite p eq))
+  ... | 2 =
+    inr
+      ( is-empty-trunc-suspension-has-two-elements
+        ( map-inv-equiv-has-cardinality-id-number-of-elements-is-finite
+          ( type-trunc-Set (suspension X))
+          ( p)
+          ( 2)
+          ( eq)))
+  ... | succ-ℕ (succ-ℕ (succ-ℕ n)) = ex-falso {! is-upper-bound-finite-enumeration  !}
+```
+
+## See also
+
+- [Suspensions of propositions](synthetic-homotopy-theory.suspensions-of-propositions.md)
diff --git a/src/univalent-combinatorics/2-element-types.lagda.md b/src/univalent-combinatorics/2-element-types.lagda.md
index b44650d1ca..5575e20b50 100644
--- a/src/univalent-combinatorics/2-element-types.lagda.md
+++ b/src/univalent-combinatorics/2-element-types.lagda.md
@@ -203,7 +203,7 @@ pr1 (extensionality-2-Element-Type X Y) = equiv-eq-2-Element-Type X Y
 pr2 (extensionality-2-Element-Type X Y) = is-equiv-equiv-eq-2-Element-Type X Y
 ```
 
-### Characterization the identifications of `Fin 2` with a `2`-element type `X`
+### Characterizing the identifications of `Fin 2` with a `2`-element type `X`
 
 #### Evaluating an equivalence and an automorphism at `0 : Fin 2`
 
diff --git a/src/univalent-combinatorics/finite-choice.lagda.md b/src/univalent-combinatorics/finite-choice.lagda.md
index 43f0971a20..1713e5712f 100644
--- a/src/univalent-combinatorics/finite-choice.lagda.md
+++ b/src/univalent-combinatorics/finite-choice.lagda.md
@@ -42,7 +42,7 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-[Propositional truncations](foundation.propositional-truncations.md) distributes
+[Propositional truncations](foundation.propositional-truncations.md) distribute
 over finite products.
 
 ## Theorems
diff --git a/src/univalent-combinatorics/finite-types.lagda.md b/src/univalent-combinatorics/finite-types.lagda.md
index ab9b151fe7..bc2bb88f8a 100644
--- a/src/univalent-combinatorics/finite-types.lagda.md
+++ b/src/univalent-combinatorics/finite-types.lagda.md
@@ -772,6 +772,18 @@ abstract
           ( λ m → has-cardinality-ℕ m X)
           ( p)
           ( pr2 (has-finite-cardinality-is-finite H)))
+
+  map-equiv-has-cardinality-id-number-of-elements-is-finite :
+    {l : Level} (X : UU l) ( H : is-finite X) (n : ℕ) →
+    has-cardinality-ℕ n X → Id (number-of-elements-is-finite H) n
+  map-equiv-has-cardinality-id-number-of-elements-is-finite X H n =
+    map-equiv (equiv-has-cardinality-id-number-of-elements-is-finite X H n)
+
+  map-inv-equiv-has-cardinality-id-number-of-elements-is-finite :
+    {l : Level} (X : UU l) ( H : is-finite X) (n : ℕ) →
+    Id (number-of-elements-is-finite H) n → has-cardinality-ℕ n X
+  map-inv-equiv-has-cardinality-id-number-of-elements-is-finite X H n =
+    map-inv-equiv (equiv-has-cardinality-id-number-of-elements-is-finite X H n)
 ```
 
 ## External links
diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md
index 5e4c08a6ec..2e19215320 100644
--- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md
+++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md
@@ -1,6 +1,8 @@
 # Finitely enumerable types
 
 ```agda
+{-# OPTIONS --allow-unsolved-metas --lossy-unification #-}
+
 module univalent-combinatorics.finitely-enumerable-types where
 ```
 
@@ -9,6 +11,7 @@ module univalent-combinatorics.finitely-enumerable-types where
 ```agda
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
 
 open import foundation.action-on-identifications-functions
 open import foundation.booleans
@@ -17,6 +20,7 @@ open import foundation.conjunction
 open import foundation.coproduct-types
 open import foundation.decidable-equality
 open import foundation.dependent-pair-types
+open import foundation.existential-quantification
 open import foundation.embeddings
 open import foundation.equality-cartesian-product-types
 open import foundation.equivalences
@@ -28,9 +32,13 @@ open import foundation.functoriality-coproduct-types
 open import foundation.functoriality-propositional-truncation
 open import foundation.identity-types
 open import foundation.logical-equivalences
+open import foundation.negation
 open import foundation.propositional-truncations
+open import foundation.injective-maps
+open import foundation.inhabited-types
 open import foundation.propositions
 open import foundation.raising-universe-levels
+open import foundation.sections
 open import foundation.subtypes
 open import foundation.transport-along-identifications
 open import foundation.type-arithmetic-booleans
@@ -38,6 +46,8 @@ open import foundation.type-arithmetic-coproduct-types
 open import foundation.unit-type
 open import foundation.universe-levels
 
+open import foundation-core.empty-types
+
 open import univalent-combinatorics.cartesian-product-types
 open import univalent-combinatorics.coproduct-types
 open import univalent-combinatorics.counting
@@ -45,7 +55,9 @@ open import univalent-combinatorics.counting-decidable-subtypes
 open import univalent-combinatorics.counting-dependent-pair-types
 open import univalent-combinatorics.dedekind-finite-types
 open import univalent-combinatorics.finite-types
+open import univalent-combinatorics.finite-choice
 open import univalent-combinatorics.standard-finite-types
+open import univalent-combinatorics.pigeonhole-principle
 open import univalent-combinatorics.subfinitely-enumerable-types
 open import univalent-combinatorics.surjective-maps
 ```
@@ -75,6 +87,21 @@ module _
   is-finitely-enumerable : UU l
   is-finitely-enumerable = type-Prop is-finitely-enumerable-prop
 
+  cardinality-finite-enumeration : finite-enumeration → ℕ
+  cardinality-finite-enumeration (n , _) = n
+
+  surjection-finite-enumeration :
+    (f : finite-enumeration) → Fin (cardinality-finite-enumeration f) ↠ X
+  surjection-finite-enumeration (n , f) = f
+
+  map-finite-enumeration :
+    (f : finite-enumeration) → Fin (cardinality-finite-enumeration f) → X
+  map-finite-enumeration f = map-surjection (surjection-finite-enumeration f)
+
+  is-surjective-finite-enumeration :
+    (f : finite-enumeration) → is-surjective (map-finite-enumeration f)
+  is-surjective-finite-enumeration (n , f) = is-surjective-map-surjection f
+
 Finitely-Enumerable-Type : (l : Level) → UU (lsuc l)
 Finitely-Enumerable-Type l = type-subtype (is-finitely-enumerable-prop {l})
 
@@ -120,6 +147,54 @@ is-finite-is-finitely-enumerable-discrete D eX =
   ∃-surjection-has-decidable-equality-if-is-finite (D , eX)
 ```
 
+We can say more: the cardinality of `X` enumerated by `Fin n` is bounded above
+by `n`. This is a dual
+[pigeonhole principle](univalent-combinatorics.pigeonhole-principle.md).
+
+```agda
+has-section-has-decidable-equality-finite-enumeration :
+  {l : Level} (X : UU l) (eq : has-decidable-equality X)
+  (f : finite-enumeration X) →
+  is-inhabited ((x : X) → fiber (map-finite-enumeration X f) x)
+has-section-has-decidable-equality-finite-enumeration X eq f =
+  finite-choice
+    ( is-finite-is-finitely-enumerable-discrete eq (unit-trunc-Prop f))
+    ( is-surjective-finite-enumeration X f)
+
+has-injective-map-is-upper-bound-finite-enumeration :
+  {l : Level} (X : UU l) (eq : has-decidable-equality X)
+  (f : finite-enumeration X) →
+  exists
+    (X → Fin (cardinality-finite-enumeration X f))
+    (is-injective-Prop (is-set-has-decidable-equality eq))
+has-injective-map-is-upper-bound-finite-enumeration X eq f =
+  rec-trunc-Prop
+    ( ∃
+      ( X → Fin (cardinality-finite-enumeration X f))
+      ( is-injective-Prop (is-set-has-decidable-equality eq)))
+    ( λ g → unit-trunc-Prop
+      ( ( λ x → inclusion-fiber (map-finite-enumeration X f) (g x)) ,
+        ( {!   !})))
+    ( has-section-has-decidable-equality-finite-enumeration X eq f)
+
+is-upper-bound-finite-enumeration :
+  {l : Level} (X : UU l) →
+  (eq : has-decidable-equality X) →
+  (f : finite-enumeration X) →
+  leq-ℕ
+    (number-of-elements-count (count-finite-enumeration-discrete eq f))
+    (cardinality-finite-enumeration X f)
+is-upper-bound-finite-enumeration X eq f =
+  rec-trunc-Prop
+    ( leq-ℕ-Prop
+      ( number-of-elements-count (count-finite-enumeration-discrete eq f))
+      ( cardinality-finite-enumeration X f))
+    ( leq-injection-count
+      ( count-finite-enumeration-discrete eq f)
+      ( count-Fin (cardinality-finite-enumeration X f)))
+    ( has-injective-map-is-upper-bound-finite-enumeration X eq f)
+```
+
 ### Finite types are finitely enumerable
 
 ```agda
diff --git a/src/univalent-combinatorics/pigeonhole-principle.lagda.md b/src/univalent-combinatorics/pigeonhole-principle.lagda.md
index dc8a1e1e99..40cd35cf33 100644
--- a/src/univalent-combinatorics/pigeonhole-principle.lagda.md
+++ b/src/univalent-combinatorics/pigeonhole-principle.lagda.md
@@ -206,6 +206,11 @@ module _
     number-of-elements-count eA ≤-ℕ number-of-elements-count eB
   leq-is-injective-count H =
     leq-is-emb-count (is-emb-is-injective (is-set-count eB) H)
+
+  leq-injection-count :
+    (f : injection A B) →
+    number-of-elements-count eA ≤-ℕ number-of-elements-count eB
+  leq-injection-count (f , inj) = leq-is-injective-count inj
 ```
 
 #### There is no embedding `A ↪ B` between types equipped with a counting if the number of elements of `B` is strictly less than the number of elements of `A`
diff --git a/tables/cyclic-types.md b/tables/cyclic-types.md
index dda8b45bec..5aac89f85e 100644
--- a/tables/cyclic-types.md
+++ b/tables/cyclic-types.md
@@ -1,7 +1,5 @@
 | Concept                                           | File                                                                                                                                            |
 | ------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------- |
-| Acyclic maps                                      | [`synthetic-homotopy-theory.acyclic-maps`](synthetic-homotopy-theory.acyclic-maps.md)                                                           |
-| Acyclic types                                     | [`synthetic-homotopy-theory.acyclic-types`](synthetic-homotopy-theory.acyclic-types.md)                                                         |
 | Acyclic undirected graphs                         | [`graph-theory.acyclic-undirected-graphs`](graph-theory.acyclic-undirected-graphs.md)                                                           |
 | Bracelets                                         | [`univalent-combinatorics.bracelets`](univalent-combinatorics.bracelets.md)                                                                     |
 | The category of cyclic rings                      | [`ring-theory.category-of-cyclic-rings`](ring-theory.category-of-cyclic-rings.md)                                                               |
@@ -15,7 +13,6 @@
 | Euler's totient function                          | [`elementary-number-theory.eulers-totient-function`](elementary-number-theory.eulers-totient-function.md)                                       |
 | Finitely cyclic maps                              | [`elementary-number-theory.finitely-cyclic-maps`](elementary-number-theory.finitely-cyclic-maps.md)                                             |
 | Generating elements of groups                     | [`group-theory.generating-elements-groups`](group-theory.generating-elements-groups.md)                                                         |
-| Hatcher's acyclic type                            | [`synthetic-homotopy-theory.hatchers-acyclic-type`](synthetic-homotopy-theory.hatchers-acyclic-type.md)                                         |
 | Homomorphisms of cyclic rings                     | [`ring-theory.homomorphisms-cyclic-rings`](ring-theory.homomorphisms-cyclic-rings.md)                                                           |
 | Infinite cyclic types                             | [`synthetic-homotopy-theory.infinite-cyclic-types`](synthetic-homotopy-theory.infinite-cyclic-types.md)                                         |
 | Multiplicative units in the standard cyclic rings | [`elementary-number-theory.multiplicative-units-standard-cyclic-rings`](elementary-number-theory.multiplicative-units-standard-cyclic-rings.md) |