Course pages 2019–20
Category Theory
Lecture slides
- Lecture 1 (10 Oct) Introduction; some history; content of this course. Definition of category. The category of sets and functions. Commutative diagrams. Alternative definitions of category.
- Lecture 2 (15 Oct) Examples of categories: pre-ordered sets and monotone functions; monoids and monoid homomorphisms; a pre-ordered set as a category; a monoid as a category. Definition of isomorphism.
- Lecture 3 (17 Oct) Terminal objects. The opposite of a category and the duality principle. Initial objects. Free monoids as initial objects.
- Lecture 4 (22 Oct) Binary products and coproducts.
- Lecture 5 (24 Oct) Exponential objects: in the category of sets and in general. Cartesian closed categories: definition and examples.
- Lecture 6 (29 Oct) Intuitionistic Propositional Logic (IPL) in Natural Deduction style. Semantics of IPL in a cartesian closed pre-ordered set.
- Lecture 7 (31 Oct) Simply Typed Lambda Calculus (STLC). Semantics of STLC types in a cartesian closed category (ccc).
- Lecture 8 (5 Nov) Semantics of STLC terms as morphisms in a ccc. Capture-avoiding substitution and its semantics in a ccc.
- Lecture 9 (7 Nov) Soundness of the ccc semantics for beta-eta equality of lambda terms. The internal language of a ccc. Free cccs. The Curry-Howard-Lawvere/Lambek correspondence.
- Lecture 10 (12 Nov) Functors. Contravariance. Identity and composition for functors. Size: small categories and locally small categories. The category of small categories.
- Lecture 11 (14 Nov) Natural transformations. Functor categories. The category of small categories is cartesian closed.
- Lecture 12 (19 Nov) Adjunctions. Examples of adjoint functors. Hom functors. Natural isomorphisms.
- Lecture 13 (21 Nov) Theorem characterizing the existence of right (respectively left) adjoints in terms of a universal property.
- Lecture 14 (26 Nov) Dependent types. Dependent product sets and dependent function sets as adjoint functors.
- Lecture 15 (3 Dec) Presheaf categories. The Yoneda lemma.
- Lecture 16 (5 Dec at 10am) The Yoneda functor is full and faithful. Presheaf categories are cartesian closed.
Office hours
- The module lecturer will be available to answer questions about the course material and exercises on Mondays between 14:00 and 15:00 in FC08 during Full Term.
Additional material
- The following is the classic text on category theory and is
definitely worth looking at if you are feeling mathematically
mature:
Mac Lane, Saunders. Categories for the Working Mathematician. Graduate Texts in Mathematics 5, second ed. (Springer, 1988), ISBN 0-387-98403-8.
- A student-oriented guide to on-line material on Category Theory is available at http://www.logicmatters.net/categories/.
- The Category Theory Seminar is held in Centre for Mathematical Sciences.
- Category Theory in the nLab.
- The Catsters' Category Theory Videos.
- Eugenia Cheng's book on Cakes, Custard and Category Theory (published in the US under the title "How to Bake Pi").
- David Spivak's book on Category Theory for the Sciences.
- The Applied Category Theory web site.