| Preface | |
| Introduction to category theory | |
| Introduction to Part 0 | p. 3 |
| Categories and functors | p. 4 |
| Natural transformations | p. 8 |
| Adjoint functors | p. 12 |
| Equivalence of categories | p. 16 |
| Limits in categories | p. 19 |
| Triples | p. 27 |
| Examples of cartesian closed categories | p. 35 |
| Cartesian closed categories and [lambda]-calculus | |
| Introduction to Part I | p. 41 |
| Historical perspective on Part I | p. 42 |
| Propositional calculus as a deductive system | p. 47 |
| The deduction theorem | p. 50 |
| Cartesian closed categories equationally presented | p. 52 |
| Free cartesian closed categories generated by graphs | p. 55 |
| Polynomial categories | p. 57 |
| Functional completeness of cartesian closed categories | p. 59 |
| Polynomials and Kleisli categories | p. 62 |
| Cartesian closed categories with coproducts | p. 65 |
| Natural numbers objects in cartesian closed categories | p. 68 |
| Typed [lambda]-calculi | p. 72 |
| The cartesian closed category generated by a typed [lambda]-calculus | p. 77 |
| The decision problem for equality | p. 81 |
| The Church-Rosser theorem for bounded terms | p. 84 |
| All terms are bounded | p. 88 |
| C-monoids | p. 93 |
| C-monoids and cartesian closed categories | p. 98 |
| C-monoids and untyped [lambda]-calculus | p. 101 |
| A construction | p. 107 |
| Historical comments on Part I | p. 114 |
| Type theory and toposes | |
| Introduction to Part II | p. 123 |
| Historical perspective on Part II | p. 124 |
| Intuitionistic type theory | p. 128 |
| Type theory based on equality | p. 133 |
| The internal language of a topos | p. 139 |
| Peano's rules in a topos | p. 145 |
| The internal language at work | p. 148 |
| The internal language at work II | p. 153 |
| Choice and the Boolean axiom | p. 160 |
| Topos semantics | p. 164 |
| Topos semantics in functor categories | p. 169 |
| Sheaf categories and their semantics | p. 177 |
| Three categories associated with a type theory | p. 186 |
| The topos generated by a type theory | p. 189 |
| The topos generated by the internal language | p. 193 |
| The internal language of the topos generated | p. 196 |
| Toposes with canonical subobjects | p. 200 |
| Applications of the adjoint functors between toposes and type theories | p. 205 |
| Completeness of higher order logic with choice rule | p. 212 |
| Sheaf representation of toposes | p. 217 |
| Completeness without assuming the rule of choice | p. 223 |
| Some basic intuitionistic principles | p. 226 |
| Further intuitionistic principles | p. 231 |
| The Freyd cover of a topos | p. 237 |
| Historical comments on Part II | p. 244 |
| Supplement to Section 17 | p. 250 |
| Representing numerical functions in various categories | |
| Introduction to Part III | p. 253 |
| Recursive functions | p. 253 |
| Representing numerical functions in cartesian closed categories | p. 257 |
| Representing numerical functions in toposes | p. 264 |
| Representing numerical functions in C-monoids | p. 271 |
| Historical comments on Part III | p. 277 |
| Bibliography | p. 279 |
| Author index | p. 289 |
| Subject index | p. 291 |
| Table of Contents provided by Syndetics. All Rights Reserved. |
