3 papers
cs.PL2026
For Generalised Algebraic Theories, Two Sorts Are Enough
Samy Avrillon, Ambrus Kaposi, Ambroise Lafont +2
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 hav…
cs.LO2025
The Groupoid-Syntax of Type Theory is a Set
Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the t…
cs.LO2025
Type Theory with Single Substitutions
Ambrus Kaposi, Szumi Xie
Type theory can be described as a generalised algebraic theory. This automatically gives a notion of model and the existence of the syntax as the initial model, which is a quotient…