Definition of phantom types simulating the inductive definition of the data constructors of Nat at the type level.
module phantomNat where open import map open import Data.List using (_∷_ ; [] ) open import Data.Vec renaming (_∷_ to _¦_ ; [] to [||] ; [_] to [|_|]) open import Data.Unit renaming (tt to ∗) open import Data.Product using (_,_)
We define now the data types phantomZero and phantomSuc as data types of arity 0 with no constructors.
phantomZero-id phantomSuc-id : id-TC-var
phantomZero-id = 6
phantomSuc-id = 7
phantomZero-name : TC-var 0
phantomZero-name = TC phantomZero-id 0
phantomSuc-name : TC-var 1
phantomSuc-name = TC phantomSuc-id 1
phantomZero : user-defined {mix-var} 0
phantomZero = dataᵀ phantomZero-name whereᵀ []
phantomSuc : user-defined {mix-var} 1
phantomSuc = dataᵀ phantomSuc-name whereᵀ []
phantomZero[] = data-typeᵀ phantomZero [ [||] ]
phantomSuc[_] = λ n → data-typeᵀ phantomSuc [ [| n |] ]
The justification of these types are pretty easy, since no justifications need to be provided for the data constructors.
⊢phantomZero : ∀ {Γ χ} → Γ ∥ χ ⊢ phantomZero[]
⊢phantomZero = data-intro {Γcs = []} {χcs = []} ∗ ∗
⊢phantomSuc : ∀ {Γ χ x} → _ → Γ ∥ χ ⊢ phantomSuc[ x ]
⊢phantomSuc = data-intro {Γcs = []} {χcs = []} ∗