In 1986 Martin-Löf proposed a reformulation of intuitionistic type theory; see Nordström, Peterson and Smith (1990) for an exposition. The purpose was to give a more compact formulation, where \(\lambda\) and \(\Pi\) are the only variable binding operations. It is nowadays considered the main version of the theory. It is also the basis for the Agda proof assistant. The 1986 theory has two parts: