Higher categories and logic

Lead Research Organisation: University of Oxford
Department Name: Computer Science


This project falls within the EPSRC Mathematical Sciences theme.

My interests revolve around category theory, its connections to logic and higher category theory. For me, a key attraction of this area is its ability to provide a natural language for generalising and unifying a wide variety of topics. Many mathematical structures can be studied using category theory and this perspective highlights many important features and constructions. Higher category theory extends this perspective so that even more mathematics can be captured. It naturally arises when studying category theory using category theory. Higher category theory is also deeply connected to topology. Diagrammatic methods can be used to reason about higher categories. Graphical calculi are prominent in the study of categorical quantum mechanics. The deep connections between mathematics, computer science and logic exemplied by the Curry-Howard-Lambek correspondence are a particular interest. Much work still needs to be done to extend these correspondences from categories to higher categories. One side of this interest is type theory including homotopy type theory.


10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509711/1 01/10/2016 30/09/2021
1734032 Studentship EP/N509711/1 03/10/2016 31/03/2020 Christopher James Dean
Description New approaches to higher category theory and type theory are being developed.
Exploitation Route The work should help with further research in in a number of areas of mathematics as well as potential computer proof assistants for mathematics .
Sectors Digital/Communication/Information Technologies (including Software)

URL http://conferences.inf.ed.ac.uk/ct2019/slides/67.pdf