An important fact about type theory, and something which is also heavily exploited in implementations, is that type checking is decidable However, from a complexity-theoretic point of view the worst case upper bounds are quite serious: according to a result by Statman from 1979, the problem is not elementary recursive. Recently, in the context of homotopy type theory people have started to consider a version of type theory in which all computation rules are replaced by propositional equalities. In this talk, I will discuss this version of type theory, which one could call “objective type theory”. In particular, I will show that if one formulates this objective type theory with sufficient care, type checking can be done in quadratic time. (This is joint work with my PhD student Martijn den Besten.)