Intrinsically typed term [ag-0002]

{-# OPTIONS --safe --without-K #-}
module ag-0002 where

open import MLTT.Spartan hiding (Type)
open import MLTT.List

Type 在 STLC 還只需要是一個簡單的 formation

data Type : 𝓤₀  ̇ where
  bool : Type
  _⇒_ : Type → Type → Type
infixr  _⇒_

variable
  S T : Type

Context 通常會自訂，比如 MLTT 需要兩種綁定時自訂就會更方便一些

Ctx = List Type
_▷_ : Ctx → Type → Ctx
Γ ▷ T = T ∷ Γ
infix  _▷_

variable Γ : Ctx

Intrinsically-scoped de Brujin indices

基本上變數都長這樣

data _∋_ : Ctx → Type → 𝓤₀  ̇ where
  here  : Γ ▷ T ∋ T
  there : Γ ∋ T → Γ ▷ S ∋ T
infix  _∋_

variable x : Γ ∋ T

Intrinsically-typed terms

確保 term 是類型良好的一種方式就是從一開始就跟 context 一起構造，讓 terms 必須是 well-typed

data _⊢_ : Ctx → Type → 𝓤₀  ̇ where
  true false : Γ ⊢ bool
  var : Γ ∋ T → Γ ⊢ T
  lam : Γ ▷ S ⊢ T → Γ ⊢ S ⇒ T
  _·_ : Γ ⊢ S ⇒ T → Γ ⊢ S → Γ ⊢ T
  if_then_else_ : Γ ⊢ bool → Γ ⊢ T → Γ ⊢ T → Γ ⊢ T
infix  _⊢_