2 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.PL2025
From Semantics to Syntax: A Type Theory for Comprehension Categories
Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens +1
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial…