Intuitionistic type theory is a possible framework for constructive mathematics in Bishop’s sense. Such constructive mathematics is compatible with classical mathematics: a constructive proof in Bishop’s sense can directly be understood as a proof in classical logic. A formal way to understand this is by constructing a set-theoretic model of intuitionistic type theory, where each concept of type theory is interpreted as the corresponding concept in Zermelo-Fraenkel Set Theory. For example, a type is interpreted as a set, and the type of functions in \(A \rightarrow B\) is interpreted as the set of all functions in the set-theoretic sense from the set representing \(A\) to the set representing \(B\). The type of natural numbers is interpreted as the set of natural numbers. The interpretations of identity types, and \(\Sigma\) and \(\Pi\)-types were already discussed in the introduction. And as already mentioned, to interpret the type-theoretic universe we need an inaccessible cardinal.