Relating set theories and type theories via categorical logic

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.