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

module HOAS.SimplyTyped.TypeSystem where

open import SimplyTyped.TypeSystem public using (Ty; base; _⟶_)

infixl  _·_
infix   ƛ_

-- Terms.

data Tm' (V : Ty → Set) : Ty → Set where
  var : ∀ {σ}   (x : V σ) → Tm' V σ
  ƛ_  : ∀ {σ τ} (t : V σ → Tm' V τ) → Tm' V (σ ⟶ τ)
  _·_ : ∀ {σ τ} (t₁ : Tm' V (σ ⟶ τ)) (t₂ : Tm' V σ) → Tm' V τ

Tm : Ty → Set1
Tm σ = ∀ {V} → Tm' V σ