About Me

I am a fourth year PhD student in the University of Manchester’s category theory group 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.

In particular, I am interested in logical properties of $2$-categories of internal categories, and $(2,1)$-categories of internal groupoids. It is possible to show that given certain axioms on $\mathcal{E}$, the $(2,1)$-category $\mathbf{Gpd}(\mathcal{E})$ forms a model of Martin-Löf type theory. In some sense, this can be seen as its internal language.

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})$. We also give a converse result of this. See the preprint here.

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. Restricting to $\mathbf{Gpd}(\mathcal{E})$, the $(2,1)$-categorical axiom of choice can be interpretted in Martin-L"{o}f type theory, giving a new formulation of the type theoretic axiom of choice. Note that we can also do this in the constructive setting, as with Palmgren’s constructive elementary theory of the category of sets, and obtain a type theoretic formulation of the presentation axiom, a weaker choice principle. Interpreting this in type theory gives a type theoretic choice principle which is novel.

One of the problems with ETCS (and hence ET2CSC) is that the internal logic cannot model any statements in Zermelo-Fraenkel set theory with choice (ZFC) 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 Von Neuman-Bernays-G"{o}del set theory (NBG) in contrast to an elementary topos, which aims to axiomatise the category of sets in ZFC. Similarly, in $2$-dimensions, we must move from the world of small categories to the world of large categories, in 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 $2$-category of “small” objects. Our motivating example is the category of large categories, for which the small objects are the small categories. Other such examples are given by categories of (pre)stacks over a small category $\mathbb{C}$, and categories internal to the category of assemblies on a partial combinatorial algebra. These examples motivate connections between $2$-dimensional logic and topics in algebraic geometry and computability theory.

I am the maintainer of the University of Manchester’s Category Theory Group website.

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.