SOGAT of type theory with $\Pi$-types, a Tarski universe, and natural numbers [ag-000W]

Learn from https://github.com/kontheocharis/erasure-agda

{-# OPTIONS --safe --without-K --confluence-check #-}
module ag-000W where

open import MLTT.Spartan hiding (Π; zero; succ)

coe : {X X' : 𝓤 ̇ } → X ＝ X' → X → X'
coe = transport id

TT 要用的 sorts，以及如果 Type 相等，可以轉換 term 用的 helper coeTm

record TT-sorts : (𝓤 ⊔ 𝓥)⁺  ̇ where
  field
    Ty : 𝓤 ̇
    Tm : Ty → 𝓥 ̇

  coeTm : ∀ {A B : Ty} → A ＝ B → Tm A → Tm B
  coeTm p a = coe (ap Tm p) a

TT 的 SOGAT

module _ (sorts : TT-sorts {𝓤} {𝓥}) where
  open TT-sorts sorts

  private
    variable
      A B C : Ty
      X Y Z : Tm _ → Ty
      t u v : Tm _
      f g h : (a : Tm _) → Tm _
      eq : _ ＝ _

  record TT-ctors : (𝓤 ⊔ 𝓥)⁺  ̇ where
    field
      -- Pi types
      Π : (A : Ty) → (Tm A → Ty) → Ty
      lam : ((a : Tm A) → Tm (X a)) → Tm (Π A X)
      app : Tm (Π A X) → (a : Tm A) → Tm (X a)
      lam-app : lam (app t) ＝ t
      app-lam : app (lam f) ＝ f

      -- Universe
      U : Ty
      El : Tm U → Ty

      -- Natural numbers
      Nat : Ty
      zero : Tm Nat
      succ : Tm Nat → Tm Nat
      elim-Nat : (X : Tm Nat → Ty)
        → (Tm (X zero))
        → ((n : Tm Nat) → Tm (X n) → Tm (X (succ n)))
        → (n : Tm Nat) → Tm (X n)

      -- Computation for elim-Nat
      elim-Nat-zero : ∀ {mz ms} → elim-Nat X mz ms zero ＝ mz
      elim-Nat-succ : ∀ {mz ms n} → elim-Nat X mz ms (succ n) ＝ ms n (elim-Nat X mz ms n)

record TT : (𝓤 ⊔ 𝓥)⁺  ̇ where
  field
    sorts : TT-sorts {𝓤} {𝓥}
  open TT-sorts sorts public
  field
    ctors : TT-ctors sorts
  open TT-ctors ctors public