Abstract: A topos is a categorical model of constructive set theory. In particular, the effective 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 fibration of modest sets which satisfies 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 fibrations, and sketches how they can be used to model various typed lambda-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 effective 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 effective 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 lambda-calculus is assumed.
LFCS report ECS-LFCS-92-208Previous | Index | Next