Higher categories and logic
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
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.
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.
Organisations
People |
ORCID iD |
Yakov Kremnizer (Primary Supervisor) | |
Christopher Dean (Student) |
Studentship Projects
Project Reference | Relationship | Related To | Start | End | Student Name |
---|---|---|---|---|---|
EP/N509711/1 | 30/09/2016 | 29/09/2021 | |||
1734032 | Studentship | EP/N509711/1 | 02/10/2016 | 30/03/2020 | Christopher 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 |