While a standard presentation of first-order logic would follow Tarski in defining the notion of model, intuitionistic type theory follows the tradition of Brouwerian meaning theory as further developed by Heyting and Kolmogorov, the so called BHK-interpretation of logic. The key point is that the proof of an implication \(A \supset B \) is a method that transforms a proof of \(A\) to a proof of \(B\). In intuitionistic type theory this method is formally represented by the program \(f {:} A \supset B\) or \(f {:} A \rightarrow B\): the type of proofs of an implication \(A \supset B\) is the type of functions which maps proofs of \(A\) to proofs of \(B\).