¹⁰This should not be confused with the statement that type theory is consistent, which is the meta-theoretic claim that it is not possible to obtain an element of 0 by following the rules of type theory.