Stlc.agda

module Stlc where

open import Agda.Builtin.String

data Type : Set where
  σ   : Type
  τ   : Type
  _⟶_ : Type → Type → Type

data Var : (a : Type) → Set where
  _∶_ : String → (a : Type) → Var a

data Expr : (a : Type) → Set where
  var  : {a : Type} → Var a → Expr a
  app  : {a b : Type} → Expr (a ⟶ b) → Expr a → Expr b
  Λ_⟶_ : {a b : Type} → Var a → Expr b → Expr (a ⟶ b)