Defining a realizability model for MLTT using induction-recursion.

mltt.agda

module realize where
open import Relation.Nullary
import      Data.Empty       as E
open import Data.Product
open import Data.Sum
open import Data.Nat

data Term : Set where
  var    : ℕ → Term
  lam    : Term → Term
  app    : Term → Term → Term
  Π      : Term → Term → Term
  sig    : Term → Term → Term
  pair   : Term → Term → Term
  π₁     : Term → Term
  π₂     : Term → Term
  bool   : Term
  tt     : Term
  ff     : Term
  choose : Term → Term → Term → Term
  ⊥      : Term

weaken : Term → Term
weaken t = go 0 t
  where go : ℕ → Term → Term
        go n (var x) with x ≤? n
        ... | yes p = var x
        ... | no ¬p = var (suc x)
        go n (lam t) = lam (go (suc n) t)
        go n (app t₁ t₂) = app (go n t₁) (go n t₂)
        go n (Π t₁ t₂) = Π (go n t₁) (go (suc n) t₂)
        go n (sig t₁ t₂) = sig (go n t₁) (go (suc n) t₂)
        go n (pair t₁ t₂) = pair (go n t₁) (go n t₂)
        go n (π₁ t) = π₁ (go n t)
        go n (π₂ t) = π₂ (go n t)
        go n bool = bool
        go n tt = tt
        go n ff = ff
        go n (choose i t e) = choose (go n i) (go n t) (go n e)
        go n ⊥ = ⊥

subst : Term → ℕ → Term → Term
subst t₁ n (var x) with n ≟ x
... | yes p = t₁
... | no ¬p = var x
subst t₁ n (lam t₂) = lam (subst (weaken t₁) (suc n) t₂)
subst t₁ n (app t₂ t₃) = app (subst t₁ n t₂) (subst t₁ n t₃)
subst t₁ n (Π t₂ t₃) = Π (subst t₁ n t₂) (subst (weaken t₁) (suc n) t₃)
subst t₁ n (sig t₂ t₃) = sig (subst t₁ n t₂) (subst (weaken t₁) (suc n) t₃)
subst t₁ n (pair t₂ t₃) = pair (subst t₁ n t₂) (subst t₁ n t₃)
subst t₁ n (π₁ t₂) = π₁ (subst t₁ n t₂)
subst t₁ n (π₂ t₂) = π₂ (subst t₁ n t₂)
subst t₁ n bool = bool
subst t₁ n tt = tt
subst t₁ n ff = ff
subst t₁ n (choose t₂ t₃ t₄) =
  choose (subst t₁ n t₂) (subst t₁ n t₃) (subst t₁ n t₄)
subst t₁ n ⊥ = ⊥

data Norm : Term → Term → Set where
  var     : ∀ {n} → Norm (var n) (var n)
  lam     : ∀ {t} → Norm (lam t) (lam t)
  app     : ∀ {t₁ t₂ t₃ t₄}
          → Norm t₁ (lam t₃)
          → Norm (subst t₂ 0 t₃) t₄
          → Norm (app t₁ t₂) t₄
  Π       : ∀ {t₁ t₂} → Norm (Π t₁ t₂) (Π t₁ t₂)
  sig     : ∀ {t₁ t₂} → Norm (sig t₁ t₂) (sig t₁ t₂)
  π₁      : ∀ {t₁ t₂ t₃ t₄}
          → Norm t₁ (pair t₂ t₃)
          → Norm t₂ t₄
          → Norm t₁ t₄
  π₂      : ∀ {t₁ t₂ t₃ t₄}
          → Norm t₁ (pair t₂ t₃)
          → Norm t₃ t₄
          → Norm t₁ t₄
  bool    : Norm bool bool
  tt      : Norm tt tt
  ff      : Norm ff ff
  choose1 : ∀ {t₁ t₂ t₃ t₄}
          → Norm t₁ tt
          → Norm t₂ t₄
          → Norm (choose t₁ t₂ t₃) t₄
  choose2 : ∀ {t₁ t₂ t₃ t₄}
          → Norm t₁ ff
          → Norm t₃ t₄
          → Norm (choose t₁ t₂ t₃) t₄
  ⊥       : Norm ⊥ ⊥

data Type : Term → Set
_⊨_ : Term → {a : Term} → Type a → Set

data Type where
  var  : ∀ {n} → Type (var n)
  Π    : ∀ {t₁ t₂}
       → (prf : Type t₁)
       → ({a : Term} → a ⊨ prf → Type (subst a 0 t₂))
       → Type (Π t₁ t₂)
  sig  : ∀ {t₁ t₂}
       → (prf : Type t₁)
       → ({a : Term} → a ⊨ prf → Type (subst a 0 t₂))
       → Type (sig t₁ t₂)
  bool : Type bool
  norm : ∀ {t₁ t₂} → Norm t₁ t₂ → Type t₂ → Type t₁
  ⊥    : Type ⊥

t₁ ⊨ var = Σ ℕ λ n → Norm t₁ (var n)
t₁ ⊨ Π t₂ t₃ = (a : Term)(prf : a ⊨ t₂) → (app t₁ a) ⊨ t₃ prf
t₁ ⊨ sig t₂ t₃ = Σ (π₁ t₁ ⊨ t₂) λ prf → π₂ t₁ ⊨ t₃ prf
t₁ ⊨ bool = Norm t₁ tt ⊎ Norm t₁ ff
t₁ ⊨ ⊥ = E.⊥
t₁ ⊨ norm n t₂ = t₁ ⊨ t₂