Preface
Part 0 Introduction to category theory
Introduction to Part 0
1 Categories and functors
2 Natural transformations
3 Adjoint functors
4 Equivalence of categories
5 Limits in categories
6 Triples
7 Examples of cartesian closed categories
Part I Cartesian closed categories and ๐-calculus
Introduction to Part I
Historical perspective on Part I
1 Propositional calculus as a deductive system
2 The deduction theorem
3 Cartesian closed categories equationally presented
4 Free cartesian closed categories generated by graphs
5 Polynomial categories
6 Functional completeness of cartesian closed categories
7 Polynomials and Kleisli categories
8 Cartesian closed categories with coproducts
9 Natural numbers objects in cartesian closed categories
10 Typed ๐-calculi
11 The cartesian closed category generated by a typed ๐-calculus
12 The decision problem for equality
13 The Church-Rosser theorem for bounded terms
14 All terms are bounded
15 C-monoids
16 C-monoids and cartesian closed categories
17 C-monoids and untyped ๐-calculus
18 A construction by Dana Scott
Historical comments on Part I
Part II Type theory and toposes
Introduction to Part II
Historical perspective on Part II
1 Intuitionistic type theory
2 Type theory based on equality
3 The internal language of a topos
4 Peano's rules in a topos
5 The internal language at work
6 The internal language at work II
7 Choice and the Boolean axiom
8 Topos semantics
9 Topos semantics in functor categories
10 Sheaf categories and their semantics
11 Three categories associated with a type theory
12 The topos generated by a type theory
13 The topos generated by the internal language
14 The internal language of the topos generated
15 Toposes with canonical subobjects
16 Applications of the adjoint functors between toposes and type theories
17 Completeness of higher order logic with choice rule
18 Sheaf representation of toposes
19 Completeness without assuming the rule of choice
20 Some basic intuitionistic principles
21 Further intuitionistic principles
22 The Freyd cover of a topos
Historical comments on Part II
Supplement to Section 17
Part III Representing numerical functions in various categories
Introduction to Part III
1 Recursive functions
2 Representing numerical functions in cartesian closed categories
3 Representing numerical functions in toposes
4 Representing numerical functions in C-monoids
Historical comments on Part III
Bibliography
Author index
Subject index