(Link)

Author: Christopher Dorn (University of Oxford)

Reference: Dorn, C. Associative n-categories. PhD thesis, University of Oxford, 2018.

Why this paper? Cited by Automating Boundary Filling in Cubical Agda and homotopy.io: a proof assistant for finitely-presented globular n-categories

I have looked at PhD dissertations for this blog before, but never one this gargantuan; at 503 pages it weighs in at 3-4 times longer than the average thesis. The author does not quite apologise for the length, but at least acknowledges it, saying “[the] length of this thesis should by no means deter the potential reader, as it is mainly a consequence of the presence of many pictures, examples and often very detailed (albeit elementary) proofs and computations”. While I wasn’t ‘deterred’ as such, I do of course have to fit my blog reading in around my other work and life commitments and therefore have only skimmed most sections.

We’ve seen 2-categories on this blog before, where we have objects, morphisms, and morphisms between morphisms. This thesis looks at n-categories for an arbitrary n, so with n dimensions of morphisms on top of the bottom layer of objects. This generalisation is by no means simple, because there is a lot of room for different definitions depending on how ‘weak’ or ‘strict’ one wants to be. The weak approach only defines various notions up to isomorphism, which gives rise to many ‘coherence conditions’ (equalities of morphisms) which are hard to check, or even define, whereas the strict approach defines notions as specific objects, but rules out many examples where structure is not so crisply definable. This thesis threads this needle by analogy with Gray categories, a *semistrict* definition of 3-category in which some constructions are weak and others strict. Crucially, any weak 3-category is equivalent to a Gray category, so Gray categories can be seen to hit a sweet spot of being as strict as possible (making definitions and computations simpler) while being weak enough not to rule out any examples. The developments of this thesis aim to hit a similar sweet spot for a general n; unfortunately that “the theory of associative n-categories is equivalent to a theory [of] weak n-categories” remains only a conjecture. However, the associative n-categories of the thesis do correspond to Gray categories at dimension 3 (technically, unbiased Gray categories, but that is a minor definitional issue). At dimensions 0, 1, and 2, they correspond to sets, categories, and strict 2-categories, so it is at dimension 4+ that this work should really pay off.

I will not spend time in this short post discussing the actual definitions of associative n-categories, which are quite involved, but instead round off by commenting that one of the new papers that led me to this slightly older work was that of Corbyn et al., who have designed a theorem prover called homotopy.io whose intended models are (finitely-presented) associative n-categories. Users can interact with this prover by means of graphical string diagrams. I have no idea yet how to read these diagrams, which are used in various parts of the thesis, but they are pretty – a topic for another day perhaps. I do know there is a textbook out there now for those who want to follow this angle up.