The consistency of intuitionistic type theory relative to set theory can be proved by model constructions. Perhaps the simplest method is an interpretation whereby each type-theoretic concept is given its corresponding set-theoretic meaning, as outlined in   section 2.3. For example the type of functions \(A \rightarrow B\) is interpreted as the set of all functions in the set-theoretic sense between the set denoted by \(A\) and the set denoted by \(B\). To interpret \(\U\) we need a set-theoretic universe which is closed under all (set-theoretic analogues of) the type constructors. Such a universe can be proved to exist if we assume the existence of an inaccessible cardinal \(\kappa\) and interpret \(\U\) by \(V_\kappa\) in the cumulative hierarchy.