Category theory provides a principled mathematical language for compositionality, that is, for describing how systems can be built out of simpler parts. It is for this reason heavily used in many subfields of “logic in computer science” (for example, semantics of programming languages). The goal of this course is to develop some fluency in the basics of the language of categories commonly used in the research-level literature in these fields.

Prerequisites

A familiarity with basic abstract algebra (monoids, groups, homomorphisms) and some mathematical maturity concerning algebraic reasoning is expected. We will however avoid sophisticated algebraic-topological examples that are typical of category theory courses for pure mathematicians.

It is useful (although not necessary) to have followed the M1 Proofs and Programs course to have some previous exposure to denotational semantics, one of the traditional application areas for categories.

Syllabus

Lectures are 2 hours long, on Tuesdays at 15:45 and Thurdays at 8:00, room B1.

The course is divided into two parts:

• Basic concepts of category theory 10 lectures over 5 weeks (21 Nov – 21 Dec), detailed below.
• Categorical semantics of proofs in linear logic: 3 weeks of lectures in January by Olivier Laurent, with details on this webpage. The material covered should roughly be:
  • monoidal categories
  • monoid objects
  • proofs-as-morphisms correspondence
  • Girard–Kleisli construction

Lecture 1 (21 Nov). Motivation for category theory: semantics of programming languages requires an axiomatic theory of “composable stuff” that goes beyond “structured sets and structure-preserving maps”; mathematicians came up with their own to do algebra and topology, we reuse it. Reminders on monoids, groups, homomorphisms and isomorphisms. An example of categorical thinking: proof that the free monoid over a set X – concretely, the monoid of lists of elements in X – is characterized up to isomorphism by its universal property. Definition of a category, and of (locally) small categories.

(Remark: while we focused on motivation related to semantics, applications of category theory to state-based system are covered in the M2 Coalgebra course (CR17) by Damien Pous and Valeria Vignudelli. The keyword “applied category theory” refers to yet another kind of applications.)

Homework 1: for 28 November. You are advised to start with doing questions 1 and 2 in Exercise 2, which only require the material covered in the first lecture.

Lecture 2 (23 Nov). Examples of categories: Set (sets and functions), Mon (monoids and homomorphisms), Rel (sets and relations), empty category. Monoids are “the same as” small categories with 1 object. Monoid of endomorphisms of an object; isomorphisms between 2 objects; group of automorphisms of an object. Subcategories: full (e.g. groups in Mon), wide (e.g. bijections in Set), or neither (e.g. FinBij in Set). Functors F : C → D between two categories: identity functor; forgetful functor U : Mon → Set; inclusion functor of a subcategory; (-)² : Set → Set. Universal morphisms from an object to a functor or vice versa; rephrasing of the universal property of the free monoid.

(Remark: the category FinBij whose objects are finite sets and morphisms are bijections is useful for combinatorics.)

Lecture 3 (28 Nov). Reminders on partial orders. Correspondence between preordered sets (e.g. prefix preorder on a monoid) and small categories with at most 1 morphism between any two objects. The category PreOrd of preordered sets and monotone functions, and its full subcategory Ord of posets. Composition of functors; the category Cat of categories. Parameterized data structures (pairs, lists, option type) as endofunctors on Set. Opposite categories, duality (between universal morphisms from X to F, and from F to X), contravariant functors (e.g. powerset with inverse image). The hom-functors C(A,–) and C(–,A).

(The use of the functorial structure of data types is pervasive in Haskell programming. For an introduction to categories as generalization of ordered sets, see these notes by Vincent Moreau. The prefix preorder on a monoid is also known as the reverse of Green’s relation R which plays an important role in automata theory.)

Homework 2: due on 5 December.

Lecture 4 (30 Nov). Duality is symmetric ((C^op)^op = C). Product of categories; hom-bifunctor C(–,–) : C^op × C → C. Uniqueness up to unique isomorphism (preserving the structure) as a general theorem on universal morphisms. Product of an I-indexed family of objects (as a universal morphism into the diagonal functor Δ : C → C^I); notation A×B (potentially ambiguous/misleading!); Examples in Set, Rel (disjoint sum), Ord, Mon. Terminal objects. In a category corresponding to a preorder: terminal = maximum element; product = infimum of a family. Dual concepts: coproducts, initial objects.

