Course pages 2015–16
Category Theory and Logic
- lecture 1 (9 Oct)
- lecture 2 (12 Oct)
- lecture 3 (16 Oct)
- lecture 4 (19 Oct)
- lecture 5 (23 Oct)
- lecture 6 (26 Oct)
- lecture 7 (30 Oct)
- lecture 8 (2 Nov)
- lecture 9 (6 Nov)
- lecture 10 (9 Nov)
- lecture 11 (13 Nov)
- lecture 12 (16 Nov)
- lecture 13 (20 Nov)
- lecture 14 (23 Nov)
- lecture 15 (27 Nov)
- lecture 16 (30 Nov)
- Lecture 1: Introduction; some history; content of this course. Definition of category. The category of sets and functions. Alternative definitions of category.
- Lecture 2: Commutative diagrams. 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: Informal notion of a "category-theoretic" property. Terminal objects. The opposite of a category and the duality principle. Initial objects. Free monoids as initial objects.
- Lecture 4: Binary products and coproducts.
- Lecture 5: I-ary products. Cartesian categories. Algebraic signatures. Terms over an algebraic signature and their interpretation in a cartesian category.
- Lecture 6: Equational Logic and its soundness for structures in a cartesian category. The internal language of a cartesian category. Algebraic theories as categories.
- Lecture 7: Exponential objects: in the category of sets and in general. Cartesian closed categories: definition and examples.
- Lecture 8: Intuitionistic Propositional Logic (IPL) in Natural Deduction style. Semantics of IPL in a cartesian closed pre-ordered set.
- Lecture 9: Simply Typed Lambda Calculus (STLC). Alpha equivalence of terms. The typing relation. Semantics of STLC types and terms in a cartesian closed category (ccc).
- Lecture 10: Capture-avoiding substitution for lambda terms. Semantics of substitution in a ccc. Soundness of the ccc semantics for beta-eta equality of lambda terms. The internal language of a ccc.
- Lecture 11: STLC theories as cccs. The Curry-Howard-Lawvere correspondence. Functors. Contravariance.
- Lecture 12: Identity and composition for functors. Size: small categories and locally small categories. The category of small categories. Finite products of categories.
- Lecture 13: Natural transformations. Functor categories. The category of small categories is cartesian closed.
- Lecture 14: Hom functors. Natural isomorphisms. Adjunctions. Examples of adjoint functors.
- Lecture 15: Theorem characterizing the existence of right (respectively left) adjoints in terms of a universal property.
- Lecture 16: Dependent types. Dependent product sets and dependent function sets as adjoint functors. Equivalence of categories. Example: the category of I-indexed sets and functions is equivalent to the slice category Set/I.
- Exercise Sheet 1
- Exercise Sheet 2 (with typo in last line of 7(b) corrected)
- Exercise Sheet 3
- Exercise Sheet 4 (solutions to this exercise sheet were graded and count for 25% of the final course mark)
- Exercise Sheet 5
- Exercise Sheet 6
- 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.