從具體到抽象可以把語法表示看成

在 well-typed terms 上再加上 conversion relation 就變成廣義代數理論（generalised algebraic theory，簡稱 GAT），GAT 用來處理 dependently typed languages 時特別方便，因為 typing 依賴了 conversion relation。在 GAT 上只能定義保留了 conversion relation 的函數，因此連印出函數都無法定義，但 normalisation（正規化）、typechecking（型別檢查）跟 parametricity 這些函數保留 conversion 因此可定義。

對任何 GAT 來說，syntax 可以定義成 initial model，因此沒有區分語法跟語意的必要，某種意義上來說，一個程式語言就是一個 GAT。

HOAS 觀點關心 bindings 跟 variables 的處理方式，比如 De Bruijn indices 使名稱選擇與語意無關，但這也表示替換必須是語法的一部分，舉例來說 form of a category with families。

Logical frameworks 跟 higher-order abstract syntax (HOAS) 提供了另一種實現 bindings 跟 variables 的方式：使用 metatheory 的函數空間。 舉例來說，pure lambda calculus 的 lambda operation 的 type 是二階函數空間 (Tm → Tm) → Tm。這在理論上的解釋是 type-theoretic internal language of presheaves over the category of contexts and syntactic substitutions，在這個 topos 的 internal language 裡，lambda 的類型就長那樣。

The main takeaway of this paper is that structural languages are SOGATs.

We justify this claim through several examples. Our technical contributions are the following:

• The theory of SOGAT signatures (ToS+), a domain-specific type theory in which every closed type is a SOGAT signature. As it is a structural type theory, it can be defined as a SOGAT itself. Signatures can be formalised in ToS+ without encoding overhead.
• A translation from SOGAT signatures to GAT signatures based on a parallel substitution calculus. Thus, for every SOGAT, we obtain all of the semantics of GATs: a category of models with an initial object, (co)free models, notions of displayed models and sections, the fact that induction is equivalent to initiality, and so on. The GAT descriptions that we obtain are readable, do not contain occurrences of Yoneda as in usual presheaf function spaces. Correctness of the translation is showed by proving that internally to presheaves over a model of the GAT, a second-order model of the SOGAT is available.
• We define an alternative translation producing a single substitution calculus.

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

open import MLTT.Spartan

Combinator calculus 可以看成一個代數理論，這時候它有

1. 一個 sort of terms
2. 一個 binary
3. 兩個 nullary operations
4. 兩個等式

record combinator-calculus : 𝓤₁ ̇ where
  field
    Tm : 𝓤₀ ̇

    _·_ : Tm → Tm → Tm

    K : Tm
    S : Tm

    Kβ : {u f : Tm} → K · u · f ＝ u
    Sβ : {f g u : Tm} → S · f · g · u ＝ f · u · (g · u)

  infixl  _·_

1. 從這個符號可以明顯看出代數/模型的概念
2. Combinator calculus 的 quotiented syntax 是初始模型，它總是存在。
3. Notions of homomorphism, displayed/dependent model, induction, products and coproducts of models, free models, and so on, are derivable from the signature, as described in any book on universal algebra
4. Algebraic Theory 的 initial algebra 叫做 quotient inductive type

其他 single-sorted algebraic theories 著名案例：

1. 邏輯：經典（或直覺主義）命題邏輯，定義為布林代數（或海廷代數）理論
2. 代數：monoids、群、環、lattices 等等

Generalised algebraic theories (GATs) 的 sort 可以 indexed by 其他 sort。案例有 typed combinator calculus、propositional logic with Hilbert-style proof theory、theories of graphs、preorders、categories 等等

module ag-0004 where

open import MLTT.Spartan

record typed-combinator-calculus : 𝓤₁ ̇ where
  field

    Ty : 𝓤₀ ̇

    Tm : Ty → 𝓤₀ ̇

    ι : Ty
    _⇒_ : Ty → Ty → Ty

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

    K : {A B : Ty} → Tm (A ⇒ B ⇒ A)
    S : {A B C : Ty} → Tm ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C)

    Kβ : {A B : Ty} {u : Tm A} {f : Tm B} → K · u · f ＝ u
    Sβ : {A B C : Ty}
      {f : Tm (A ⇒ B ⇒ C)}
      {g : Tm (A ⇒ B)}
      {u : Tm A}
      → S · f · g · u ＝ f · u · (g · u)

  infixl  _·_
  infixr  _⇒_

如果一個語言有變數或是綁定，就被定義成一個二階理論。

module ag-0005 where

open import MLTT.Spartan

record lambda-calculus : 𝓤₁ ̇ where
  field
    Tm : 𝓤₀ ̇

    lam : (Tm → Tm) → Tm
    _·_ : Tm → Tm → Tm

    β : {f : Tm → Tm} {u : Tm} → lam f · u ＝ f u

  infixl  _·_

  Y : Tm
  Y = lam (λ f → (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x))))

  Y-is-fixed-point : {f : Tm} → Y · f ＝ f · (Y · f)
  Y-is-fixed-point {f} =
    Y · f                                                                 ＝⟨by-definition⟩
    lam (λ f → (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))) · f ＝⟨ β ⟩
    (λ f → (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))) f       ＝⟨ refl ⟩
    (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))                 ＝⟨ β ⟩
    f · ((lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x))))           ＝⟨ refl ⟩
    f · ((λ f → (lam (λ x → f · (x · x))) · (lam (λ x → f · (x · x)))) f) ＝⟨ ap (f ·_) (β ⁻¹) ⟩
    f · (Y · f) ∎

