Practical Foundations of Mathematics

Paul Taylor

IV. Cartesian Closed Categories

INTRODUCTION

4.1    CATEGORIES

• Categories as theories
• Categories as congregations
• Categories as structures
• Size issues

4.2    ACTIONS AND SKETCHES

• Actions with a single sort
• Sketches
• Generating a category

4.3    CATEGORIES FOR FORMAL LANGUAGES

• Operational interpretation
• Logical interpretation
• Normal forms
• The category of contexts and substitutions
• Terms as sections
• Use of variables

4.4    FUNCTORS

• Constructions as functors
• A classifying category
• The force of functoriality
• Full and faithful

4.5    A UNIVERSAL PROPERTY: PRODUCTS

• The terminal object
• Unique up to unique isomorphism
• Products
• Preservation and creation of products
• Using the existence of products
• Universal properties give functors
• All universal properties are terminal objects

4.6    ALGEBRAIC THEORIES

• Examples
• Semantics of expressions
• The classifying category

4.7    INTERPRETATION OF THE LAMBDA CALCULUS

• The raw calculus
• Interpretation
• The b- and h-rules
• The universal property
• Cartesian closed categories of domains

4.8    NATURAL TRANSFORMATIONS

• Composition
• Equivalences
• Functor categories
• The Yoneda Lemma
• 2-Categories

EXERCISES  IV