Abstract

This talk will mainly be concerned with notions of largeness in constructive set theory and type theory.

The introduction of universes in Martin-Loef type theory resembles in many aspects the process of extending classical set theory via large cardinal axioms, and can thus be considered a constructivist's large cardinal programme.

Certain systems of intuitionistic set theory, like Aczel's ``Constructive Zermelo Fraenkel Set Theory'', CZF, have canonical interpretations in Martin-Loef type theory. They lend themselves to investigate notions of largeness that arise from universes, i.e. large sets. The latter turn out to be classically equivalent to well known large cardinal notions. CZF also allows for a sensible theory of large sets in that many of their classically known properties can be proved on the basis of CZF. On the other hand, extensions of CZF by large set axioms have surprisingly little consistency strength.