------------------------------------------------------------------------
-- The type system of the simply type lambda calculus
------------------------------------------------------------------------

module SimplyTyped.TypeSystem where

open import Data.Nat

infixl  _·_
infix   ƛ_
infixr  _⟶_
infixl  _▻_
infix   _∋_ _⊢_

-- Types.

data Ty : Set where
  base : ℕ → Ty
  _⟶_  : Ty → Ty → Ty

-- Contexts.

data Ctxt : Set where
  -- Empty context.
  ε   : Ctxt
  -- Extension of the context with one more type.
  _▻_ : Ctxt → Ty → Ctxt

-- An abbreviation.

TmLike : Set1
TmLike = Ctxt → Ty → Set

-- Variables (de Bruijn indices).

data _∋_ : TmLike where
  -- Zero.
  vz : ∀ {Γ σ}   → Γ ▻ σ ∋ σ
  -- Successor.
  vs : ∀ {Γ σ τ} → Γ ∋ τ → Γ ▻ σ ∋ τ

-- Terms.

data _⊢_ : TmLike where
  var  : ∀ {Γ τ}   → Γ ∋ τ → Γ ⊢ τ
  ƛ_   : ∀ {Γ σ τ} → Γ ▻ σ ⊢ τ → Γ ⊢ σ ⟶ τ
  _·_  : ∀ {Γ σ τ} → Γ ⊢ σ ⟶ τ → Γ ⊢ σ → Γ ⊢ τ