diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
index 135cca7543..aaaa001d05 100644
--- a/src/elementary-number-theory.lagda.md
+++ b/src/elementary-number-theory.lagda.md
@@ -1,5 +1,9 @@
 # Elementary number theory
 
+```agda
+{-# OPTIONS --guardedness #-}
+```
+
 ## Modules in the elementary number theory namespace
 
 ```agda
@@ -27,6 +31,7 @@ open import elementary-number-theory.cofibonacci public
 open import elementary-number-theory.collatz-bijection public
 open import elementary-number-theory.collatz-conjecture public
 open import elementary-number-theory.commutative-semiring-of-natural-numbers public
+open import elementary-number-theory.conatural-numbers public
 open import elementary-number-theory.congruence-integers public
 open import elementary-number-theory.congruence-natural-numbers public
 open import elementary-number-theory.cross-multiplication-difference-integer-fractions public
@@ -66,11 +71,13 @@ open import elementary-number-theory.greatest-common-divisor-natural-numbers pub
 open import elementary-number-theory.group-of-integers public
 open import elementary-number-theory.half-integers public
 open import elementary-number-theory.hardy-ramanujan-number public
+open import elementary-number-theory.inclusion-natural-numbers-conatural-numbers public
 open import elementary-number-theory.inequality-integer-fractions public
 open import elementary-number-theory.inequality-integers public
 open import elementary-number-theory.inequality-natural-numbers public
 open import elementary-number-theory.inequality-rational-numbers public
 open import elementary-number-theory.inequality-standard-finite-types public
+open import elementary-number-theory.infinite-conatural-numbers public
 open import elementary-number-theory.infinitude-of-primes public
 open import elementary-number-theory.initial-segments-natural-numbers public
 open import elementary-number-theory.integer-fractions public
@@ -117,6 +124,7 @@ open import elementary-number-theory.peano-arithmetic public
 open import elementary-number-theory.pisano-periods public
 open import elementary-number-theory.poset-of-natural-numbers-ordered-by-divisibility public
 open import elementary-number-theory.positive-and-negative-integers public
+open import elementary-number-theory.positive-conatural-numbers public
 open import elementary-number-theory.positive-integer-fractions public
 open import elementary-number-theory.positive-integers public
 open import elementary-number-theory.positive-rational-numbers public
@@ -158,9 +166,11 @@ open import elementary-number-theory.twin-prime-conjecture public
 open import elementary-number-theory.type-arithmetic-natural-numbers public
 open import elementary-number-theory.unit-elements-standard-finite-types public
 open import elementary-number-theory.unit-similarity-standard-finite-types public
+open import elementary-number-theory.universal-property-conatural-numbers public
 open import elementary-number-theory.universal-property-integers public
 open import elementary-number-theory.universal-property-natural-numbers public
 open import elementary-number-theory.upper-bounds-natural-numbers public
 open import elementary-number-theory.well-ordering-principle-natural-numbers public
 open import elementary-number-theory.well-ordering-principle-standard-finite-types public
+open import elementary-number-theory.zero-conatural-numbers public
 ```
