Quadratic type checking for objective type theory

TL;DR

This paper presents a modified type theory that replaces definitional equality with propositional equalities, enabling quadratic time type checking and providing a homotopy-theoretic semantics.

Contribution

It introduces a quadratic time type checking method for a modified Martin-Löf type theory with propositional equalities instead of definitional equality.

Findings

Type checking is quadratic in the modified system.

The system admits a natural homotopy-theoretic semantics.

Elimination of definitional equality simplifies the computational process.

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.