Course pages 2016–17
Category Theory and Logic
Lecture slides and notes
- Lecture 1 (7 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 (10 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 (14 Oct) Terminal objects. The opposite of a category and the duality principle. Initial objects. Free monoids as initial objects.
- Lecture 4 (17 Oct) Binary products and coproducts.
- Lecture 5 (21 Oct) Exponential objects: in the category of sets and in general. Cartesian closed categories: definition and examples.
- Lecture 6 (24 Oct) Intuitionistic Propositional Logic (IPL) in Natural Deduction style. Semantics of IPL in a cartesian closed pre-ordered set.
- Brief notes on the category theoretic semantics of Simply Typed Lambda Calculus.
- Lecture 7 (28 Oct) Simply Typed Lambda Calculus (STLC). Alpha equivalence of terms. The typing relation. Semantics of STLC types in a cartesian closed category (ccc).
- Lecture 8 (31 Oct) Semantics of STLC terms as morphisms in a ccc. Capture-avoiding substitution for lambda terms. Semantics of substitution in a ccc.
- Lecture 9 (4 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 (7 Nov) Functors. Contravariance. Identity and composition for functors. Size: small categories and locally small categories. The category of small categories. Finite products of categories.
- Lecture 11 (11 Nov) Natural transformations. Functor categories. The category of small categories is cartesian closed.
- Lecture 12 (14 Nov) Adjunctions. Examples of adjoint functors. Hom functors. Natural isomorphisms.
- Lecture 13 (18 Nov) Theorem characterizing the existence of right (respectively left) adjoints in terms of a universal property.
- Lecture 14 (21 Nov) Dependent types. Dependent product sets and dependent function sets as adjoint functors.
- Lecture 15 (25 Nov) Equivalence of categories. Example: the category of I-indexed sets and functions is equivalent to the slice category Set/I. Presheaf categories. The Yoneda functor.
- Lecture 16 (28 Nov) The Yoneda lemma. Presheaf categories are cartesian closed.
- Exercise Sheet 1 (Solutions)
- Exercise Sheet 2 (Solutions)
- Exercise Sheet 3 (Solutions)
- Exercise Sheet 4 (Solutions)
- Exercise Sheet 5 (Solutions)
- Exercise Sheet 6 (Solutions)
- The module lecturer will be available to answer questions about the course material and exercises on Wednesdays between 12:00 and 13:00 in FC08 during Full Term.
- The following is the classic text on category theory and is
definitely worth looking at if you are feeling mathematically
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 at 2.15pm on Tuesdays in Room MR5 of the Centre for Mathematical Sciences.
- Julia Goedecke's Category Theory course for the 2013/4 Mathematical Tripos Part III / Masters of Mathematics.
- 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").