Minimal Martin-Löf type theory (SOGAT) [ag-000B]

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

open import MLTT.Spartan
open import MLTT.NaturalNumbers

variable
  𝑖 : ℕ

record minimal-martin-lof-type-theory : 𝓤₁ ̇  where
  field
    Ty : ℕ → 𝓤₀ ̇
    U : (𝑖 : ℕ) → Ty (succ 𝑖)
    Tm : Ty 𝑖 → 𝓤₀ ̇

    c : Ty 𝑖 → Tm (U 𝑖)
    El : Tm (U 𝑖) → Ty 𝑖

    PI : (A : Ty 𝑖) → (Tm A → Ty 𝑖) → Ty 𝑖
    Lift : Ty 𝑖 → Ty (succ 𝑖)

    lam : {𝐴 : Ty 𝑖}{𝐵 : Tm 𝐴 → Ty 𝑖} → ((𝑎 : Tm 𝐴) → Tm (𝐵 𝑎)) → Tm (PI 𝐴 𝐵)
    _·_ : {𝐴 : Ty 𝑖}{𝐵 : Tm 𝐴 → Ty 𝑖} → Tm (PI 𝐴 𝐵) → ((𝑎 : Tm 𝐴) → Tm (𝐵 𝑎))

    mk : {𝐴 : Ty 𝑖} → Tm 𝐴 → Tm (Lift 𝐴)
    un : {𝐴 : Ty 𝑖} → Tm (Lift 𝐴) → Tm 𝐴

這個理論的對應 GAT 得到一個具有族的範疇（CwF），更準確地說，是一個具有 N 個 families 的範疇，這些族配備了 familywise Π-types、宇宙以及族之間的一步向上提升。 這些類型是 Ty : Con → N → Set 和 Tm : (Γ : Con) → Ty Γ 𝑖 → Set，其中 𝑖 論證隱含在後者中。