A display map 2-category semantics for axiomatic type theory is shown sound, yielding a semantic proof that the identity type computation rule is not admissible.
Quadratic type checking for objective type theory
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
abstract
We introduce a modification of standard Martin-Lof type theory in which we eliminate definitional equality and replace all computation rules by propositional equalities. We show that type checking for such a system can be done in quadratic time and that it has a natural homotopy-theoretic semantics.
citation-role summary
background 1
citation-polarity summary
fields
math.LO 1years
2025 1verdicts
CONDITIONAL 1roles
background 1polarities
unclear 1representative citing papers
citing papers explorer
-
A 2-categorical approach to the semantics of dependent type theory with computation axioms
A display map 2-category semantics for axiomatic type theory is shown sound, yielding a semantic proof that the identity type computation rule is not admissible.