For the Metatheory of Type Theory, Internal Sconing Is Enough
Article
Formal Antecedent
Category Theory
Citation
Rafaël Bocquet and Ambrus Kaposi and Christian Sattler. (2023). For the Metatheory of Type Theory, Internal Sconing Is Enough. LIPIcs – Proceedings of FSCD 2023. 260. pp. 18:1–18:23.
Why this reference is included
Bocquet, Kaposi, and Sattler’s 2023 For the Metatheory of Type Theory, Internal Sconing Is Enough, published in LIPIcs – Proceedings of FSCD 2023, is one of the program’s working technical references. 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 “Bocquet, Kaposi, and Sattler developed internal sconing (also called internal gluing) as a method for proving metatheorems about type theories within presheaf categories”.
Cited in
-
Book I — Categorical Foundations Part 18Chapter The Self-Hosting Landscape
Bocquet, Kaposi, and Sattler developed internal sconing (also called internal gluing) as a method for proving metatheorems about type theories within presheaf categories
-
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 (fragments) & No full system at
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
Bocquet, Kaposi, and Sattler develop internal sconing — a categorical technique for proving properties of type theories from inside a larger type theory
-
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 )