但注意沒有可用的 SOAT models $M$ 和 $N$ 之間的同態概念。為了討論同態或語法，我們將 SOAT 轉換為一階 GAT：加上上下文、替換、索引 Tm 以及所有基於上下文的操作，然後 lam 就變成了一個以擴展上下文中的項作為輸入的一階函數。轉換出來的 GAT 就是

module ag-0006 where

open import MLTT.Spartan hiding (_∘_; id)

record first-order-lambda-calculus : 𝓤₁ ̇  where
  field
    Con : 𝓤₀ ̇
    Sub : Con → Con → 𝓤₀ ̇

    _∘_ : {Δ Γ Θ : Con} → Sub Δ Γ → Sub Θ Δ → Sub Θ Γ
    assoc : {A B C D : Con} {γ : Sub C D} {δ : Sub B C} {θ : Sub A B}
      → (γ ∘ δ) ∘ θ ＝ γ ∘ (δ ∘ θ)
    id : {Γ : Con} → Sub Γ Γ
    id-left : {A B : Con} {γ : Sub A B} → id ∘ γ ＝ γ
    id-right : {A B : Con} {γ : Sub A B} → γ ∘ id ＝ γ
    -- empty context: zero
    ◇ : Con
    ε : {Γ : Con} → Sub Γ ◇
    -- terminal
    ◇η : {Γ : Con} → (σ : Sub Γ ◇) → σ ＝ ε

    Tm : Con → 𝓤₀ ̇
    _[_] : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ
    [id] : {Γ : Con} {t : Tm Γ} → t [ id ] ＝ t
    [∘] : {Θ Γ Δ : Con} {t : Tm Γ} {γ : Sub Δ Γ} {δ : Sub Θ Δ} → t [ γ ∘ δ ] ＝ t [ γ ] [ δ ]

    _▹ : Con → Con

    _,,_ : {Δ Γ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹)

    p : {Γ : Con} → Sub (Γ ▹) Γ
    q : {Γ : Con} → Tm (Γ ▹)

    ▹β₁ : {Δ Γ : Con} {γ : Sub Δ Γ} {t : Tm Δ}
      → p ∘ (γ ,, t) ＝ γ
    ▹β₂ : {Δ Γ : Con} {γ : Sub Δ Γ} {t : Tm Δ}
      → q [ γ ,, t ] ＝ t
    ▹η : {Δ Γ : Con} {σ : Sub Δ (Γ ▹)} → σ ＝ (p ∘ σ ,, q [ σ ])

    lam : {Γ : Con} → Tm (Γ ▹) → Tm Γ
    lam[] : {Δ Γ : Con} {γ : Sub Δ Γ} {t : Tm (Γ ▹)} → (lam t)[ γ ] ＝ lam (t [ γ ∘ p ,, q ])

    _·_ : {Γ : Con} → Tm Γ → Tm Γ → Tm Γ
    ·[] : {Δ Γ : Con} {γ : Sub Δ Γ} {t u : Tm Γ} → (t · u)[ γ ] ＝ t [ γ ] · (u [ γ ])

    β : {Δ Γ : Con} {γ : Sub Δ Γ} {t : Tm (Γ ▹)} {u : Tm Γ}
      → lam t · u ＝ t [ id ,, u ]

  infixl  _∘_
  infixl  _,,_
  infixl  _·_
  infixl  _[_]

SOGATs combine the two previous classes: sorts can be indexed over previous sorts and second-order operations are allowed.

module ag-0007 where

open import MLTT.Spartan
open import UF.Equiv

record simply-typed-lambda-calculus : 𝓤₁ ̇  where
  field
    Ty : 𝓤₀ ̇
    _⇒_ : Ty → Ty → 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)

module ag-0008 where

open import MLTT.Spartan
open import UF.Subsingletons

record minimal-intuitionistic-first-order-logic : 𝓤₁ ̇  where
  field
    For : 𝓤₀ ̇
    Tm : 𝓤₀ ̇
    _⊃_ : For → For → For
    All : (Tm → For) → For
    Eq : Tm → Tm → For

    Pf : For → 𝓤₀ ̇
    Pf-is-prop : (A : For) → is-prop (Pf A)

    intro⊃ : {A B : For} → (Pf A → Pf B) → Pf (A ⊃ B)
    elim⊃ : {A B : For} → Pf (A ⊃ B) → (Pf A → Pf B)

    intro∀ : {A : Tm → For} → ((𝑡 : Tm) → Pf (A 𝑡)) → Pf (All A)
    elim∀ : {A : Tm → For} → Pf (All A) → ((𝑡 : Tm) → Pf (A 𝑡))

    introEq : {t : Tm} → Pf (Eq t t)
    elimEq : {t t' : Tm} → (A : Tm → For) → Pf (Eq t t') → Pf (A t) → Pf (A t')

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 (𝐴 𝑋))

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)

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 𝐴