STLC-StdModel.agda

data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty
infixr 3 _⇒_

data Con : Set where
  ∙   : Con
  _▶_ : Con → Ty → Con
infixl 3 _▶_

data Var : Con → Ty → Set where
  vz : ∀ {Γ A} → Var (Γ ▶ A) A
  vs : ∀ {Γ A B} → Var Γ A → Var (Γ ▶ B) A

data Tm (Γ : Con) : Ty → Set where
  var : ∀ {A} → Var Γ A → Tm Γ A
  lam : ∀ {A B} → Tm (Γ ▶ A) B → Tm Γ (A ⇒ B)
  app : ∀ {A B} → Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B

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

open import Data.Unit
open import Data.Empty
open import Data.Product

⟦_⟧Ty : Ty → Set
⟦ ι     ⟧Ty = ⊥
⟦ A ⇒ B ⟧Ty = ⟦ A ⟧Ty → ⟦ B ⟧Ty

⟦_⟧Con : Con → Set
⟦ ∙     ⟧Con = ⊤
⟦ Γ ▶ A ⟧Con = ⟦ Γ ⟧Con × ⟦ A ⟧Ty

⟦_⟧Tm : ∀ {Γ A} → Tm Γ A → ⟦ Γ ⟧Con → ⟦ A ⟧Ty
⟦ var vz     ⟧Tm γ = proj₂ γ
⟦ var (vs x) ⟧Tm γ = ⟦ var x ⟧Tm (proj₁ γ)
⟦ lam t      ⟧Tm γ = λ α → ⟦ t ⟧Tm (γ , α)
⟦ app t u    ⟧Tm γ = ⟦ t ⟧Tm γ (⟦ u ⟧Tm γ)

consistent : Tm ∙ ι → ⊥
consistent t = ⟦ t ⟧Tm tt