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

**Wesley Phoa**
*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-208*

This is a 150-page report which is available as a 1Mb PostScript file or as a 315kb gzipped PostScript file.

Previous |

Index |

Next