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