Polymorphic lambda calculus (SOGAT) [ag-0009]

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

open import MLTT.Spartan

record polymorphic-lambda-calculus : 𝓤₁ ̇  where
  field
    Ty : 𝓤₀ ̇
    Tm : Ty → 𝓤₀ ̇
    _⇒_ : Ty → Ty → Ty
    lam : {𝐴 𝐵 : Ty} → (Tm 𝐴 → Tm 𝐵) → Tm (𝐴 ⇒ 𝐵)
    _·_ : {𝐴 𝐵 : Ty} → Tm (𝐴 ⇒ 𝐵) → (Tm 𝐴 → Tm 𝐵)
    All : (Ty → Ty) → Ty
    Lam : {𝐴 : Ty → Ty} → ((𝑋 : Ty) → Tm (𝐴 𝑋)) → Tm (All 𝐴)
    _•_ : {𝐴 : Ty → Ty} → Tm (All 𝐴) → ((𝑋 : Ty) → Tm (𝐴 𝑋))

一樣參照 first-order lambda calculus 的過程，加上 contexts、加上 substitutions，相應的 first-order 等式跟改寫。