FOM: set theory in Martin-Loef's type theory

[William Tait]

Please, if you can, give me a good reference to a treatment of set 
theory in M-L's type theory, answering the question: what is a subset 
of a type. One reference I know is Martin-Loef's ``Intuitionistic
>Type Theory'', notes by G. Sambin of a series of lectures given in
>Padua, June 1980, Bibliopolis, Naples. But I am unable to locate a 
>copy of tyhis and, perhaps it is anyway out of date.

Bill Tait
--