diff --git a/src/elementary-number-theory/conatural-numbers.lagda.md b/src/elementary-number-theory/conatural-numbers.lagda.md
new file mode 100644
index 0000000000..79ae6d05b3
--- /dev/null
+++ b/src/elementary-number-theory/conatural-numbers.lagda.md
@@ -0,0 +1,172 @@
+# Conatural numbers
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module elementary-number-theory.conatural-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.homotopies
+open import foundation.injective-maps
+open import foundation.maybe
+open import foundation.negated-equality
+open import foundation.retractions
+open import foundation.sections
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+The {{#concept "conatural numbers" Agda=ℕ∞}} `ℕ∞` is a
+[set](foundation-core.sets.md) that satisfies the dual of the universal property
+of [natural numbers](elementary-number-theory.natural-numbers.md) in the sense
+that it is the final coalgebra of the functor `X ↦ 1 + X` rather than the
+initial algebra.
+
+## Definitions
+
+### The coinductive type of conatural numbers
+
+```agda
+record ℕ∞ : UU lzero
+  where
+  coinductive
+  field
+    decons-ℕ∞ : Maybe ℕ∞
+
+open ℕ∞ public
+```
+
+### The zero element of the conatural numbers
+
+```agda
+zero-ℕ∞ : ℕ∞
+decons-ℕ∞ zero-ℕ∞ = exception-Maybe
+```
+
+### The element at infinity of the conatural numbers
+
+```agda
+infinity-ℕ∞ : ℕ∞
+decons-ℕ∞ infinity-ℕ∞ = unit-Maybe infinity-ℕ∞
+```
+
+### The successor function on the conatural numbers
+
+```agda
+succ-ℕ∞ : ℕ∞ → ℕ∞
+decons-ℕ∞ (succ-ℕ∞ x) = unit-Maybe x
+```
+
+### The constructor function for conatural numbers
+
+```agda
+cons-ℕ∞ : Maybe ℕ∞ → ℕ∞
+cons-ℕ∞ (inl x) = succ-ℕ∞ x
+cons-ℕ∞ (inr x) = zero-ℕ∞
+```
+
+### Alternative definition of the deconstructor function for conatural numbers
+
+```agda
+decons-ℕ∞' : ℕ∞ → Maybe ℕ∞
+decons-ℕ∞' x = rec-coproduct inl inr (decons-ℕ∞ x)
+
+compute-decons-ℕ∞ : decons-ℕ∞' ~ decons-ℕ∞
+compute-decons-ℕ∞ x with decons-ℕ∞ x
+compute-decons-ℕ∞ x | inl q = refl
+compute-decons-ℕ∞ x | inr q = refl
+```
+
+### The coiterator function for conatural numbers
+
+```agda
+coit-ℕ∞ : {l : Level} {A : UU l} → (A → Maybe A) → A → ℕ∞
+decons-ℕ∞ (coit-ℕ∞ f x) with f x
+decons-ℕ∞ (coit-ℕ∞ f x) | inl a = unit-Maybe (coit-ℕ∞ f a)
+decons-ℕ∞ (coit-ℕ∞ f x) | inr _ = exception-Maybe
+```
+
+### The corecursor function for conatural numbers
+
+```agda
+corec-ℕ∞ : {l : Level} {A : UU l} → (A → ℕ∞ + Maybe A) → A → ℕ∞
+decons-ℕ∞ (corec-ℕ∞ f x) with f x
+decons-ℕ∞ (corec-ℕ∞ f x) | inl q = unit-Maybe q
+decons-ℕ∞ (corec-ℕ∞ f x) | inr (inl a) = unit-Maybe (corec-ℕ∞ f a)
+decons-ℕ∞ (corec-ℕ∞ f x) | inr (inr *) = inr *
+```
+
+## Properties
+
+### Zero is not a successor
+
+```agda
+neq-zero-succ-ℕ∞ : (x : ℕ∞) → succ-ℕ∞ x ≠ zero-ℕ∞
+neq-zero-succ-ℕ∞ x p = is-not-exception-unit-Maybe x (ap decons-ℕ∞ p)
+```
+
+### Zero is not the point at infinity
+
+```agda
+neq-zero-infinity-ℕ∞ : infinity-ℕ∞ ≠ zero-ℕ∞
+neq-zero-infinity-ℕ∞ p =
+  is-not-exception-unit-Maybe infinity-ℕ∞ (ap decons-ℕ∞ p)
+
+neq-infinity-zero-ℕ∞ : zero-ℕ∞ ≠ infinity-ℕ∞
+neq-infinity-zero-ℕ∞ =
+  is-symmetric-nonequal infinity-ℕ∞ zero-ℕ∞ neq-zero-infinity-ℕ∞
+```
+
+### The constructor function is a section of the deconstructor
+
+```agda
+is-section-cons-ℕ∞ : is-section decons-ℕ∞ cons-ℕ∞
+is-section-cons-ℕ∞ (inl x) = refl
+is-section-cons-ℕ∞ (inr x) = refl
+
+section-decons-ℕ∞ : section decons-ℕ∞
+section-decons-ℕ∞ = cons-ℕ∞ , is-section-cons-ℕ∞
+
+retraction-cons-ℕ∞ : retraction cons-ℕ∞
+retraction-cons-ℕ∞ = decons-ℕ∞ , is-section-cons-ℕ∞
+
+is-injective-cons-ℕ∞ : is-injective cons-ℕ∞
+is-injective-cons-ℕ∞ = is-injective-retraction cons-ℕ∞ retraction-cons-ℕ∞
+```
+
+```agda
+is-section-cons-ℕ∞' : is-section decons-ℕ∞' cons-ℕ∞
+is-section-cons-ℕ∞' (inl x) = refl
+is-section-cons-ℕ∞' (inr x) = refl
+
+section-decons-ℕ∞' : section decons-ℕ∞'
+section-decons-ℕ∞' = cons-ℕ∞ , is-section-cons-ℕ∞'
+
+retraction-cons-ℕ∞' : retraction cons-ℕ∞
+retraction-cons-ℕ∞' = decons-ℕ∞' , is-section-cons-ℕ∞'
+```
+
+### The successor function is injective
+
+```agda
+is-injective-succ-ℕ∞ : is-injective succ-ℕ∞
+is-injective-succ-ℕ∞ p = is-injective-inl (is-injective-cons-ℕ∞ p)
+```
+
+## External links
+
+- [CoNaturals](https://martinescardo.github.io/TypeTopology/CoNaturals.index.html)
+  at TypeTopology
+- [extended natural numbers](https://ncatlab.org/nlab/show/extended+natural+number)
+  at $n$Lab
diff --git a/src/elementary-number-theory/inclusion-natural-numbers-conatural-numbers.lagda.md b/src/elementary-number-theory/inclusion-natural-numbers-conatural-numbers.lagda.md
new file mode 100644
index 0000000000..d4e985773f
--- /dev/null
+++ b/src/elementary-number-theory/inclusion-natural-numbers-conatural-numbers.lagda.md
@@ -0,0 +1,82 @@
+# The inclusion of the natural numbers into the conatural numbers
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module elementary-number-theory.inclusion-natural-numbers-conatural-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.conatural-numbers
+open import elementary-number-theory.infinite-conatural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.existential-quantification
+open import foundation.injective-maps
+open import foundation.negated-equality
+open import foundation.negation
+open import foundation.surjective-maps
+
+open import foundation-core.empty-types
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "inclusion of the nautural numbers into the conatural numbers" Agda=ℕ∞}}
+is the inductively defined map
+
+```text
+  conatural-ℕ : ℕ → ℕ∞
+```
+
+that sends zero to zero, and the successor of a natural number to the successor
+of its inclusion.
+
+## Definitions
+
+### The canonical inclusion of the natural numbers into the conatural numbers
+
+```agda
+conatural-ℕ : ℕ → ℕ∞
+conatural-ℕ zero-ℕ = zero-ℕ∞
+conatural-ℕ (succ-ℕ x) = succ-ℕ∞ (conatural-ℕ x)
+```
+
+## Properties
+
+### The canonical inclusion of the natural numbers is injective
+
+```agda
+is-injective-conatural-ℕ : is-injective conatural-ℕ
+is-injective-conatural-ℕ {zero-ℕ} {zero-ℕ} p = refl
+is-injective-conatural-ℕ {zero-ℕ} {succ-ℕ y} p =
+  ex-falso (neq-zero-succ-ℕ∞ (conatural-ℕ y) (inv p))
+is-injective-conatural-ℕ {succ-ℕ x} {zero-ℕ} p =
+  ex-falso (neq-zero-succ-ℕ∞ (conatural-ℕ x) p)
+is-injective-conatural-ℕ {succ-ℕ x} {succ-ℕ y} p =
+  ap succ-ℕ (is-injective-conatural-ℕ {x} {y} (is-injective-succ-ℕ∞ p))
+```
+
+### The canonical inclusion of the natural numbers is not surjective
+
+The canonical inclusion of the natural numbers is not surjective because it does
+not hit the point at infinity.
+
+```text
+neq-infinity-conatural-ℕ : (n : ℕ) → conatural-ℕ n ≠ infinity-ℕ∞
+neq-infinity-conatural-ℕ zero-ℕ = neq-infinity-zero-ℕ∞
+neq-infinity-conatural-ℕ (succ-ℕ n) p =
+  neq-infinity-conatural-ℕ n
+    ( is-injective-succ-ℕ∞ (p ∙ {! is-infinite-successor-condition-infinity-ℕ∞  !}))
+
+is-not-surjective-conatural-ℕ : ¬ (is-surjective conatural-ℕ)
+is-not-surjective-conatural-ℕ H =
+  elim-exists empty-Prop neq-infinity-conatural-ℕ (H infinity-ℕ∞)
+```
diff --git a/src/elementary-number-theory/infinite-conatural-numbers.lagda.md b/src/elementary-number-theory/infinite-conatural-numbers.lagda.md
new file mode 100644
index 0000000000..6718c3413d
--- /dev/null
+++ b/src/elementary-number-theory/infinite-conatural-numbers.lagda.md
@@ -0,0 +1,92 @@
+# Infinite conatural numbers
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module elementary-number-theory.infinite-conatural-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.conatural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.coproduct-types
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+A [conatural number](elementary-number-theory.conatural-numbers.md) `x` is
+{{#concept "infinite" Disambiguation="conatural number" Agda=is-infinite-successor-condition-ℕ∞}}
+if it is its own predecessor
+
+```text
+  decons-ℕ∞ x ＝ inl x
+```
+
+or, [equivalently](foundation-core.equivalences.md), if it is its own successor
+
+```text
+  x ＝ succ-ℕ∞ x.
+```
+
+## Definitions
+
+### The predicate on conatural numbers of being infinite
+
+```agda
+is-infinite-ℕ∞ : ℕ∞ → UU lzero
+is-infinite-ℕ∞ x = decons-ℕ∞ x ＝ inl x
+
+is-infinite-successor-condition-ℕ∞ : ℕ∞ → UU lzero
+is-infinite-successor-condition-ℕ∞ x = x ＝ succ-ℕ∞ x
+```
+
+## Properties
+
+### The point at infinity is infinite
+
+```agda
+is-infinite-infinity-ℕ∞ : is-infinite-ℕ∞ infinity-ℕ∞
+is-infinite-infinity-ℕ∞ = refl
+```
+
+### The two definitions of being infinite agree
+
+```agda
+is-infinite-is-infinite-successor-condition-ℕ∞ :
+  (x : ℕ∞) → is-infinite-successor-condition-ℕ∞ x → is-infinite-ℕ∞ x
+is-infinite-is-infinite-successor-condition-ℕ∞ x = ap decons-ℕ∞
+
+is-infinite-successor-condition-cons-is-infinite-cons-ℕ∞ :
+  (x : ℕ∞) →
+  is-infinite-ℕ∞ (cons-ℕ∞ (decons-ℕ∞ x)) →
+  is-infinite-successor-condition-ℕ∞ (cons-ℕ∞ (decons-ℕ∞ x))
+is-infinite-successor-condition-cons-is-infinite-cons-ℕ∞ x =
+  ind-coproduct
+    ( λ y →
+      is-infinite-ℕ∞ (cons-ℕ∞ y) →
+      is-infinite-successor-condition-ℕ∞ (cons-ℕ∞ y))
+    ( λ x' → ap cons-ℕ∞)
+    ( λ x' → ap cons-ℕ∞)
+    ( decons-ℕ∞ x)
+```
+
+> It remains to formalize the full equivalence.
+
+### The point at infinity is unique
+
+```text
+eq-is-infinite-successor-condition-ℕ∞ :
+  (x y : ℕ∞) →
+  is-infinite-successor-condition-ℕ∞ x →
+  is-infinite-successor-condition-ℕ∞ y →
+  x ＝ y
+eq-is-infinite-successor-condition-ℕ∞ x y p q =
+```
diff --git a/src/elementary-number-theory/positive-conatural-numbers.lagda.md b/src/elementary-number-theory/positive-conatural-numbers.lagda.md
new file mode 100644
index 0000000000..d50eb34f27
--- /dev/null
+++ b/src/elementary-number-theory/positive-conatural-numbers.lagda.md
@@ -0,0 +1,90 @@
+# Positive conatural numbers
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module elementary-number-theory.positive-conatural-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.conatural-numbers
+open import elementary-number-theory.zero-conatural-numbers
+
+open import foundation.coproduct-types
+open import foundation.decidable-types
+open import foundation.dependent-pair-types
+open import foundation.maybe
+open import foundation.negation
+open import foundation.universe-levels
+
+open import foundation-core.empty-types
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+A [conatural number](elementary-number-theory.conatural-numbers.md) `x` is
+{{#concept "positive" Disambiguation="conatural number" Agda=is-positive-ℕ∞}} if
+it has a predecessor. In other words, if it is not
+[zero](elementary-number-theory.zero-conatural-numbers.md).
+
+## Definitions
+
+### The predicate on conatural numbers of being positive
+
+```agda
+is-positive-ℕ∞ : ℕ∞ → UU lzero
+is-positive-ℕ∞ x = is-value-Maybe (decons-ℕ∞ x)
+```
+
+## Properties
+
+### Zero is not positive
+
+```agda
+is-not-positive-zero-ℕ∞ : ¬ (is-positive-ℕ∞ zero-ℕ∞)
+is-not-positive-zero-ℕ∞ ()
+```
+
+### Successors are positive
+
+```agda
+is-positive-succ-ℕ∞ : (x : ℕ∞) → is-positive-ℕ∞ (succ-ℕ∞ x)
+is-positive-succ-ℕ∞ x = x , refl
+```
+
+### The point at infinity is positive
+
+```agda
+is-positive-infinity-ℕ∞ : is-positive-ℕ∞ infinity-ℕ∞
+is-positive-infinity-ℕ∞ = is-positive-succ-ℕ∞ infinity-ℕ∞
+```
+
+### Positivity is decidable
+
+```agda
+is-decidable-is-positive-ℕ∞ : (x : ℕ∞) → is-decidable (is-positive-ℕ∞ x)
+is-decidable-is-positive-ℕ∞ x with decons-ℕ∞ x
+is-decidable-is-positive-ℕ∞ x | inl y = inl (is-positive-succ-ℕ∞ y)
+is-decidable-is-positive-ℕ∞ x | inr _ = inr is-not-positive-zero-ℕ∞
+```
+
+### A conatural number is positive if and only if it is nonzero
+
+```agda
+is-positive-is-not-zero-ℕ∞ : (x : ℕ∞) → ¬ (is-zero-ℕ∞ x) → is-positive-ℕ∞ x
+is-positive-is-not-zero-ℕ∞ x H with decons-ℕ∞ x
+is-positive-is-not-zero-ℕ∞ x H | inl y = y , refl
+is-positive-is-not-zero-ℕ∞ x H | inr * = ex-falso (H refl)
+
+is-not-zero-is-positive-ℕ∞ : (x : ℕ∞) → is-positive-ℕ∞ x → ¬ (is-zero-ℕ∞ x)
+is-not-zero-is-positive-ℕ∞ x = is-not-exception-is-value-Maybe (decons-ℕ∞ x)
+```
+
+## See also
+
+- [Infinite conatural numbers](elementary-number-theory.infinite-conatural-numbers.md)
diff --git a/src/elementary-number-theory/universal-property-conatural-numbers.lagda.md b/src/elementary-number-theory/universal-property-conatural-numbers.lagda.md
new file mode 100644
index 0000000000..c593269a23
--- /dev/null
+++ b/src/elementary-number-theory/universal-property-conatural-numbers.lagda.md
@@ -0,0 +1,64 @@
+# The universal property of the conatural numbers
+
+```agda
+module elementary-number-theory.universal-property-conatural-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.coalgebras-maybe
+open import foundation.contractible-types
+open import foundation.morphisms-coalgebras-maybe
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+The [conatural numbers](elementary-number-theory.conatural-numbers.md) `ℕ∞`
+enjoys many universal properties, among others:
+
+1. It is the one-point compactification of the
+   [natural numbers](elementary-number-theory.natural-numbers.md).
+2. It classifies downward-stable subsets of the natural numbers.
+3. It is the final coalgebra of the [maybe monad](foundation.maybe.md).
+
+On this page we consider the last of these. Thus, a
+`Maybe`-[coalgebra](foundation.coalgebras-maybe.md) `η : X → Maybe X` satisfies
+the
+{{#concept "universal property of the conatural numbers" Agda=universal-property-conatural-numbers}}
+if, for every other `Maybe`-coalgebra `η' : Y → Maybe Y` there is a
+[unique](foundation-core.contractible-types.md)
+[coalgebra homomorphism](foundation.morphisms-coalgebras-maybe.md)
+
+```text
+            f
+     Y ----------> X
+     |             |
+   η'|             | η
+     ∨             ∨
+  Maybe Y ----> Maybe X.
+         Maybe f
+```
+
+## Definitions
+
+### The universal property of the conatural numbers at a universe level
+
+```agda
+universal-property-conatural-numbers-Level :
+  {l1 : Level} → coalgebra-Maybe l1 → (l : Level) → UU (l1 ⊔ lsuc l)
+universal-property-conatural-numbers-Level N∞ l =
+  (X : coalgebra-Maybe l) → is-contr (hom-coalgebra-Maybe X N∞)
+```
+
+### The universal property of the conatural numbers at a universe level
+
+```agda
+universal-property-conatural-numbers :
+  {l1 : Level} → coalgebra-Maybe l1 → UUω
+universal-property-conatural-numbers N∞ =
+  {l : Level} → universal-property-conatural-numbers-Level N∞ l
+```
diff --git a/src/elementary-number-theory/zero-conatural-numbers.lagda.md b/src/elementary-number-theory/zero-conatural-numbers.lagda.md
new file mode 100644
index 0000000000..ea40798173
--- /dev/null
+++ b/src/elementary-number-theory/zero-conatural-numbers.lagda.md
@@ -0,0 +1,84 @@
+# The zero conatural number
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module elementary-number-theory.zero-conatural-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.conatural-numbers
+
+open import foundation.coproduct-types
+open import foundation.decidable-types
+open import foundation.function-types
+open import foundation.maybe
+open import foundation.negation
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+open import foundation-core.propositions
+```
+
+</details>
+
+## Idea
+
+A [conatural number](elementary-number-theory.conatural-numbers.md) `x` is
+{{#concept "zero" Disambiguation="conatural number" Agda=is-zero-ℕ∞}} if it does
+not have a predecessor.
+
+## Definitions
+
+### The predicate on conatural numbers of being zero
+
+```agda
+is-zero-ℕ∞ : ℕ∞ → UU lzero
+is-zero-ℕ∞ x = is-exception-Maybe (decons-ℕ∞ x)
+```
+
+## Properties
+
+### Zero is zero
+
+```agda
+is-zero-zero-ℕ∞ : is-zero-ℕ∞ zero-ℕ∞
+is-zero-zero-ℕ∞ = refl
+```
+
+### Successors are not zero
+
+```agda
+is-not-zero-succ-ℕ∞ : (x : ℕ∞) → ¬ (is-zero-ℕ∞ (succ-ℕ∞ x))
+is-not-zero-succ-ℕ∞ x ()
+```
+
+### The point at infinity is not zero
+
+```agda
+is-not-zero-infinity-ℕ∞ : ¬ (is-zero-ℕ∞ infinity-ℕ∞)
+is-not-zero-infinity-ℕ∞ = is-not-zero-succ-ℕ∞ infinity-ℕ∞
+```
+
+### Being zero is decidable
+
+```agda
+is-decidable-is-zero-ℕ∞ : (x : ℕ∞) → is-decidable (is-zero-ℕ∞ x)
+is-decidable-is-zero-ℕ∞ x with decons-ℕ∞ x
+is-decidable-is-zero-ℕ∞ x | inl y = inr (is-not-zero-succ-ℕ∞ y)
+is-decidable-is-zero-ℕ∞ x | inr * = inl is-zero-zero-ℕ∞
+```
+
+### Being zero is a property
+
+```agda
+is-prop-is-zero-ℕ∞ : (x : ℕ∞) → is-prop (is-zero-ℕ∞ x)
+is-prop-is-zero-ℕ∞ = is-prop-is-exception-Maybe ∘ decons-ℕ∞
+```
+
+## See also
+
+- [Positive conatural numbers](elementary-number-theory.positive-conatural-numbers.md)
+- [Infinite conatural numbers](elementary-number-theory.infinite-conatural-numbers.md)
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 8d049c7d4c..a37fa70f98 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -55,6 +55,7 @@ open import foundation.cartesian-products-set-quotients public
 open import foundation.category-of-families-of-sets public
 open import foundation.category-of-sets public
 open import foundation.choice-of-representatives-equivalence-relation public
+open import foundation.coalgebras-maybe public
 open import foundation.codiagonal-maps-of-types public
 open import foundation.coherently-idempotent-maps public
 open import foundation.coherently-invertible-maps public
@@ -276,6 +277,7 @@ open import foundation.mere-path-cosplit-maps public
 open import foundation.monomorphisms public
 open import foundation.morphisms-arrows public
 open import foundation.morphisms-binary-relations public
+open import foundation.morphisms-coalgebras-maybe public
 open import foundation.morphisms-cospan-diagrams public
 open import foundation.morphisms-cospans public
 open import foundation.morphisms-double-arrows public
diff --git a/src/foundation/coalgebras-maybe.lagda.md b/src/foundation/coalgebras-maybe.lagda.md
new file mode 100644
index 0000000000..855690a002
--- /dev/null
+++ b/src/foundation/coalgebras-maybe.lagda.md
@@ -0,0 +1,53 @@
+# Coalgebras of the maybe monad
+
+```agda
+module foundation.coalgebras-maybe where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.maybe
+open import foundation.universe-levels
+
+open import trees.polynomial-endofunctors
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "coalgebra" Disambiguation="of the maybe monad" Agda=coalgebra-Maybe}}
+is a type `X` [equipped](foundation.structure.md) with a map
+
+```text
+  X → Maybe X.
+```
+
+## Definitions
+
+### Maybe-coalgebra structure on a type
+
+```agda
+coalgebra-structure-Maybe : {l : Level} → UU l → UU l
+coalgebra-structure-Maybe X = X → Maybe X
+```
+
+### Maybe-coalgebras
+
+```agda
+coalgebra-Maybe : (l : Level) → UU (lsuc l)
+coalgebra-Maybe l = Σ (UU l) (coalgebra-structure-Maybe)
+
+module _
+  {l : Level} (X : coalgebra-Maybe l)
+  where
+
+  type-coalgebra-Maybe : UU l
+  type-coalgebra-Maybe = pr1 X
+
+  map-coalgebra-Maybe : type-coalgebra-Maybe → Maybe type-coalgebra-Maybe
+  map-coalgebra-Maybe = pr2 X
+```
diff --git a/src/foundation/maybe.lagda.md b/src/foundation/maybe.lagda.md
index 88c74894d2..eb0267724d 100644
--- a/src/foundation/maybe.lagda.md
+++ b/src/foundation/maybe.lagda.md
@@ -26,6 +26,7 @@ open import foundation-core.equivalences
 open import foundation-core.identity-types
 open import foundation-core.injective-maps
 open import foundation-core.negation
+open import foundation-core.propositions
 open import foundation-core.retractions
 open import foundation-core.sections
 ```
@@ -87,6 +88,12 @@ is-exception-Maybe {l} {X} x = (x ＝ exception-Maybe)
 
 is-not-exception-Maybe : {l : Level} {X : UU l} → Maybe X → UU l
 is-not-exception-Maybe x = ¬ (is-exception-Maybe x)
+
+is-prop-is-exception-Maybe :
+  {l : Level} {X : UU l} (x : Maybe X) → is-prop (is-exception-Maybe x)
+is-prop-is-exception-Maybe (inl x) ()
+is-prop-is-exception-Maybe (inr x) =
+  is-prop-equiv (compute-eq-coproduct-inr-inr x star) (is-set-unit x star)
 ```
 
 ### The predicate of being a value
@@ -131,19 +138,23 @@ abstract
   is-injective-unit-Maybe = is-injective-inl
 ```
 
-### Being an exception is decidable
+### Being an exception is a decidable proposition
 
 ```agda
-is-decidable-is-exception-Maybe :
-  {l : Level} {X : UU l} (x : Maybe X) → is-decidable (is-exception-Maybe x)
-is-decidable-is-exception-Maybe {l} {X} (inl x) =
-  inr (λ p → ex-falso (is-empty-eq-coproduct-inl-inr x star p))
-is-decidable-is-exception-Maybe (inr star) = inl refl
-
-is-decidable-is-not-exception-Maybe :
-  {l : Level} {X : UU l} (x : Maybe X) → is-decidable (is-not-exception-Maybe x)
-is-decidable-is-not-exception-Maybe x =
-  is-decidable-neg (is-decidable-is-exception-Maybe x)
+module _
+  {l : Level} {X : UU l}
+  where
+
+  is-decidable-is-exception-Maybe :
+    (x : Maybe X) → is-decidable (is-exception-Maybe x)
+  is-decidable-is-exception-Maybe (inl x) =
+    inr (λ p → ex-falso (is-empty-eq-coproduct-inl-inr x star p))
+  is-decidable-is-exception-Maybe (inr star) = inl refl
+
+  is-decidable-is-not-exception-Maybe :
+    (x : Maybe X) → is-decidable (is-not-exception-Maybe x)
+  is-decidable-is-not-exception-Maybe x =
+    is-decidable-neg (is-decidable-is-exception-Maybe x)
 ```
 
 ### The values of the unit of the `Maybe` monad are not exceptions
@@ -152,7 +163,19 @@ is-decidable-is-not-exception-Maybe x =
 abstract
   is-not-exception-unit-Maybe :
     {l : Level} {X : UU l} (x : X) → is-not-exception-Maybe (unit-Maybe x)
-  is-not-exception-unit-Maybe {l} {X} x ()
+  is-not-exception-unit-Maybe x ()
+```
+
+### The unit of `Maybe` is not surjective
+
+```agda
+abstract
+  is-not-surjective-unit-Maybe :
+    {l : Level} {X : UU l} → ¬ (is-surjective (unit-Maybe {X = X}))
+  is-not-surjective-unit-Maybe H =
+    rec-trunc-Prop empty-Prop
+      ( λ p → is-not-exception-unit-Maybe (pr1 p) (pr2 p))
+      ( H exception-Maybe)
 ```
 
 ### For any element of type `Maybe X` we can decide whether it is a value or an exception
diff --git a/src/foundation/morphisms-coalgebras-maybe.lagda.md b/src/foundation/morphisms-coalgebras-maybe.lagda.md
new file mode 100644
index 0000000000..356b8eba5b
--- /dev/null
+++ b/src/foundation/morphisms-coalgebras-maybe.lagda.md
@@ -0,0 +1,72 @@
+# Morphisms of coalgebras of the maybe monad
+
+```agda
+module foundation.morphisms-coalgebras-maybe where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.coalgebras-maybe
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.maybe
+open import foundation.universe-levels
+
+open import trees.polynomial-endofunctors
+```
+
+</details>
+
+## Idea
+
+Given two [coalgebras](foundation.coalgebras-maybe.md) of the
+[maybe monad](foundation.maybe.md) `η : X → Maybe X`, `η' : Y → Maybe Y`, then a
+map `f : X → Y` is a
+{{#concept "morphism of coalgebras" Disambiguation="of the maybe monad" Agda=hom-coalgebra-Maybe}}
+if the square
+
+```text
+            f
+     X ----------> Y
+     |             |
+     |             |
+     ∨             ∨
+  Maybe X ----> Maybe Y
+         Maybe f
+```
+
+[commutes](foundation.commuting-squares-of-maps.md).
+
+## Definitions
+
+```agda
+coherence-hom-coalgebra-Maybe :
+  {l1 l2 : Level} (X : coalgebra-Maybe l1) (Y : coalgebra-Maybe l2) →
+  (type-coalgebra-Maybe X → type-coalgebra-Maybe Y) → UU (l1 ⊔ l2)
+coherence-hom-coalgebra-Maybe X Y f =
+  coherence-square-maps
+    ( f)
+    ( map-coalgebra-Maybe X)
+    ( map-coalgebra-Maybe Y)
+    ( map-Maybe f)
+
+hom-coalgebra-Maybe :
+  {l1 l2 : Level} (X : coalgebra-Maybe l1) (Y : coalgebra-Maybe l2) →
+  UU (l1 ⊔ l2)
+hom-coalgebra-Maybe X Y =
+  Σ ( type-coalgebra-Maybe X → type-coalgebra-Maybe Y)
+    ( coherence-hom-coalgebra-Maybe X Y)
+
+module _
+  {l1 l2 : Level} (X : coalgebra-Maybe l1) (Y : coalgebra-Maybe l2)
+  (f : hom-coalgebra-Maybe X Y)
+  where
+
+  map-hom-coalgebra-Maybe : type-coalgebra-Maybe X → type-coalgebra-Maybe Y
+  map-hom-coalgebra-Maybe = pr1 f
+
+  coh-hom-coalgebra-Maybe :
+    coherence-hom-coalgebra-Maybe X Y map-hom-coalgebra-Maybe
+  coh-hom-coalgebra-Maybe = pr2 f
+```
diff --git a/src/foundation/noncontractible-types.lagda.md b/src/foundation/noncontractible-types.lagda.md
index 537377c85d..98d2d49311 100644
--- a/src/foundation/noncontractible-types.lagda.md
+++ b/src/foundation/noncontractible-types.lagda.md
@@ -10,21 +10,33 @@ module foundation.noncontractible-types where
 open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.inhabited-types
 open import foundation.universe-levels
 
 open import foundation-core.contractible-types
-open import foundation-core.empty-types
 open import foundation-core.function-types
 open import foundation-core.identity-types
 open import foundation-core.negation
+open import foundation-core.propositions
 ```
 
 </details>
 
 ## Idea
 
-A type `X` is noncontractible if it comes equipped with an element of type
-`¬ (is-contr X)`.
+_Noncontractibility_ is a positive way of stating that a type is
+[not](foundation.negation.md)
+[contractible](foundation-core.contractible-types.md). A type `A` is
+{{#concept "noncontractible" Agda=is-noncontractible}} if it is
+[empty](foundation.empty-types.md), or, inductively, if there
+[exists](foundation.existential-quantification.md) two elements `x y : A` whose
+[identity type](foundation-core.identity-types.md) `x ＝ y` is noncontractible.
+More specifically, we may say `A` has an
+$n$-{{#concept "noncontractibility" Agda=noncontractibility'}} if there are
+$n$-identifications `p` and `q` in `A` such that `p ≠ q`. When a type is
+noncontractible in this sense, it is [apart](foundation.apartness-relations.md)
+from the [unit type](foundation.unit-type.md).
 
 ## Definitions
 
@@ -35,20 +47,35 @@ is-not-contractible : {l : Level} → UU l → UU l
 is-not-contractible X = ¬ (is-contr X)
 ```
 
-### A positive formulation of being noncontractible
+### Noncontractibilities of a type
 
-Noncontractibility is a more positive way to prove that a type is not
-contractible. When `A` is noncontractible in the following sense, then it is
-apart from the unit type.
+```agda
+noncontractibility' : {l : Level} → UU l → ℕ → UU l
+noncontractibility' A zero-ℕ = is-empty A
+noncontractibility' A (succ-ℕ k) =
+  Σ A (λ x → Σ A (λ y → noncontractibility' (x ＝ y) k))
+
+noncontractibility : {l : Level} → UU l → UU l
+noncontractibility A = Σ ℕ (noncontractibility' A)
+```
+
+### The property of being noncontractible
 
 ```agda
-is-noncontractible' : {l : Level} (A : UU l) → ℕ → UU l
+is-noncontractible' : {l : Level} → UU l → ℕ → UU l
 is-noncontractible' A zero-ℕ = is-empty A
-is-noncontractible' A (succ-ℕ k) =
-  Σ A (λ x → Σ A (λ y → is-noncontractible' (x ＝ y) k))
+is-noncontractible' A (succ-ℕ n) =
+  is-inhabited (noncontractibility' A (succ-ℕ n))
+
+is-prop-is-noncontractible' :
+  {l : Level} {A : UU l} {n : ℕ} → is-prop (is-noncontractible' A n)
+is-prop-is-noncontractible' {n = zero-ℕ} = is-property-is-empty
+is-prop-is-noncontractible' {n = succ-ℕ n} = is-property-is-inhabited _
+```
 
-is-noncontractible : {l : Level} (A : UU l) → UU l
-is-noncontractible A = Σ ℕ (is-noncontractible' A)
+```agda
+is-noncontractible : {l : Level} → UU l → UU l
+is-noncontractible A = is-inhabited (noncontractibility A)
 ```
 
 ## Properties
@@ -62,15 +89,34 @@ is-not-contractible-is-empty H C = H (center C)
 
 is-not-contractible-empty : is-not-contractible empty
 is-not-contractible-empty = is-not-contractible-is-empty id
+
+noncontractibility-is-empty :
+  {l : Level} {X : UU l} → is-empty X → noncontractibility X
+noncontractibility-is-empty H = 0 , H
+
+noncontractibility-empty : noncontractibility empty
+noncontractibility-empty = 0 , id
 ```
 
 ### Noncontractible types are not contractible
 
 ```agda
-is-not-contractible-is-noncontractible :
-  {l : Level} {X : UU l} → is-noncontractible X → is-not-contractible X
-is-not-contractible-is-noncontractible
-  ( pair zero-ℕ H) = is-not-contractible-is-empty H
-is-not-contractible-is-noncontractible (pair (succ-ℕ n) (pair x (pair y H))) C =
-  is-not-contractible-is-noncontractible (pair n H) (is-prop-is-contr C x y)
+is-not-contractible-noncontractibility :
+  {l : Level} {X : UU l} → noncontractibility X → is-not-contractible X
+is-not-contractible-noncontractibility (zero-ℕ , H) =
+  is-not-contractible-is-empty H
+is-not-contractible-noncontractibility (succ-ℕ n , x , y , H) C =
+  is-not-contractible-noncontractibility (n , H) (is-prop-is-contr C x y)
 ```
+
+## Comments
+
+The dimension of noncontractibility of a type is not unique. For instance,
+consider the disjoint sum of the unit type and the
+[circle](synthetic-homotopy-theory.circle.md) `1 + 𝕊¹`. This type has a
+1-noncontractibility as the two base points are not equal, but it also has a
+2-noncontractiblity between the reflexivity at the basepoint of the circle and
+the free loop. In fact, the free fixed point of the operation `1 + Σ(-)`, where
+`Σ` is the
+[suspension operator](synthetic-homotopy-theory.suspensions-of-types.md), is
+$n$-noncontractible for every $n ≥ 1$.
diff --git a/src/polytopes/abstract-polytopes.lagda.md b/src/polytopes/abstract-polytopes.lagda.md
index 159269c933..85a5bacfab 100644
--- a/src/polytopes/abstract-polytopes.lagda.md
+++ b/src/polytopes/abstract-polytopes.lagda.md
@@ -7,7 +7,8 @@ module polytopes.abstract-polytopes where
 <details><summary>Imports</summary>
 
 ```agda
-open import elementary-number-theory
+open import elementary-number-theory.inequality-standard-finite-types
+open import elementary-number-theory.natural-numbers
 
 open import foundation.binary-relations
 open import foundation.cartesian-product-types