is fundamental to intuitionistic type theory. This principle is also known as the Curry-Howard correspondence or even Curry-Howard isomorphism. Curry discovered a correspondence between the implicational fragment of intuitionistic logic and the simply typed lambda-calculus. Howard extended this correspondence to first-order predicate logic. In intuitionistic type theory this correspondence becomes an identification of proposition and types, which has been extended to include quantification over higher types and more.