An introduction to fibrations, topos theory, the effective topos and modest sets

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