Advanced Topics in Category Theory

Teaching

The teaching style will be largely based on lectures, but supported by a practical component where students will learn to use a proof assistant for higher category theory.

Aims

The module will introduce advanced topics in category theory. The aim is to train students to engage and start modern research on the mathematical foundations of higher categories, the graphical calculus, logical systems, programming languages, type theories, and their applications in theoretical computer science, both classical and quantum.

Objectives

On completion of this module, students should:

• Be familiar with the techniques of compositional category theory.
• Have a strong understanding of basic categorical semantic models.
• Have glimpsed current research in higher categorical structures.

Syllabus

• Monoidal categories and the graphical calculus (Lectures 1 and 2)
• Coherence, higher categories (Lectures 3 and 4)
• Linearity, superposition (Lecture 5)
• Duality, quantum entanglement (Lecture 6)
• Monoids, Frobenius algebras, and bialgebras (Lectures 7 and 8)
• Monoidal models of dualities (Lecture 9)
• Presheaves and profunctors (Lectures 10 and 11)
• Combinatorial structures (Lecture 12)
• Polynomial functors (Lectures 13 and 14)
• Models of linear logic (Lectures 15 and 16)

Practical

There will be 4 practical sessions where students will be guided to use the proof assistant homotopy.io. These would take place in the computer room, but could be delivered over Zoom if required, since the tool is web-based and can be easily accessed from any location.
Once students gain an understanding of the tool, they will choose problems to attempt from a long list of suggestions, of varying difficulty, from easy bookwork to research-level. 
At the end of the course, students will be required to submit 5 homotopy.io project workspaces, demonstrating their best work using the system. At least 3 of these workspaces should be attempts on research-level problems. The practical portfolio will be graded and form part of the assessment of the course.
No special computing resources are required, the tool runs adequately on an ordinary laptop.

Classes

There will be 4 exercise sheets for homework, and 4 classes taught by a TA from the lecturers’ research group. These exercise sheets will be graded and form part of the assessment of the course.

Assessment

• Graded exercise sheets (70%)
• Practical portfolio (30%)

Reading List

Chris Heunen and Jamie Vicary, “Category for Quantum Theory: An Introduction”, Oxford University Press

Further Information

Due to COVID-19, the method of teaching for this module will be adjusted to cater for physical distancing and students who are working remotely. We will confirm precisely how the module will be taught closer to the start of term.