Department of Computer Science and Technology

Course pages 2018–19

Category Theory

Lecture slides

  • Lecture 1 (9 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 (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.
  • Lecture 3 (16 Oct) Terminal objects. The opposite of a category and the duality principle. Initial objects. Free monoids as initial objects.
  • Lecture 4 (18 Oct) Binary products and coproducts.
  • Lecture 5 (23 Oct) Exponential objects: in the category of sets and in general. Cartesian closed categories: definition and examples.
  • Lecture 6 (25 Oct) Intuitionistic Propositional Logic (IPL) in Natural Deduction style. Semantics of IPL in a cartesian closed pre-ordered set.
  • Lecture 7 (30 Oct) Simply Typed Lambda Calculus (STLC). Semantics of STLC types in a cartesian closed category (ccc).
  • Lecture 8 (1 Nov) Semantics of STLC terms as morphisms in a ccc. Capture-avoiding substitution and its semantics in a ccc.
  • Lecture 9 (6 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 (8 Nov) Functors. Contravariance. Identity and composition for functors. Size: small categories and locally small categories. The category of small categories.
  • Lecture 11 (13 Nov) Natural transformations. Functor categories. The category of small categories is cartesian closed.
  • Lecture 12 (15 Nov) Adjunctions. Examples of adjoint functors. Hom functors. Natural isomorphisms.
  • Lecture 13 (20 Nov) Theorem characterizing the existence of right (respectively left) adjoints in terms of a universal property.
  • Lecture 14 (22 Nov) Dependent types. Dependent product sets and dependent function sets as adjoint functors.
  • Lecture 15 (27 Nov) Presheaf categories. The Yoneda lemma.
  • Lecture 16 (29 Nov) The Yoneda functor is full and faithful. Presheaf categories are cartesian closed.

Exercise sheets

Office hours

  • The module lecturer will be available to answer questions about the course material and exercises on Fridays between 9:00 and 10:00 in FC08 during Full Term.

Additional material