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

[Peter Schuster]

Bill Tait wrote: 

>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.

According to my opinion, these notes still are one of the most handy 
and comprehensive accounts of intuitionistic type theory. (They seem 
to be available, at least could be ordered last year through an Italian 
bookshop, whereas repeated attempts to order them by e-mail from 
Bibliopolis failed.)

However, for a recent theory of subsets in type theory that is built 
upon the general framework presented in those notes, see 

Sambin, Giovanni; Valentini, Silvio, 
Building up a toolbox for Martin-Löf's type theory: subset theory. 
= pp. 221--244 of: 
Sambin, Giovanni; Smith, Jan M., 
Twenty-five years of constructive type theory (Venice, 1995), 
Oxford Logic Guides, 36, Oxford Univ. Press, New York, 1998. 

Needless to say, this and the other contributions to type theory contained 
in this volume definitely aren't out of date. 

Peter Schuster.