System Fω (SOGAT) [ag-000A]

{-# OPTIONS --safe --without-K #-}
module ag-000A where

open import MLTT.Spartan

record system-F-ω : 𝓤₁ ̇  where
  field
    □ : 𝓤₀ ̇
    Ty : □ → 𝓤₀ ̇

    _⇛_ : □ → □ → □
    LAM : {K L : □} → (Ty K → Ty L) → Ty (K ⇛ L)
    _●_ : {K L : □} → Ty (K ⇛ L) → (Ty K → Ty L)

    ∗ : □
    Tm : Ty ∗ → 𝓤₀ ̇

    All : {K : □} → (Ty K → Ty ∗) → Ty ∗
    Lam : {K : □}{A : Ty K → Ty ∗} → ((X : Ty K) → Tm (A X)) → Tm (All A)
    _•_ : {K : □}{A : Ty K → Ty ∗} → Tm (All A) → ((X : Ty K) → Tm (A X))

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

System Fω 轉換後有

1. 3 個 operations 綁定 Ty-variables
2. 1 個 operation 綁定 term-variable