Category Theory
Lecture slides
The lectures will be delivered live and recorded, with each recording available shortly after the lecture has finished.
A single pdf of all the slides, unannoted, but with hyperlinks, is here.
Individual pdfs for each lecture:
- Lecture 1 (8 Oct) Introduction; some history; content of this course. Definition of category. The category of sets and functions. Commutative diagrams. Alternative definitions of category. [video]
- Lecture 2 (11 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. [video]
- Lecture 3 (13 Oct) Terminal objects. The opposite of a category and the duality principle. Initial objects. Free monoids as initial objects. [video]
- Lecture 4 (15 Oct) Binary products and coproducts. [video]
- Lecture 5 (18 Oct) Exponential objects: in the category of sets and in general. Cartesian closed categories: definition and examples. [video]
- Lecture 6 (20 Oct) Intuitionistic Propositional Logic (IPL) in Natural Deduction style. Semantics of IPL in a cartesian closed pre-ordered set. [video]
- Lecture 7 (22 Oct) Simply Typed Lambda Calculus (STLC). Semantics of STLC types in a cartesian closed category (ccc). [video]
- Lecture 8 (25 Oct) Semantics of STLC terms as morphisms in a ccc. Capture-avoiding substitution and its semantics in a ccc. [video]
- Lecture 9 (27 Oct) 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. [video]
- Lecture 10 (29 Oct) Functors. Contravariance. Identity and composition for functors. Size: small categories and locally small categories. The category of small categories. [video]
- Lecture 11 (1 Nov) Natural transformations. Functor categories. The category of small categories is cartesian closed. [video]
- Lecture 12 (3 Nov) Adjunctions. Examples of adjoint functors. Hom functors. Natural isomorphisms. [video]
- Lecture 13 (5 Nov) Theorem characterizing the existence of right (respectively left) adjoints in terms of a universal property. [video]
- Lecture 14 (8 Nov) Dependent types. Dependent product sets and dependent function sets as adjoint functors. [video]
- Lecture 15 (10 Nov) Presheaf categories. The Yoneda lemma. Presheaf categories are cartesian closed. [video]
- Lecture 16 (12 Nov) Moggi's computational lambda calculus and its categorical semantics using (strong) monads. Notions of computation. Monads and adjunctions. [video]
Exercise sheets
- Exercise Sheet 1
- Exercise Sheet 2
- Exercise Sheet 3
- Exercise Sheet 4 (GRADED; worth 25% of final mark; upload solutions to Moodle by 12:00 on Friday 5 November.)
- Exercise Sheet 5
- Exercise Sheet 6
Solution notes for the excerises will be posted on the Moodle site.
Examples classes
The course has two one-hour Exercise/Help sessions:
- Tuesday 26 Oct 4-5pm
- Tuesday 16 Nov 4-5pm
Details of the arrangements for these sessions are on the Moodle site.
Office hours
For details see the Moodle site.
Additional material
See the syllabus for the recommended reading list. 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.
Other material:
- A student-oriented guide to on-line material on Category Theory is available at http://www.logicmatters.net/categories/.
- 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.