Simply typed lambda calculus [ag-0007]

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

open import MLTT.Spartan
open import UF.Equiv

record simply-typed-lambda-calculus : 𝓤₁ ̇  where
  field
    Ty : 𝓤₀ ̇
    _⇒_ : Ty → Ty → Ty

generalised 的部分是因為 index Tm by Ty

    Tm : Ty → 𝓤₀ ̇

綁定的部分

    lam : {A B : Ty} → (Tm A → Tm B) → Tm (A ⇒ B)
    _·_ : {A B : Ty} → Tm (A ⇒ B) → (Tm A → Tm B)

    stlc-cong : {A B : Ty} → Tm (A ⇒ B) ≃ (Tm A → Tm B)

一樣參照 first-order lambda calculus 的過程，加上 contexts、加上 substitutions，相應的 first-order 等式跟改寫，就會得到 simply-typed-lambda-calculus 的 GAT。