About Me

I am a third year PhD student at the University of Manchester studying category theory and its relation to logic, supervised by Nicola Gambino.

My research centres around topics in internal category theory, $2$-topos theory, type theory, constructive logic and the intersection of these things.

I started out by constructing a model structure on the category of categories internal to an arithmetic $\Pi$-pretopos; this restricts to a model structure on the category of internal groupoids which forms a model of Martin-Löf type theory (MLTT). When the category in question is the category of sets, this recovers Hofmann and Streicher’s groupoidal model of MLTT, and gives a constructive proof of this and the existence of a model structure on $\mathbf{Cat}$.

In order to prove this result, I needed colimits in $\mathbf{Cat}(\mathcal{E})$. In joint work with Adrian Miranda, we worked out conditions on $\mathcal{E}$ which give finite $2$-colimits in $\mathbf{Cat}(\mathcal{E})$.

I am also interested in $2$-dimensional categorical foundations of mathematics. In work with Adrian Miranda on The Elementary Theory of the 2-Category of Small Categories (ET2CSC), we extend Lawvere’s elementary theory of the category of sets (ETCS) to a 2-dimensional setting. This gives an axiomatisation of the $2$-category of small categories.

One of the problems with ETCS (and hence ET2CSC) is that the internal logic cannot model any statements for which the axiom of replacement is used. In order to solve this in the 1-dimensional setting, we must look at the category of classes rather than the category of sets. Joyal and Moerdijk’s concept of a Class category aims to axiomatise the categorical properties of the category of classes in contrast to an elementary topos, which aims to axiomatise the category of sets. Similarly, in $2$-dimensions, we must move from the world of small categories to the world of locally small categories, ion which we can state the axiom of replacement. Our $2$-dimensional reformulation of Class categories gives a suitable environment for talking about a $2$-category with a well-behaved class of “small” objects. Our motivating example is the category of locally small categories, for which the small objects are the small categories.

I completed an MMath in Mathematics at the university of Sheffield in 2022. My MMath project was on the Dold-Kan correspondence, supervised by Prof. Sarah Whitehouse.