Intuitionistic type theory is not only a formal logical system but also provides a comprehensive philosophical framework for intuitionism. It is an interpreted language, where the distinction between the demonstration of a judgment and the proof of a proposition plays a fundamental role (Sundholm 2012). The framework clarifies the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic and extends it to the more general setting of intuitionistic type theory. In doing so it provides a general conception not only of what a constructive proof is, but also of what a constructive mathematical object is. The meaning of the judgments of intuitionistic type theory is explained in terms of computations of the canonical forms of types and terms. These informal, intuitive meaning explanations are “pre-mathematical” and should be contrasted to formal mathematical models developed inside a standard mathematical framework such as set theory.