IR DT Types + Terms

gistfile1.txt

open import Level
open import Data.Product public using ( Σ ; _,_ ; proj₁ ; proj₂ )

data ⊥ {a} : Set a where

! : ∀ {a b} {A : Set a} → ⊥ {b} → A
! ()

record ⊤ {a} : Set a where
  constructor tt

data Bool {a} : Set a where
  true  : Bool
  false : Bool

if_then_else_ : ∀ {a b} {A : Set a} → Bool {b} → A → A → A
if true  then t else f = t
if false then t else f = f

----------------------------------------------------------------------

data Type {a} : Set (suc a)
⟦_⟧ᵗ : ∀{a} → Type {a} → Set (suc a)

data Type {a} where
  `Set `⊥ `⊤ `Bool : Type
  `Σ `Π : (τ : Type) (τ′ : ⟦ τ ⟧ᵗ → Type) → Type

⟦ `Set ⟧ᵗ = Set _
⟦ `⊥ ⟧ᵗ = ⊥
⟦ `⊤ ⟧ᵗ = ⊤
⟦ `Bool ⟧ᵗ = Bool
⟦ `Σ τ τ′ ⟧ᵗ = Σ ⟦ τ ⟧ᵗ λ ρ → ⟦ τ′ ρ ⟧ᵗ
⟦ `Π τ τ′ ⟧ᵗ = (ρ : ⟦ τ ⟧ᵗ) → ⟦ τ′ ρ ⟧ᵗ

----------------------------------------------------------------------

data Term {a} : Type {suc a} → Set (suc (suc a))
⟦_⟧ : ∀{a τ} → Term {a} τ → ⟦ τ ⟧ᵗ

data Term {a} where
  `Set `⊥ `⊤ `Bool : Term `Set
  `Σ `Π :
    (ρ : Term `Set)
    (δ : ⟦ ρ ⟧ → Term `Set)
    → Term `Set
  `tt : Term `⊤
  `true `false : Term `Bool
  _`,_ : ∀{τ τ′}
    (e : Term τ)
    (e′ : Term (τ′ ⟦ e ⟧))
    → Term (`Σ τ τ′)
  `λ : ∀{τ τ′}
    (e : (ρ : ⟦ τ ⟧ᵗ) → Term (τ′ ρ))
    → Term (`Π τ τ′)
  `! : ∀{τ}
    (e : Term `⊥)
    → Term τ
  `if_then_else_ : ∀{τ}
    (e : Term `Bool)
    (e₁ e₂ : Term τ)
    → Term τ
  `proj₁ : ∀{τ τ′}
    (e : Term (`Σ τ τ′))
    → Term τ
  `proj₂ : ∀{τ τ′}
    (e : Term (`Σ τ τ′))
    → Term (τ′ (proj₁ ⟦ e ⟧))
  _`$_ : ∀{τ τ′}
    (e : Term (`Π τ τ′)) (e′ : Term τ)
    → Term (τ′ ⟦ e′ ⟧)

⟦ `Set ⟧ = Set _
⟦ `⊥ ⟧ = ⊥
⟦ `⊤ ⟧ = ⊤
⟦ `Bool ⟧ = Bool
⟦ `Σ τ τ′ ⟧ = Σ ⟦ τ ⟧ λ v → ⟦ τ′ v ⟧
⟦ `Π τ τ′ ⟧ = (v : ⟦ τ ⟧) → ⟦ τ′ v ⟧
⟦ `tt ⟧ = tt
⟦ e `, e′ ⟧ = ⟦ e ⟧ , ⟦ e′ ⟧
⟦ `true ⟧ = true
⟦ `false ⟧ = false
⟦ `λ e ⟧ = λ v → ⟦ e v ⟧
⟦ `! e ⟧ = ! ⟦ e ⟧
⟦ `if e then e₁ else e₂ ⟧ = if ⟦ e ⟧ then ⟦ e₁ ⟧ else ⟦ e₂ ⟧
⟦ `proj₁ e ⟧ = proj₁ ⟦ e ⟧
⟦ `proj₂ e ⟧ = proj₂ ⟦ e ⟧
⟦ e `$ e′ ⟧ = ⟦ e ⟧ ⟦ e′ ⟧

----------------------------------------------------------------------

⟦_⟧₀ : ∀{τ} → Term {zero} τ → ⟦ τ ⟧ᵗ
⟦ e ⟧₀ = ⟦ e ⟧

_`→_ : ∀{a} (τ τ′ : Term {a} `Set) → Term `Set
τ `→ τ′ = `Π τ λ _ → τ′

_`×_ : ∀{a} (τ τ′ : Term {a} `Set) → Term `Set
τ `× τ′ = `Π `Bool λ b → if b then τ else τ′

_`⊎_ : ∀{a} (τ τ′ : Term {a} `Set) → Term `Set
τ `⊎ τ′ = `Σ `Bool λ b → if b then τ else τ′

----------------------------------------------------------------------

and : ⟦ `Bool `→ (`Bool `→ `Bool) ⟧
and = ⟦ `λ (λ b → `λ (λ b′ → if b then (if b′ then `true else `false) else `false )) ⟧₀

How can this construction be improved so we can write id?

id : ⟦ ΠSet (λ A → ? → ?) ⟧ id = ⟦λ (λ A → `λ (λ x → ?)) ⟧₀

Unformatted:

id : ⟦ `Π `Set (λ A → ? `→ ?) ⟧
id = ⟦ `λ (λ A → `λ (λ x → ?)) ⟧₀