Publications
Journal and conference papers
Hom \(\omega\)-categories of a computad are free
Journal of the London Mathematical Society(2025)Abstract
We provide a new description of the hom functor on weak \(\omega\)‐categories, and show that it admits a left adjoint that we call the suspension functor. We then show that the hom functor preserves the property of being free on a computad, in contrast to the hom functor for strict \(\omega\)‐categories. Using the same technique, we define the opposite of an \(\omega\)‐category with respect to a set of dimensions, and show that this construction also preserves the property of being free on a computad. Finally, we show that the constructions of opposites and homs commute.
Naturality for higher-dimensional path types
Proceedings of the 40th Annual ACM/IEEE Symposium on Logic in Computer Science(2025)Abstract
We define a naturality construction for the operations of weak \(\omega\)-categories, as a meta-operation in a dependent type theory. Our construction has a geometrical motivation as a local tensor product with a directed interval, and behaves logically as a globular analogue of Reynolds parametricity. Our construction operates as a ``power tool'' to support construction of terms with geometrical structure, and we use it to define composition operations for cylinders and cones in omega-categories. The machinery can generate terms of high complexity, and we have implemented our construction in a proof assistant, which verifies that the generated terms have the correct type. All our results can be exported to homotopy type theory, allowing the explicit computation of complex path type inhabitants.
CaTT contexts are finite computads
Electronic Notes in Theoretical Informatics and Computer Science(2024)Abstract
Two novel descriptions of weak \(\omega\)-categories have been recently proposed, using type-theoretic ideas. The first one is the dependent type theory CaTT whose models are \(\omega\)-categories. The second is a recursive description of a category of computads together with an adjunction to globular sets, such that the algebras for the induced monad are again \(\omega\)-categories. We compare the two descriptions by showing that there exits a fully faithful morphism of categories with families from the syntactic category of CaTT to the opposite of the category of computads, which gives an equivalence on the subcategory of finite computads. We derive a more direct connection between the category of models of CaTT and the category of algebras for the monad on globular sets, induced by the adjunction with computads.
Computads for generalised signatures
Journal of Pure and Applied Algebra(2024)Abstract
We introduce a notion of signature whose sorts form a direct category, and study computads for such signatures. Algebras for such a signature are presheaves with an interpretation of every function symbol of the signature, and we describe how computads give rise to signatures. Generalising work of Batanin, we show that computads with certain generator-preserving morphisms form a presheaf category, and describe a forgetful functor from algebras to computads. Algebras free on a computad turn out to be the cofibrant objects for certain cofibrantly generated factorisation system, and the adjunction above induces the universal cofibrant replacement, in the sense of Garner, for this factorisation system. Finally, we conclude by explaining how many-sorted structures, weak \(\omega\)-categories, and algebraic semi-simplicial Kan complexes are algebras of such signatures, and we propose a notion of weak multiple category.
Computads for weak \(\omega\)-categories as an inductive type
Advances in Mathematics(2024)Abstract
We give a new description of computads for weak globular ω-categories by giving an explicit inductive definition of the free words. This yields a new understanding of computads, and allows a new definition of \(\omega\)-category that avoids the technology of globular operads. Our framework permits direct proofs of important results via structural induction, and we use this to give new proofs that every ω-category is equivalent to a free one, and that the category of computads with variable-to-variable maps is a presheaf topos, giving a direct description of the index category. We prove that our resulting definition of \(\omega\)-category agrees with that of Batanin and Leinster and that the induced notion of cofibrant replacement for \(\omega\)-categories coincides with that of Garner.
Preprints
Beyond Eckmann-Hilton: Commutativity in Higher Categories
Abstract
We show that in a weak globular \(\omega\)-category, all composition operations are equivalent and commutative for cells with sufficiently degenerate boundary, which can be considered a higher-dimensional generalisation of the Eckmann-Hilton argument. Our results are formulated constructively in a type-theoretic presentation of \(\omega\)-categories. The heart of our construction is a family of padding and repadding techniques, which gives an equivalence relation between cells which are not necessarily parallel. Our work has been implemented, allowing us to explicitly compute suitable witnesses, which grow rapidly in complexity as the dimension increases. These witnesses can be exported as inhabitants of identity types in Homotopy Type Theory, and hence are of relevance in synthetic homotopy theory.
Invertible cells in \(\omega\)-categories
Abstract
We study coinductive invertibility of cells in weak \(\omega\)-categories. We use the inductive presentation of weak \(\omega\)-categories via an adjunction with the category of computads, and show that invertible cells are closed under all operations of $\omega$-categories. Moreover, we give a simple criterion for invertibility in computads, together with an algorithm computing the data witnessing the invertibility, including the inverse, and the cancellation data.
Computing minimal generating systems for some special toric ideals
Abstract
Let \(X_P\) be the projective toric surface associated to a lattice polytope \(P\). If the number of lattice points lying on the boundary of \(P\) is at least \(4\), it is known that \(X_P\) is embeddable into a suitable projective space as zero set of finitely many quadrics. In this case, the determination of a minimal generating system of the toric ideal defining \(X_P\) is reduced to a simple Gaussian elimination.
Thesis
An inductive approach to \(\omega\)-categories and their computads
University of Cambridge(2024)Abstract
Given an algebraic structure, a basic question is to determine the data from which it can be freely generated. In the case of \(\omega\)-categories, this data can be either globular sets, or the computads of Street and Batanin. In this thesis, we give an inductive description to computads and the free weak \(\omega\)-categories they generate. We then generalise this approach to other higher structures.
The first part of the thesis is concerned with strict \(\omega\)-categories and globular pasting diagrams. We give an inductive description of the set of Batanin trees, parametrising globular pasting diagrams, as well as a recursive definition of globular pasting diagrams using the wedge sum and the suspension of globular sets. We then give a new direct proof that globular pasting diagrams familially represent the free strict \(\omega\)-category monad on globular sets, giving in particular a structurally recursive description of the monad multiplication.
The second part of the thesis introduces weak \(\omega\)-categories and their computads. First, computads are defined mutually inductively with the underlying globular set of the free \(\omega\)-category they generate. This globular set is defined inductively via a pair of constructors, and not as a pushout in an already-known category of \(\omega\)-categories. This yields a new understanding of computads, and allows a new definition of \(\omega\)-categories that avoids the technology of globular operads. This new description permits direct proofs of important results via structural induction, and we use this to give new proofs that every \(\omega\)-category is equivalent to a free one, and that the category of computads with generator-preserving maps is a presheaf topos. We also use this description to construct the hom and suspension of an \(\omega\)-category, and to prove that the homs of a computad are computads. We then show that our definition of \(\omega\)-category agrees with that of Batanin and Leinster.
In the final part of the thesis, we generalise our inductive approach to other higher structures. We introduce a notion of signature whose sorts form a direct category, and study computads for such signatures. Algebras for such a signature are presheaves with an interpretation of every function symbol of the signature, and we describe how computads give rise to algebras. Motivated by work of Batanin, we show that computads with generator-preserving morphisms form a presheaf category, and describe a forgetful functor from algebras to computads. Algebras free on a computad turn out to be the cofibrant objects for a certain cofibrantly generated weak factorisation system, and the adjunction above induces the universal cofibrant replacement in the sense of Garner, for this weak factorisation system. Finally, we conclude by explaining how many-sorted structures and algebraic semi-simplicial Kan complexes are algebras of such signatures, and by proposing a notion of weak multiple category.