skip to primary navigationskip to content

Department of Computer Science and Technology



Course pages 2022–23

Advanced Topics in Category Theory

Principal lecturers: Prof Marcelo Fiore, Dr Jamie Vicary
Taken by: MPhil ACS, Part III
Code: L118
Term: Lent
Hours: 16
Prerequisites: Category Theory
Moodle, timetable


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.


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.


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.


  • 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)
  • Presheaf categories (Lectures 10, 11, and 12)
  • Models of abstract syntax (Lecture 13 and 14)
  • Normalisation by evaluation (Lectures 15 and 16)


There will be 4 practical sessions where students will be guided to use the proof assistant 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 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.


There will be four exercise sheets for optional homework with accompanying classes by a teaching assistant to go over them.


  • Take-home test (65%)
  • Practical portfolio (35%)

Reading List

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

Further Information

Due to infectious respiratory diseases, the method of teaching for this module may be adjusted to cater for physical distancing and students who are working remotely. Unless otherwise advised, this module will be taught in person.