Acyclic types are inhabited

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
+```

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
+```

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
@@ -873,6 +874,18 @@ module _
     is-inhabited-is-surjective (is-surjective-map-surjection f)
 ```
 
+### When `X` is empty and `X` surjects onto `Y`, then `Y` is empty
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (emp-A : is-empty A)
+  where
+
+  is-empty-surjection-empty : A ↠ B → is-empty B
+  is-empty-surjection-empty (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.

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