Type theory was invented at the beginning of the twentieth century with the aim of avoiding the paradoxes which result from the self-application of functions. ?-calculus was developed in the early 1930s as a theory of functions. In 1940, Church added type theory to his ?-calculus giving us the influential simply typed ?-calculus where types were simple and never created by binders (or abstractors). However, realising the limitations of the simply typed ?-calculus, in the second half of the twentieth century we saw the birth of new more powerful typed ?-calculi where types are indeed created by abstraction. Most of these calculi use two binders ? and ? to distinguish between functions (created by ?-abstraction) and types (created by ?-abstraction). Moreover, these calculi allow ß-reduction but not ?-reduction. That is, (px·A. B)C ?B[x := C] is only allowed when p is ? but not when it is ?. This means that, modern systems do not allow types to have the same instantiation right as functions. In particular, when b has type B, the type of (?x:A.b)C is taken immediately to be B[x := C] instead of (Hx·A.B)C. Extensions of modern type systems with both Fl-reduction and type instantiation have appeared in (Kamareddine, Bloo and Nederpelt, 1999; Kamareddine and Nederpelt, 1996; Peyton-Jones and Meijer, 1997). This makes the ? and ? very similar and hence leads to the obvious question: why not use a unique binder instead of the ? and ?? This makes more sense since already, versions of de Bruijn's Automath unified ? and ? giving more elegant systems. This paper studies the main properties of type systems with unified ? and ?. © 2005 Cambridge University Press.