Conatural numbers

Content created by Fredrik Bakke.

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

{-# OPTIONS --guardedness #-}

module elementary-number-theory.conatural-numbers where
Imports 
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

Idea

The conatural numbers ℕ∞ is a set that satisfies the dual of the universal property of natural numbers 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

record ℕ∞ : UU lzero
  where
  coinductive
  field
    decons-ℕ∞ : Maybe ℕ∞

open ℕ∞ public

The zero element of the conatural numbers

zero-ℕ∞ : ℕ∞
decons-ℕ∞ zero-ℕ∞ = exception-Maybe

The element at infinity of the conatural numbers

infinity-ℕ∞ : ℕ∞
decons-ℕ∞ infinity-ℕ∞ = unit-Maybe infinity-ℕ∞

The successor function on the conatural numbers

succ-ℕ∞ : ℕ∞ → ℕ∞
decons-ℕ∞ (succ-ℕ∞ x) = unit-Maybe x

The constructor function for conatural numbers

cons-ℕ∞ : Maybe ℕ∞ → ℕ∞
cons-ℕ∞ (inl x) = succ-ℕ∞ x
cons-ℕ∞ (inr x) = zero-ℕ∞

Alternative definition of the deconstructor function for conatural numbers

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

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

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

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

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

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-ℕ∞

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

is-injective-succ-ℕ∞ : is-injective succ-ℕ∞
is-injective-succ-ℕ∞ p = is-injective-inl (is-injective-cons-ℕ∞ p)

Recent changes