FOM: set theory in Martin-Loef's type theory
pschust at rz.mathematik.uni-muenchen.de
Thu Aug 2 06:54:12 EDT 2001
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
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.
More information about the FOM