Relating set theories and type theories via categorical logic

Lead Research Organisation: University of Leeds
Department Name: Pure Mathematics


Ever since the fundamental work of Aczel in the '60s, the study of the relationship between constructive set theories and constructive type theories has been a very important topic of research. Further impetus in this area has been given by the recent development of Homotopy Type Theory.

The aim of this project is to develop further categorical logic so as to provide a unified account of the plethora of type-theoretic interpretations of constructive set theories, thereby providing a clear understanding of their relationship. This will require significant and challenging technical work in extending the framework of Algebraic Set Theory to allow for interpretations of logic other than the standard propositions-as-subobjects one, in order to encompass some examples of type-theoretic interpretations of set theories that use the propositions-as-types or propositions-as-h-props paradigms. Potential applications include the creation of new models of constructive set theories by considering examples in known categorical models of type theory (groupoids, simplicial sets). These may lead to new applications to relative consistency and independence results.


10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/R513258/1 30/09/2018 29/09/2023
2438979 Studentship EP/R513258/1 30/09/2020 31/03/2024 Matteo Spadetto
EP/T517860/1 30/09/2020 29/09/2025
2438979 Studentship EP/T517860/1 30/09/2020 31/03/2024 Matteo Spadetto