2 papers
math.LO2025
A 2-categorical approach to the semantics of dependent type theory with computation axioms
Matteo Spadetto
Axiomatic type theory is a dependent type theory without computation rules. The term equality judgements that usually characterise these rules are replaced by computation axioms, i…
math.LO2025
The biequivalence of path categories and axiomatic Martin-Löf type theories
Daniël Otten, Matteo Spadetto
The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 1-types, and Sigma-types are biequivalent to finitely complete categ…