Higher categories and logic

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.