{"id":"arxiv/2601.19426","url":"https://arxiv.org/abs/2601.19426","tags":["cs.PL","cs.LO","math.CT"],"score":0,"title":"For Generalised Algebraic Theories, Two Sorts Are Enough","domain":"cs.PL","source":"arxiv","authors":["Samy Avrillon","Ambrus Kaposi","Ambroise Lafont","Niyousha Najmaei","Johann Rosain"],"reviews":0,"subject":"cs.PL","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-01-27","reactions":{}}