Computer Laboratory

Course pages 2014–15

Category Theory and Logic

Lecture slides

Lecture summaries

  • 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: posets and monotone functions; monoids and monoid homomorphisms; a poset as a category; a monoid as a category. Definition of isomorphism. Informal notion of a "category-theoretic" property.
  • Lecture 3: Terminal objects. The opposite of a category and the duality principle. Initial objects. Free monoids as initial objects.
  • Lecture 4: Binary products and coproducts. I-ary products. Cartesian categories.
  • Lecture 5: 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 poset.
  • 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.
  • Lecture 11: The internal language of a ccc. 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 sheets

Additional material

  • The classic text on category theory is
    Mac Lane, Saunders. Categories for the Working Mathematician. Graduate Texts in Mathematics 5, second ed. (Springer, 1988), ISBN 0-387-98403-8.
    and is definitely worth looking at if you are feeling mathematically mature.
  • 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.