Talks and presentations

The Elementary Theory of the 2-Category of Small Categories

March 12, 2024

Talk, Hicks Building, The University of Sheffield, ShEAF seminar

Abstract: Lawvere’s Elementary Theory of the Category of Sets (ETCS) provides a set theory which axiomatises the properties of function composition rather than those of a global set membership relation. It provides an important fragment of a category-theoretic foundation of mathematics but is strictly weaker than the traditional foundation of mathematics given by Zermelo Fraenkel Set Theory with the Axiom of Choice (ZFC). Precisely, ZFC is equiconsistent with ETCS augmented with the axiom schema of replacement. In this talk, I will motivate a 2-dimensional version of ETCS which axiomatises the properties of functors and functor composition; this is the elementary theory of the 2-category of small categories (ET2CSC) of the title. The advantage of this approach is that the two-dimensional setting supports a convenient way of incorporating the axiom schema of replacement, albeit in a non-elementary way. This talk is based on joint work with Adrian Miranda.

The Elementary Theory of the 2-Category of Small Categories

March 01, 2024

Talk, Alan Turing Building, The University of Manchester, Pure Postgraduate Seminar

Abstract: Lawvere’s Elementary Theory of the Category of Sets (ETCS) provides a set theory which axiomatises the properties of function composition rather than those of a global set membership relation. It provides an important fragment of a category-theoretic foundation of mathematics but is strictly weaker than the traditional foundation of mathematics given by Zermelo Fraenkel Set Theory with the Axiom of Choice (ZFC). Precisely, ZFC is equiconsistent with ETCS augmented with the axiom schema of replacement. Lawvere also called for a similar axiomatization of the two-dimensional structure of categories, functors, and natural transformations. In this talk, I will describe a characterisation of 2-categories of categories internal to a model of ETCS. The resulting theory is the elementary theory of the 2-category of small categories (ET2CSC) of the title. The main result is that the 2-categories of models of ETCS and ET2CSC are biequivalent. The advantage of this approach is that the two-dimensional setting supports a convenient way of incorporating the axiom schema of replacement, albeit in a non-elementary way. This talk is based on joint work with Adrian Miranda.

An Algebraic Folk Model Structure for Internal Categories

November 27, 2023

Talk, The Alan Turing Building, The University of Manchester, Category Theory Seminar

Quillen model categories provide an abstract framework in which to do homotopy theory. A key example is the folk model structure on $\mathbf{Cat}$, for which the notion of homotopy is that of equivalences of categories. The construction of this model structure requires the axiom of choice, meaning that groupoidal models of type theory which exploit the structure of the trivial cofibrations are not constructive. In analogy to work by Gambino, Henry, Sattler and Szumiło on the effective model structure on simplicial objects in a lextensive category, we construct a model structure on internal categories that does not require the axiom of choice; when we consider categories internal to $\mathbf{Set}$ and assume the axiom of choice, this recovers the folk model structure on $\mathbf{Cat}$. Moreover, we prove that this forms an algebraic model structure whose underlying ordinary model structure turns out to recover Everaert, Kieboom and Van de Linden’s folk model structure on internal categories equipped with the trivial topology. Restricting this construction to a model structure on internal groupoids, the extra algebraicity provides us with a constructive model of Martin-Löf Type Theory due to the type-theoretic algebraic weak factorisation systems of Gambino and Larrea. In this talk, I will introduce the construction of this algebraic model structure and some related ideas.

The Elementary Theory of the Category of Sets

November 24, 2023

Talk, Alan Turing Building, The University of Manchester, Student Logic Seminar

Abstract: Lawvere’s Elementary Theory of the Category of Sets (ETCS) characterises when a category E behaves ‘similarly’ to the category of sets. More formally, it is an axiomitization of categorical models of ZFC except for the axiom schema of replacement. As such, it provides the language for a category-theoretic foundation of mathematics. In this talk, I will define relevant category-theoretic notions and give an idea of how these relate to the ZFC axioms. I will also exemplify how one can do logic internal to a category satisfying ETCS (or more generally, in an elementary topos). No prior category theoretic knowledge is required. This talk is a precursor to some work that I have been doing with Arian on developing a 2-dimensional version of this; the elementary theory of the 2-category of small categories.

An Introduction to Homotopy Type Theory

June 09, 2023

Talk, Alan Turing Building, The University of Manchester, Pure Postgraduate seminar

It might not be too much of a stretch to say that we live in a golden age of mathematics; there is an explosion of content, theorems, and disparate research areas. With this vast wealth of content comes the need to check it all. This process is highly fallible and time consuming if done by humans, and so it is natural to ask if there is some way to get a computer to do this for us. However, our set-theoretic foundation presents many barriers to the success of this. So, we rip it up and start again!

Homotopy Type Theory Conference 2023

June 08, 2023

Talk, Alan Turing Building, The University of Manchester, Category Theory seminar

I explain some of the ideas that were presented at the Homotopy Type Theory conference 2023 at Carnegie Mellon University. In particular, I explain the construction of Riehl and Shulman’s theory of synthetic $(\infty,1)$-categories through their simplicial type theory. I also discuss synthetic algebraic geometry, other extensions of homotopy type theory, and the unifying theory of modal type theory.

Contractibility as Uniqueness

January 23, 2023

Talk, Alan Turing Building, The University of Manchester, Student Logic Seminar

A 1 hour talk presenting ideas from Emily Riehl.

The Small Object Argument

November 17, 2022

Talk, Alan Turing Building, The University of Manchester, Category Theory Seminar

A 2 hour talk presenting ideas from Richard Garner’s paper “Understanding the Small object Argument”.

The Dold-Kan Correspondence

April 28, 2022

Talk, Hicks Building, The University of Sheffield

Slides for a 15 minute talk outlining the work I completed on my fourth year MMath project on the Dold-Kan correspondence.

A Visual Introduction to Homology and Homotopy

April 28, 2022

Talk, Hicks Building, The University of Sheffield

Slides for a 20 minute talk to first and second year undergraduate students introducing the ideas behind (simplicial) homology and homotopy in a visual way.