  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.
