The zero conatural number

Content created by Fredrik Bakke.

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

{-# OPTIONS --guardedness #-}

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

Idea

A conatural number x is zero if it does not have a predecessor.

Definitions

The predicate on conatural numbers of being zero

is-zero-ℕ∞ : ℕ∞ → UU lzero
is-zero-ℕ∞ x = is-exception-Maybe (decons-ℕ∞ x)

Properties

Zero is zero

is-zero-zero-ℕ∞ : is-zero-ℕ∞ zero-ℕ∞
is-zero-zero-ℕ∞ = refl

Successors are not zero

is-not-zero-succ-ℕ∞ : (x : ℕ∞) → ¬ (is-zero-ℕ∞ (succ-ℕ∞ x))
is-not-zero-succ-ℕ∞ x ()

The point at infinity is not zero

is-not-zero-infinity-ℕ∞ : ¬ (is-zero-ℕ∞ infinity-ℕ∞)
is-not-zero-infinity-ℕ∞ = is-not-zero-succ-ℕ∞ infinity-ℕ∞

Being zero is decidable

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

is-prop-is-zero-ℕ∞ : (x : ℕ∞) → is-prop (is-zero-ℕ∞ x)
is-prop-is-zero-ℕ∞ = is-prop-is-exception-Maybe ∘ decons-ℕ∞

See also

Recent changes