 Since type theory includes first-order logic, it is no surprise that most systems of type theory are undecidable. However, one may look for solvable special cases of the decision problem. For example, the system \(\cQ_{0}^1\) obtained by adding to \(\cQ_0\) the additional axiom \(\forall x_{\imath}\forall y_{\imath}[x_{\imath}=y_{\imath}]\) is decidable.