Positive conatural numbers

Content created by Fredrik Bakke.

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

{-# OPTIONS --guardedness #-}

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

Idea

A conatural number x is positive if it has a predecessor. In other words, if it is not zero.

Definitions

The predicate on conatural numbers of being positive

is-positive-ℕ∞ : ℕ∞ → UU lzero
is-positive-ℕ∞ x = is-value-Maybe (decons-ℕ∞ x)

Properties

Zero is not positive

is-not-positive-zero-ℕ∞ : ¬ (is-positive-ℕ∞ zero-ℕ∞)
is-not-positive-zero-ℕ∞ ()

Successors are positive

is-positive-succ-ℕ∞ : (x : ℕ∞) → is-positive-ℕ∞ (succ-ℕ∞ x)
is-positive-succ-ℕ∞ x = x , refl

The point at infinity is positive

is-positive-infinity-ℕ∞ : is-positive-ℕ∞ infinity-ℕ∞
is-positive-infinity-ℕ∞ = is-positive-succ-ℕ∞ infinity-ℕ∞

Positivity is decidable

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

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

Recent changes