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.

翻译：我们引入了对标准马丁-Lof类型理论的修改,在这种修改中,我们消除了定义平等,用主张平等取代了所有计算规则。 我们表明,这种系统的类型检查可以在二次时间进行,并且它具有自然的同质理论语义语义。