The universal property of the conatural numbers

Content created by Fredrik Bakke.

Created on 2025-01-04.
Last modified on 2025-01-04.

module elementary-number-theory.universal-property-conatural-numbers where
Imports 
open import foundation.coalgebras-maybe
open import foundation.contractible-types
open import foundation.morphisms-coalgebras-maybe
open import foundation.universe-levels

Idea

The conatural numbers ℕ∞ enjoys many universal properties, among others:

  1. It is the one-point compactification of the natural numbers.
  2. It classifies downward-stable subsets of the natural numbers.
  3. It is the final coalgebra of the maybe monad.

On this page we consider the last of these. Thus, a Maybe-coalgebra η : X → Maybe X satisfies the universal property of the conatural numbers if, for every other Maybe-coalgebra η' : Y → Maybe Y there is a unique coalgebra homomorphism

            f
     Y ----------> X
     |             |
   η'|             | η
     ∨             ∨
  Maybe Y ----> Maybe X.
         Maybe f

Definitions

The universal property of the conatural numbers at a universe level

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

universal-property-conatural-numbers :
  {l1 : Level} → coalgebra-Maybe l1 → UUω
universal-property-conatural-numbers N∞ =
  {l : Level} → universal-property-conatural-numbers-Level N∞ l

Recent changes