Abstract

The concept of an elementary topos can be seen as a generalisation of the category of sets. Every topos possesses an internal language which can be used to reason about its objects. By retaining enough structure from the category of sets we get a powerful internal language that allows us to reason in familiar, “set-like” ways. However, the internal language differs from set theories, such as ZF, in several ways. In particular, the law of excluded middle does not (in general) hold inside a topos.

• The definition of a topos
• Examples of topoi/toposes
• Properties and alternative definitions
• The internal language of a topos
• Using the internal language

• Familiarity with basic category theory, particularly the category of sets
• Familiarity with the simply typed lambda calculus as the internal language for CCCs. See here, lectures 9-11 for details.