← 研踪 PaperTrailarXiv:2601.19426 · v2
For Generalised Algebraic Theories, Two Sorts Are Enough
首次提交 2026-01-27 18:05
版本更新 2026-11-07 17:36
雷达观测 2026-11-10 11:14
摘要
Generalised algebraic theories (GATs) allow multiple sorts indexed over each other. For example, the theories of categories or Martin-L{ö}f type theories form GATs. Categories have two sorts, objects and morphisms, and the latter are double-indexed over the former. Martin-L{ö}f type theory has four sorts: contexts, substitutions, types and terms. For example, types are indexed over contexts, and terms are indexed over both contexts and types. In this paper we show that any GAT can be reduced to a GAT with only two sorts, and there is a section-retraction correspondence (formally, a strict coreflection) between models of the original and the reduced GAT. In particular, any model of the original GAT can be turned into a model of the reduced (two-sorted) GAT and back, and this roundtrip is the identity. The reduced GAT is simpler than the original GAT in the following aspects: it does not have sort equalities; it does not have interleaved sorts and operations; if the original GAT did not have interleaved sorts and operations, then the reduced GAT won't have operations interleaved between different sorts. In a type-theoretic metatheory, the initial algebra of a GAT is called a quotient inductive-inductive type (QIIT). Our reduction provides a way to implement QIITs with sort equalities or interleaved constructors which are not allowed by Cubical Agda. An instance of our reduction is the well-known method of reducing mutual inductive types to a single indexed family. Our approach is semantic in that it does not rely on a syntactic description of GATs, but instead, on Uemura's bi-initial characterisation of the category of (finite) GATs in the 2-category of finitely complete categories with a chosen exponentiable morphism.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v3 · 2026-11-10 18:06 · 最新观测版本
For Generalised Algebraic Theories, Two Sorts Are Enough
Generalised algebraic theories (GATs) allow multiple sorts indexed over each other. Categories have two sorts, objects and morphisms, and the latter are double-indexed over the former. Martin-Löf type theory has four sorts: contexts, substitutions, types and terms. For example, types are indexed over contexts, and terms are indexed over both contexts and types. In this paper we show that any GAT can be reduced to a GAT involving only two sorts: a first one without dependencies, and another one indexed over the former. We show that a model of the reduced GAT is equivalently given by a pair consisting of a model of the original GAT, which we call the core model, and a "cartesian" morphism from the family of sets induced by this core model. In a type-theoretic metatheory, the initial model of a GAT is called a quotient inductive-inductive type (QIIT). The above characterisation justifies soundness of the reduction, in the sense that the QIIT of the original GAT can be simulated from the QIIT of the reduced GAT, by taking its core model. A particular case of our reduction is the well-known method of reducing mutual inductive types to a single indexed family. Other instances of this reduction can be found in the literature to simulate sophisticated QIITs in Cubical Agda. Indeed, the reduced GAT is simpler than the original GAT in the following aspects: it does not have sort equalities; it does not have interleaved sorts and operations; if the original GAT did not have interleaved sorts and operations, then the reduced GAT won't have operations interleaved between different sorts. Our approach is semantic in that it does not rely on a syntactic description of GATs, but instead, on Uemura's bi-initial characterisation of the category of (finite) GATs in the 2-category of finitely complete categories with a chosen exponentiable morphism.
查看此版本解读 →查看此版本原文 ↗v2 · 2026-11-07 17:36
For Generalised Algebraic Theories, Two Sorts Are Enough
Generalised algebraic theories (GATs) allow multiple sorts indexed over each other. For example, the theories of categories or Martin-L{ö}f type theories form GATs. Categories have two sorts, objects and morphisms, and the latter are double-indexed over the former. Martin-L{ö}f type theory has four sorts: contexts, substitutions, types and terms. For example, types are indexed over contexts, and terms are indexed over both contexts and types. In this paper we show that any GAT can be reduced to a GAT with only two sorts, and there is a section-retraction correspondence (formally, a strict coreflection) between models of the original and the reduced GAT. In particular, any model of the original GAT can be turned into a model of the reduced (two-sorted) GAT and back, and this roundtrip is the identity. The reduced GAT is simpler than the original GAT in the following aspects: it does not have sort equalities; it does not have interleaved sorts and operations; if the original GAT did not have interleaved sorts and operations, then the reduced GAT won't have operations interleaved between different sorts. In a type-theoretic metatheory, the initial algebra of a GAT is called a quotient inductive-inductive type (QIIT). Our reduction provides a way to implement QIITs with sort equalities or interleaved constructors which are not allowed by Cubical Agda. An instance of our reduction is the well-known method of reducing mutual inductive types to a single indexed family. Our approach is semantic in that it does not rely on a syntactic description of GATs, but instead, on Uemura's bi-initial characterisation of the category of (finite) GATs in the 2-category of finitely complete categories with a chosen exponentiable morphism.
查看此版本解读 →查看此版本原文 ↗