Quadratic type checking for objective type theory

Benno van den Berg, Martijn den Besten

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 th…