(CR15) Category theory for computer scientists, M2 ÉNS Lyon, 2023–2024

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.

Basic concepts of category theory

10 lectures over 5 weeks (21 Nov – 21 Dec).

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 ((Cop)op = C). Product of categories; hom-bifunctor C(–,–) : Cop × 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 → CI); 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 Relop versus equivalence of categories between Set/I and SetI. 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 SetI is the simplest example of an important pattern (e.g. fibrations vs indexed categories, …) that appears in the semantics of dependent type theory.)

The following lectures will be mostly dedicated to the following fundamental notions:

If time allows (probably not…): monomorphisms and epimorphisms; algebras over a functor/monad; the Yoneda lemma and categories of preshaves.

Categorical semantics of λ-calculus and linear logic

3 weeks of lectures in January by Olivier Laurent.

References

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