This talk describes work in progress on a form of constructive type theory featuring the simple computational effect of generating fresh names combined with name equality, name swapping and name abstraction. The motivation is to try to extend the FreshML functional programming language (or more precisely, a fragment of it with only totally defined functions) to a dependently typed language. FreshML provides user-friendly support for writing syntax-manipulating programs featuring structural recursion "modulo alpha-conversion"; but it does so using generative names. The aim is to obtain a constructive type theory in which such programs can also express (via a Curry-Howard style correspondence) proofs by structural induction modulo alpha-conversion. In such a type theory terms can involve generative names and types can depend upon terms; therefore types involve generative names. To understand the properties of such types, I am guided by a relatively simple model using nominal sets.