Natural numbers

Here we define the inductive natural numbers to be used in other examples.

module nat where

open import map
open import Data.List using (_∷_ ; [] ; [_])
open import Data.Vec renaming ([] to [||]; [_] to [|_|])
open import Data.Unit renaming (tt to ∗)
open import Data.Product using (_,_)

We define the data type of natural numbers with the usual constructors zeroNat and sucNat (we don’t use zero and suc to avoid any confusion with the type ℕ of Agda’s standard library).

Nat-id : id-TC-var
Nat-id = 2

Nat-name : TC-var 0
Nat-name = TC Nat-id 0

zero-id suc-id : id-data-constructor
zero-id = 21
suc-id = 22

zeroNat sucNat : data-constructor {mix-var} 0
zeroNat = zero-id ∷ [] ⇒ᵀ [||]
sucNat = suc-id ∷ [ appᵀ Nat-name [ [||] ] ] ⇒ᵀ [||]

Nat : user-defined {mix-var} 0
Nat = dataᵀ Nat-name whereᵀ (zeroNat ∷ sucNat ∷ [])

Nat[] = data-typeᵀ Nat [ [||] ]

Some shortcuts to use actual natural numbers in the examples.

0Nat 1Nat 2Nat 3Nat 4Nat 5Nat : term-expr
0Nat = dc zeroNat [||]
1Nat = dc sucNat [| 0Nat |]
2Nat = dc sucNat [| 1Nat |]
3Nat = dc sucNat [| 2Nat |]
4Nat = dc sucNat [| 3Nat |]
5Nat = dc sucNat [| 4Nat |]

Finally, we justify the application of Nat to the empty tuple of type expressions.

⊢zeroNat : ∅ ∥ ∅ ⊢ᶜ zeroNat
⊢zeroNat = dcᵀ-intro {G = Nat-name} ∗ ∗

⊢sucNat : ∅ ∥ ∅ ⊢ᶜ sucNat
⊢sucNat = dcᵀ-intro {G = Nat-name} (app-intro ∗ ∋-last , ∗) ∗

⊢Nat : ∅ ∥ ∅ ⊢ Nat[]
⊢Nat =
  data-intro
  {Γcs = ∅ ∷ ∅ ∷ []}
  {χcs = ∅ ∷ ∅ ∷ []}
  (⊢zeroNat , ⊢sucNat , ∗) ∗