STLC.agda

data ★ : Set where
  ι : ★
  _⊳_ : ★ → ★ → ★
infixr 15 _⊳_

data Term : Set where
  var  : Atom → Term
  ƛ_↦_ : Atom → Term → Term
  _⋅_  : Term → Term → Term
infix 7 ƛ_↦_
infix 6 _⋅_

_﹕_ : ∀ {A B : Set} → A → B → A × B
_﹕_ = ⟨_,_⟩
infix 5 _﹕_

Cx : Set
Cx = List (Term × ★)

data _⊢_ : Cx → (Term × ★) → Set where
  VAR : ∀ {Γ α x}       → Γ , (var x ﹕ α) ⊢ (var x ﹕ α)
  LAM : ∀ {Γ α β x M}   → Γ , (var x ﹕ α) ⊢ (M ﹕ β) → Γ ⊢ (ƛ x ↦ M ﹕ α ⊳ β)
  APP : ∀ {Γ α β f x y} → Γ ⊢ (f ﹕ α ⊳ β) → Γ ⊢ (x ﹕ α) → Γ ⊢ (y ﹕ β)
infix 1 _⊢_

-- Free variables in a term.
FV : ∀ {Γ A} → Γ ⊢ A → List Atom
FV (VAR {x = a})   = [ a ]
FV (LAM {x = a} t) = (FV t) - a
FV (APP t₁ t₂)     = (FV t₁) ∪ (FV t₂)

-- λI terms.
λI : ∀ {Γ A} → Γ ⊢ A → Set
λI VAR             = ⊤
λI (LAM {x = a} t) = (λI t) × (a ∈ (FV t))
λI (APP t₁ t₂)     = (λI t₁) × (λI t₂)


Closed : (Term × ★) → Set
Closed = _⊢_ ∅

I : Closed ((ƛ v₀ ↦ (var v₀)) ﹕ (ι ⊳ ι))
I = LAM VAR

I-is-λI : λI I
I-is-λI = ⟨ • , zero ⟩