A topos is a categorical model of constructive set theory. In particular, the eective topos is the
categorical 'universe' of recursive mathematics. Among its objects are the modest sets, which
form a set-theoretic model for polymorphism. More precisely, there is a bration of modest sets
which satises suitable categorical completeness properties, that make it a model for various
polymorphic type theories.
These lecture notes provide a reasonably thorough introduction to this body of material,
aimed at theoretical computer scientists rather than topos theorists. Chapter 2 is an outline of
the theory of brations, and sketches how they can be used to model various typed -calculi.
Chapter 3 is an exposition of some basic topos theory, and explains why a topos can be regarded
as a model of set theory. Chapter 4 discusses the classical PER model for polymorphism, and
shows how it 'lives inside' a particular topos|the eective topos|as the category of modest
sets. An appendix contains a full presentation of the internal language of a topos, and a map of
the eective topos.
Chapters 2 and 3 provide a sampler of categorical type theory and categorical logic, and
should be of more general interest than Chapter 4. They can be read more or less independently
of each other; a connection is made at the end of Chapter 3.
The main prerequisite for reading these notes is some basic category theory: limits and colimits,
functors and natural transformations, adjoints, cartesian closed categories. No knowledge
of indexed categories or categorical logic is needed. Some familiarity with 'ordinary' logic and
typed -calculus is assumed.
1