CoursePlan

Category Theory

7.5hp, master level course, LP2 2020

Examiner: Thierry Coquand

Course Description

Category theory, with an origin in algebra and topology, has found use in recent decades for computer science and logic applications. Category Theory is an increasingly popular setting for describing the semantics of functional programming languages. There are other connections with functional programming: the categorical paradigm has influenced the language design, and given rise to several of the language elements (functions, functors, monads, arrows, ...). We expect students to previously have taken courses on Programming languages, Functional programming and Logic and to have some level of mathematical maturity. (The courses "Types for Programs and Proofs" or "Advanced Functional Programming" are also recommended.) We also expect students to have had contact with linear algebra and discrete mathematics in order to follow the motivating examples behind the theory expounded.

Overview

This course aims to give an introduction to Category Theory from first principles, following the book of Steve Awodey.

The students meet twice a week (2 x 2 hours) and present in turn one chapter of Awodey's book, and then discuss exercises.

We cover chapters 1 (Categories), 2 (Abstract structures), 3 (Duality), 5 (Limits and colimits), 6 (Exponentials), 7 (Functors and naturality), 8 (Categories of diagrams).

After the course is completed, students are expected to be able to follow and perform category theoretical arguments and diagram chases. Know about limits, colimits, adjunctions, exponentials, the Yoneda lemma.

Schedule

Chapter discussions happen at Wednesday 10 am (with the exception of the first week), and exercises sessions at Friday 10am.

All the meetings will take place on Zoom.

Fri 04/11 - Chapter 1 by Lukas (obs. no exercise session for Chapter 1)

Wed 11/11 - Chapter 2 by David

Wed 18/11 - Chapter 3 by Jeremy

Wed 25/11 - Chapter 5 by Oskar

Wed 02/12 - Chapter 6 by Andreas (obs. Chapter 4 skipped!)

Wed 09/12 - Chapter 7 by Nachi

Wed 16/12 - Chapter 8 by Lukas

Recommended exercises

Chapter 2:

1, 3, 4, 5, 13, 15, 16.
if you have time (optional): 8, 7, 9, 10, 14, 18. An object A in a category is called projective if for every epimorphism p : Y → X, every map f : A → X lifts against p in the sense that there is a map g : A → Y such that f = p g.

Chapter 3:

1, 2, 3, 6, 11, 14.
if you have time (optional): 7, 9, 13, 15.

Chapter 5:

1, 2(a), 3, 6, 7, 12
if you have time (optional): rest of 2, 10, 11 (hint: use the dual version of 7).

Chapter 6:

1, 2, 9, 12, 13.
if you have time (optional): 8, 11, 14.

Chapter 7:

4, 6, 7, 8, 9, 10.
if you have time, choose between (optional): 1+2+3, 12, 13, 15, 16, 17.

Chapter 8:

1, 2, 3, 6, 7, 8.
if you have time (optional): 4+5 (if you treated simplicial sets), 9+10 (of you treated the λ-calculus), 12(a)+13 (if you treated subobject classifiers).

Examination

Written examination at the end of the course.