Booleans

We define the inductive booleans to be used in other examples.

module bool where

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

We define the data type of booleans, with the usual constructors true and false.

Bool-id : id-TC-var
Bool-id = 

Bool-name : TC-var 
Bool-name = TC Bool-id 

true-id false-id : id-data-constructor
true-id = 
false-id = 

true false : data-constructor {mix-var} 
true = true-id ∷ [] ⇒ᵀ [||]
false = false-id ∷ [] ⇒ᵀ [||]

Bool : user-defined {mix-var} 
Bool = dataᵀ Bool-name whereᵀ ( true ∷ false ∷ [])

Bool[] = data-typeᵀ Bool [ [||] ]
true[] = dc true [||]
false[] = dc false [||]

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

⊢true : ∅ ∥ ∅ ⊢ᶜ true
⊢true = dcᵀ-intro {G = Bool-name} ∗ ∗

⊢false : ∅ ∥ ∅ ⊢ᶜ false
⊢false = dcᵀ-intro {G = Bool-name} ∗ ∗

⊢Bool : ∀ {Γ χ} → Γ ∥ χ ⊢ Bool[]
⊢Bool =
  data-intro {G = Bool-name}
  {Γcs = ∅ ∷ ∅ ∷ []}
  {χcs = ∅ ∷ ∅ ∷ []}
  (⊢true , ⊢false , ∗)
  ∗