 (e) Martin-Löf type theory is an intuitionist theory of dependent types intended to be a full scale system for formalizing constructive mathematics. Its origins of can be traced to Principia Mathematica, Hilbert’s Über das Unendliche, the natural deduction systems of Gentzen, taken in conjunction with Prawitz’s reduction procedures, and to Gödel’s Dialectica system. It incorporates inductively defined data types which together with the vehicle of internal reflection via universes endow it with considerable consistency strength.