Type Theory in Type Theory Using Quotient Inductive Types
Conference Paper
Formal Antecedent
Foundations and Logic
Citation
Thorsten Altenkirch and Ambrus Kaposi. (2016). Type Theory in Type Theory Using Quotient Inductive Types. Proceedings of POPL 2016. pp. 18–29. ACM.
Why this reference is included
Altenkirch and Kaposi’s Type Theory in Type Theory Using Quotient Inductive Types (2016) is a key conference paper that the program draws on as a technical source. Cited across Book I (Categorical Foundations), Part 18, Chapter The Self-Hosting Landscape; Book I (Categorical Foundations), Part 18, Chapter The Enrichment Frontier — the central framing is “Altenkirch and Kaposi internalized dependent type theory inside the Calculus of Inductive Constructions using quotient inductive types (QITs)”.
Cited in
-
Book I — Categorical Foundations Part 18Chapter The Self-Hosting Landscape
Altenkirch and Kaposi internalized dependent type theory inside the Calculus of Inductive Constructions using quotient inductive types (QITs)
-
Book I — Categorical Foundations Part 18Chapter The Self-Hosting Landscape
Examples: Altenkirch–Kaposi's type theory in type theory (dependent type theory internalized in CIC with quotient inductive types ), Joyal's arithmetic universes (internalize enough to prove G\"odel's theorem internally ), Bocquet–Kaposi–Sattler's internal sconing (metatheorems via internal gluing )
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
1.3 @p1.2cmp3.0cmp3.0cmp2.3cm@ →prule Transition & Closest Precedent & Remaining Gap & τ Feature , E_0 → E_1 & Altenkirch–Kaposi 2016 ; Bocquet–Kaposi–Sattler 2023 & Non-Boolean, constructive adaptation to four-valued Ω_τ & Earned topos E_τ (I.D59) , E_1 → E_2 & Joyal arithmetic universes ; Abel graded modal DTT & Linear DTT not yet complete; no internal cut-elimination & 5 diagonal discipline; three-grade semiring , E_2 → E_3 & Willard 2001 (weak); Girard TX
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
Precedent. This transition has close antecedents in the categorical semantics of type theory: Altenkirch and Kaposi construct type theory in type theory (TT-in-TT) via quotient inductive types (QITs)
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
The enrichment frontier classification assigns a novelty status to each transition of the enrichment ladder: E_0 → E_1: Achieved. Internalizing types within a categorical framework has been accomplished by multiple groups (Altenkirch–Kaposi , Bocquet–Kaposi–Sattler , Moerdijk–Palmgren )