Typed combinator calculus (Generalised algebraic theories) [ag-0004]

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

open import MLTT.Spartan

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

給 types 的 sort

    Ty : 𝓤₀ ̇

每個 type 對應（index）一個 term 用的 sort

    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  _⇒_

上述 Algebraic Theory 的通用代數特徵可以推廣到 GAT。具體來說，每個 GAT 都具有由 quotient inductive-inductive type 給出的語法，我們有 free 模型和 cofree 模型。