Infinite conatural numbers

Content created by Fredrik Bakke.

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

{-# OPTIONS --guardedness #-}

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

Idea

A conatural number x is infinite if it is its own predecessor

  decons-ℕ∞ x ＝ inl x

or, equivalently, if it is its own successor

  x ＝ succ-ℕ∞ x.

Definitions

The predicate on conatural numbers of being infinite

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

is-infinite-infinity-ℕ∞ : is-infinite-ℕ∞ infinity-ℕ∞
is-infinite-infinity-ℕ∞ = refl

The two definitions of being infinite agree

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

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 =

Recent changes