Calum Hughes

Calum Hughes

PhD student studying category theory and logic at the University of Manchester.

Publications

The algebraic groupoid model of Martin-Löf type theory

Published in , 2025

We extend the model structure on the category $\mathbf{Cat}(\mathcal{E})$ of internal categories studied by Everaert, Kieboom and Van der Linden to an algebraic model structure. Moreover, we show that it restricts to the category of internal groupoids. We show that in this case, the algebraic weak factorisation system that consists of the algebraic trivial cofibrations and algebraic fibrations forms a model of Martin-Löf type theory. Taking $\mathcal{E} = \mathbf{Set}$ and forgetting the algebraic structure, this recovers Hofmann and Streicher’s groupoid model of Martin-Löf type theory. Finally, we are able to provide axioms on a $(2,1)$-category which ensure that it gives an algebraic model of Martin-Löf type theory. To do this, we give necessary and sufficient axioms on a 2-category $\mathcal{K}$ such that $\mathcal{K} \simeq \mathbf{Cat}(\mathcal{E})$ in which $\mathcal{E}$ is a locally cartesian closed locos with coequalisers, a result which we believe is of independent interest.

Download here

Colimits of Internal Categories, with Adrian Miranda

Published in , 2025

We show that for a list-arithmetic pretopos $\mathcal{E}$ with pullback stable coequalisers, the 2-category $\mathbf{Cat}(\mathcal{E})$ of internal categories, functors and natural transformations has finite $2$-colimits.

Download here

The Elementary Theory of the 2-Category of Small Categories, with Adrian Miranda

Published in , 2024

We give an elementary description of $2$-categories $\mathbf{Cat}\left(\mathcal{E}\right)$ of internal categories, functors and natural transformations, where $\mathcal{E}$ is a category modelling Lawvere’s elementary theory of the category of sets (ETCS). This extends Bourke’s characterisation of $2$-categories $\mathbf{Cat}\left(\mathcal{E}\right)$ where $\mathcal{E}$ has pullbacks to take account for the extra properties in ETCS, and Lawvere’s characterisation of the (one dimensional) category of small categories to take account of the two-dimensional structure. Important two-dimensional concepts which we introduce include $2$-well-pointedness, full-subobject classifiers, and the categorified axiom of choice. Along the way, we show how generating families (resp. orthogonal factorisation systems) on $\mathcal{E}$ give rise to generating families (resp. orthogonal factorisation systems) on $\mathbf{Cat}\left(\mathcal{E}\right)_{1}$, results which we believe are of independent interest.

Download here