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 ((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.)

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

- Representable functors (another point of view on universal properties)
- Adjunctions (← everything before leads up to this!)
- Monads (will appear again in the M2 coalgebra course); Kleisli categories
- Various kinds of limits and colimits; preservation of limits by adjoints

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.

- monoidal categories
- monoid objects (general case)
- proofs-as-morphisms correspondence
- Girard–Kleisli construction

# 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*.