(“cocoproducts” would just be products; “a comathematician turns cotheorems into ffee”. Warning: the notation 1 for a terminal object – used in Homework 2 – is incompatible with the notations for linear logic that will be used in the second half of the course. But the 0 of linear logic does correspond to an initial object.)

Lecture 5 (5 Dec). Examples of initial objects and coproducts (in Mon/Grp: singletons are initial; coproducts exist but are complicated). Cartesian categories: chosen products and terminal objects (and dually: cocartesian categories). Up to isomorphism, × is commutative, unital and associative – proof of the latter via ternary products (cartesian categories have all finite products). Extension of × on objects to a functor. Natural transformations (motivation: in what way is this functor compatible with the aforementioned isos?).

(Cartesian categories are a typical example of structure, not just property!)

Homework 3: due on 12 December.

Lecture 6 (7 Dec). Generic functions between data structures (e.g. Option ⇒ List) as natural transformations. Naturality of structural morphisms in a cartesian category. Combining natural transformations and functors. Category of functors [C,D]; natural isomorphisms. Isomorphism of categories between Rel and Rel^op versus equivalence of categories between Set/I and Set^I. The correspondence between monoids (resp. preorders) and small categories with 1 object (resp. with …) is an equivalence of categories. Full, faithful and essentially surjective functors; FinSet is equivalent to a full subcategory with 1 set for each cardinality.

(Set/I is the slice category of Set over I ∈ ob(Set); its equivalence with Set^I is the simplest example of an important pattern (e.g. fibrations vs indexed categories, …) that appears in the semantics of dependent type theory.)

Lecture 7 (12 Dec). Horizontal composition of natural transformations. Proof of interchange law. Equivalences of categories can be composed: “being equivalent” is indeed an equivalence relation on categories. Representable functors e.g. pairs as Set({1,2},–) or Mon({1,2}*,–); contravariant powerset functor. Products vs representability, pairing of two morphisms X → A and X → B. For F : C → D, correspondence between representations of D(X,F(–)) and universal morphisms from X to F.

Homework 4: due on 19 December.

Lecture 8 (14 Dec). Examples of the above correspondence (free monoids; binary (co)products; Set((–)×A,B) ≅ Set(–,A→B) yields the evaluation map with its universal property). Unique extension of a family of universal morphisms from X to F (resp. F to X) for each X into a left adjoint (resp. right adjoint) functor equipped with a natural unit (resp. counit), e.g. the free monoid functor with the “List.map operation”. Left/right adjoints are unique up to unique natural isomorphism. The “representable” point of view: L is left adjoint to R ⇔ C(L(X),A) ≅ D(X,R(A)) naturally in both X and A ⇔ (miraculously) R is right adjoint to L. The counit of the free/forgetful adjunction between monoids and sets is related to “fold” in functional programming.

(Actually, it’s precisely Haskell’s mconcat.)

Lecture 9 (19 Dec). Examples of adjunctions (previous examples of universal morphisms; Set/Rel with covariant powerset; left and right adjoints to forgetful functor PreOrd → Set), with their units and counits. Non-example: the forgetful functor Mon → Set has no right adjoint (no proof yet). Composition of adjunctions. Triangle identities → alternative definition of adjunctions. Monads defined as (M,μ,η) where η : Id ⇒ M is the unit of an adjunction and µ : M∘M ⇒ M is derived from its counit. Examples over Set: List (via Mon), covariant powerset (via Rel), state monad (product/arrow adjunction). Intuition: monads over Set model effectful computations. “Bind” operation x >>= f for x ∈ M(A) and f : A → M(B).

Homework 5: a bit longer than usual, due on 16 January.

Lecture 10 (21 Dec). Canceled because of a campus blockade protesting against the recent immigration bill. Here’s a handout covering the material that was supposed to be in this lecture. (Kleisli categories, monads as internal monoids in categories of endofunctors. Representable and adjoint functors preserve products. Very quick introduction to (co)limits.)

References

• Steve Awodey, Category Theory
• Benjamin Pierce, Basic Category Theory for Computer Scientists

More mathematically-inclined students may also consult Emily Riehl’s Category Theory in Context.