文档介绍：Introduction to
CATEGORY THEORY
and
CATEGORICAL LOGIC
Thomas Streicher
SS 03 and WS 03/04
Contents
1 Categories 5
2 Functors and Natural Transformations 9
3 Subcategories, Full and Faithful Functors, Equivalences 14
ma Categories and Slice Categories 16
5 Yoneda Lemma 17
6 Grothendieck universes : big vs. small 20
7 Limits and Colimits 22
8 Adjoint Functors 36
9 Adjoint Functor Theorems 46
10 Monads 52
11 Cartesian Closed Categories and λ–Calculus 63
Exponentials in Presheaf Categories . . . . . . . . . . . . . . . 64
Categorical semantics of typed λ-calculus c’s . . . . . . . 68
12 Elementary Toposes 76
13 Logic of Toposes 85
14 Some Exercises in Presheaf Toposes 105
15 Sheaves 110
1
Introduction
The aim of this course is to give an introduction to the basic notions of
Category Theory and Categorical Logic.
The first part on Category Theory should be of interest to a general math-
ematical audience with interest in algebra, geometry and topology where at
least the language of category theory and some of its basic notions like lim-
its, colimits and adjoint functors are indispensible nowadays. However, for
following the lectures in a profitable way one should have already attended a
course in basic algebra or topology because algebraic structures like groups,
rings, modules etc. and topological spaces serve as the most important source
of examples illustrating the abstract notions introduced in the course of the
lectures.
The second part will be of interest to people who want to know about logic
and how it can be modelled in categories. In particular, we will present
cartesian closed categories where one can interpret typed λ-calculus, the
basis of modern functional programming languages, and (elementary) toposes
providing a most concise and simple notion of model for constructive higher
order logic. Guiding examples for both notions will be presented en detail.
Some knowledge about constructive logic would b