21 citations · 58 across the 8 of their papers we have counts for
Showing 2025Show all
2 papers · 1 filter
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…
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…