Nathanael Arkor

About me

Hi – I am a postdoctoral researcher in the Logic and Semantics Group at Tallinn University of Technology, working under Tarmo Uustalu. My present research interests fall broadly within pure category theory and type theory, and include more specifically: formal category theory, relative monads, double category theory, 2-category theory, abstract syntax & algebraic type theory, and categorical algebra & logic.

Previously, I was a postdoctoral researcher in the Algebra Group at Masaryk University, working under John Bourke. I completed my PhD in the Programming, Logic, and Semantics Group at the University of Cambridge with Marcelo Fiore.

I am happy to supervise bachelor's and master's projects in any of the areas mentioned above – feel free to email me to discuss potential projects.

Preprints

1. Idempotence for relative monads 2025 Nathanael Arkor & Andrew Slattery

   We study the concept of idempotence for relative monads, which exhibits several subtleties not present for non-relative monads. In particular, there is a bifurcation of notions of idempotence in the relative setting, which are indistinguishable for idempotent monads. As a special case, we obtain several characterisations of idempotence for monads in extension form.

   arXiv
2. Magmal characterisations of cocartesian categories 2025 Nathanael Arkor

   We present a survey of characterisations of cocartesian categories in terms of monoidal categories – and, more generally, magmal categories – satisfying additional properties. In particular, we show that the following are equivalent for a unital magmal category $(\mathcal M, \otimes)$, sharpening several classical characterisations.

   • $(\mathcal M, \otimes)$ is cocartesian monoidal.
   • Every object of $\mathcal M$ admits the structure of a unital magma with respect to $\otimes$, such that every morphism is a homomorphism, and a single compatibility condition holds between the magma structures and $\otimes$.
   • The tensor product functor ${\otimes} \colon \mathcal M \times \mathcal M \to \mathcal M$ admits a right adjoint.
   arXiv
3. Exponentiable virtual double categories and presheaves for double categories 2025 Nathanael Arkor

   Given a pair of pseudo double categories $\mathbb A$ and $\mathbb B$, the lax functors from $\mathbb A$ to $\mathbb B$, along with their transformations, modules, and multimodulations, assemble into a virtual double category $\mathbf{\mathbb Lax}(\mathbb A, \mathbb B)$. We exhibit a universal property of this construction by observing that it arises naturally from the consideration of exponentiability for virtual double categories. In particular, we show that every pseudo double category is exponentiable as a virtual double category, whereby the virtual double category $\mathbf{\mathbb Lax}(\mathbb A, \mathbb B)$ of lax functors arises as the virtual double category $\mathbf{\mathbb Mod}(\mathbb B^{\mathbb A})$ of monads and modules in the exponential $\mathbb B^{\mathbb A}$. We explore some consequences of this characterisation, demonstrating that it facilitates simple proofs of statements that heretofore required unwieldy computations. For instance, we deduce that the 2-category of pseudo double categories and lax functors is enriched in the 2-category of normal virtual double categories, and demonstrate that several aspects of the Yoneda theory of pseudo double categories – such as the correspondence between presheaves and discrete fibrations – are substantially simplified by this perspective.

   arXiv
4. Bicategories of algebras for relative pseudomonads 2025 Nathanael Arkor, Andrew Slattery & Philip Saville

   We introduce pseudoalgebras for relative pseudomonads and develop their theory. For each relative pseudomonad $T$, we construct a free–forgetful relative pseudoadjunction that exhibits the bicategory of $T$-pseudoalgebras as terminal among resolutions of $T$. The Kleisli bicategory for $T$ thus embeds into the bicategory of pseudoalgebras as the sub-bicategory of free pseudoalgebras. We consequently obtain a coherence theorem that implies, for instance, that the bicategory of distributors is biequivalent to the 2-category of presheaf categories. In doing so, we extend several aspects of the theory of pseudomonads to relative pseudomonads, including doctrinal adjunction, transport of structure, and lax-idempotence. As an application of our general theory, we prove that, for each class of colimits $\Phi$, there is a correspondence between monads relative to free $\Phi$-cocompletions, and $\Phi$-cocontinuous monads on free $\Phi$-cocompletions.

   arXiv
5. Enhanced 2-categorical structures, two-dimensional limit sketches and the symmetry of internalisation 2025 Nathanael Arkor, John Bourke & Joanna Ko

   Many structures of interest in two-dimensional category theory have aspects that are inherently strict. This strictness is not a limitation, but rather plays a fundamental role in the theory of such structures. For instance, a monoidal fibration is – crucially – a strict monoidal functor, rather than a pseudo or lax monoidal functor. Other examples include monoidal double categories, double fibrations, and intercategories. We provide an explanation for this phenomenon from the perspective of enhanced 2-categories, which are 2-categories having a distinguished subclass of 1-cells representing the strict morphisms. As part of our development, we introduce enhanced 2-categorical limit sketches and explain how this setting addresses shortcomings in the theory of 2-categorical limit sketches. In particular, we establish the symmetry of internalisation for such structures, entailing, for instance, that a monoidal double category is equivalently a pseudomonoid in an enhanced 2-category of double categories, or a pseudocategory in an enhanced 2-category of monoidal categories.

   arXiv
6. Higher-order algebraic theories 2020 Nathanael Arkor & Dylan McDermott See Chapter 4 of my thesis for an revised account.

   Algebraic theories give a presentation-free categorical formulation of universal algebraic structure: objects equipped with first-order operators, subject to equational laws. Similarly, higher-order algebraic theories describe objects equipped with higher-order, variable-binding operators, such as logical quantifiers or $\lambda$-abstraction. While higher-order structures abound in mathematics and computer science, there exists no systematic treatment in the spirit of that for first-order structure. This has led to a proliferation of variations of higher-order theory, and consequently a lacklustre general understanding. We take the first steps to rectify this, defining a notion of multisorted higher-order algebraic theory and carrying out a development analogous to that of the first-order setting. In addition to unifying various previous notions, we (1) establish a correspondence between higher-order algebraic theories and a class of (relative) monads, whose algebras describe the closed-term structure of the corresponding theories; (2) prove that the categories of higher-order algebraic theories, and of the term algebras for a higher-order algebraic theory, are locally strongly finitely presentable; (3) give a new explanation for the apparent asymmetry between models of algebraic theories in the category of sets, and models in arbitrary cartesian categories.

   PDF

Papers

1. The nerve theorem for relative monads 2025 Nathanael Arkor & Dylan McDermott Theory and Applications of Categories

   A fundamental result in the theory of monads is the characterisation of the category of algebras for a monad in terms of a pullback of the category of presheaves on the category of free algebras: intuitively, this expresses that every algebra is a colimit of free algebras. We establish an analogous result for enriched relative monads with dense roots, and explain how it generalises the nerve theorems for monads with arities and nervous monads. As an application, we derive sufficient conditions for the existence of algebraic colimits of relative monads. More generally, we establish such a characterisation of the category of algebras in the context of an exact virtual equipment. In doing so, we are led to study the relationship between a $j$-relative monad $T$ and its associated loose-monad $E(j, T)$, and consequently show that the opalgebra object and the algebra object for $T$ may be constructed from certain double categorical limits and colimits associated to $E(j, T)$.

   DOI arXiv
2. Relative monadicity 2025 Nathanael Arkor & Dylan McDermott Journal of Algebra

   We establish a relative monadicity theorem for relative monads with dense roots in a virtual equipment, specialising to a relative monadicity theorem for enriched relative monads. In particular, for a dense $\mathbb V$-functor $j \colon A \to E$, a $\mathbb V$-functor $r \colon D \to E$ is $j$-monadic if and only if $r$ admits a left $j$-relative adjoint and creates $j$-absolute colimits. This provides a refinement of the classical monadicity theorem – characterising those categories whose objects are given by those of $E$ equipped with algebraic structure – in which the arities of the algebraic operations are valued in $A$. In particular, when $j = 1$, we recover a formal monadicity theorem. Furthermore, we examine the interaction between the pasting law for relative adjunctions and relative monadicity. As a consequence, we derive necessary and sufficient conditions for the ($j$-relative) monadicity of the composite of a $\mathbb V$-functor with a ($j$-relatively) monadic $\mathbb V$-functor.

   DOI arXiv
3. Adjoint functor theorems for lax-idempotent pseudomonads 2024 Nathanael Arkor, Ivan Di Liberti & Fosco Loregian Theory and Applications of Categories

   For each pair of lax-idempotent pseudomonads $R$ and $I$, for which $I$ is locally fully faithful and $R$ distributes over $I$, we establish an adjoint functor theorem, relating $R$-cocontinuity to adjointness relative to $I$. This provides a new perspective on the nature of adjoint functor theorems, which may be seen as methods to decompose adjointness into cocontinuity and relative adjointness. As special cases, we recover variants of the adjoint functor theorem of Freyd, the multiadjoint functor theorem of Diers, and the pluriadjoint functor theorem of Solian–Viswanathan, as well as the adjoint functor theorems for locally presentable categories. More generally, we recover enriched $\Phi$-adjoint functor theorems for weakly sound classes of weight $\Phi$.

   DOI arXiv
4. The formal theory of relative monads 2024 Nathanael Arkor & Dylan McDermott Journal of Pure and Applied Algebra

   We develop the theory of relative monads and relative adjunctions in a virtual equipment, extending the theory of monads and adjunctions in a 2-category. The theory of relative comonads and relative coadjunctions follows by duality. While some aspects of the theory behave analogously to the non-relative setting, others require new insights. In particular, the universal properties that define the algebra object and the opalgebra object for a monad in a virtual equipment are stronger than the classical notions of algebra object and opalgebra object for a monad in a 2-category. Inter alia, we prove a number of representation theorems for relative monads, establishing the unity of several concepts in the literature, including the devices of Walters, the $j$-monads of Diers, and the relative monads of Altenkirch, Chapman, and Uustalu. A motivating setting is the virtual equipment $\mathbb{V}\text{-}\mathbf{\mathbb{C}at}$ of categories enriched in a monoidal category $\mathbb{V}$, though many of our results are new even for $\mathbb{V} = \mathbf{Set}$.

   DOI arXiv
5. Abstract clones for abstract syntax 2021 Nathanael Arkor & Dylan McDermott FSCD 2021

   We give a formal treatment of simple type theories, such as the simply-typed $\lambda$-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed $\lambda$-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as $\beta$- and $\eta$-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax.

   DOI arXiv
6. Algebraic models of simple type theories: a polynomial approach 2020 Nathanael Arkor & Marcelo Fiore LICS 2020

   We develop algebraic models of simple type theories, laying out a framework that extends universal algebra to incorporate both algebraic sorting and variable binding. Examples of simple type theories include the unityped and simply-typed $\lambda$-calculi, the computational $\lambda$-calculus, and predicate logic.

   Simple type theories are given models in presheaf categories, with structure specified by algebras of polynomial endofunctors that correspond to natural deduction rules. Initial models, which we construct, abstractly describe the syntax of simple type theories. Taking substitution structure into consideration, we further provide sound and complete semantics in structured cartesian multicategories. This development generalises Lambek's correspondence between the simply-typed $\lambda$-calculus and cartesian-closed categories, to arbitrary simple type theories.

   DOI arXiv

Thesis

1. Monadic and Higher-Order Structure 2022 Nathanael Arkor

   Simple type theories, ubiquitous in the study of programming language theory, augment algebraic theories with higher-order, variable-binding structure. This motivates the definition of higher-order algebraic theories to capture this structure, permitting the study of simple type theories in a categorical setting analogous to that of algebraic theories. The theory of higher-order algebraic theories is in one sense much richer than that of algebraic theories, as we may stratify the former according to their order: for instance, the first-order algebraic theories are precisely the classical algebraic theories, the second-order algebraic theories permit operators to abstract over operators, the third-order algebraic theories permit operators to abstract over operators that themselves abstract over operators, and so on. We study the structure of the category of $(n + 1)$^th-order algebraic theories, demonstrating that it may be viewed as a construction on the category of $n$^th-order algebraic theories, facilitating an inductive construction of the category of higher-order algebraic theories. In turn, this description leads naturally to a monad–theory correspondence for higher-order algebraic theories, subsuming the classical monad–theory correspondence, and providing a new, monadic understanding of higher-order structure.

   In proving the monad–theory correspondence for higher-order algebraic theories, we are led to reconsider the traditional perspective on the classical monad–theory correspondence. In doing so, we reveal a new understanding of the relationship between algebraic theories and monads that clarifies the nature of the correspondence. The crucial insight follows from the consideration of relative monads, which are shown to act as an intermediary in the correspondence. To support our proposal that this be viewed as the correct perspective of the monad–theory correspondence, we show how the same proof may be carried out in a formal 2-categorical setting. The classical monad–theory correspondence, as well as those in the literature for enriched and internal categories, then follow as corollaries of a general theory.

   PDF DOI

Software

1. quiver: a modern commutative diagram editor for the web.
2. tangle: a modern string diagram editor for the web.

Talks

1. Convolution via exponentiation ItaCa Fest 2025
   Recording Slides
   This talk was based on the material in this paper.
2. The three-dimensional structures formed by monoidal categories, bicategories, double categories, etc. Category Theory 2025
   Slides
3. Virtual double categories: Past, present, and future Séminaire Itinérant de Catégories
   Slides
4. Relative monadicity PSSL 110
   Slides
   This talk was based on the material in this paper.
5. A (virtual) double category theorist's perspective on polynomials The Topos Institute Colloquium
   Recording Slides
6. A recipe for enriched categories TSEM Seminar
   Slides
7. The pullback theorem for relative monads Category Theory 2024
   Slides
   This talk was based on the material in this paper.
8. The pullback theorem for relative monads TSEM Seminar
   Recording Slides
   This talk was based on the material in this paper.
9. Relative monads and distributors #LoVe Seminar
   Slides
   This talk was based on the material in this paper.
10. The nature of adjoint functor theorems PSSL 108
    Slides
    This talk was based on the material in this paper.
11. The formal theory of relative monads Category Theory 2023
    Recording Slides
    This talk was based on the material in this paper.
12. The theory of relative (co)monads Comonads Seminar
    Slides
    This talk was based on the material in this paper.
13. The formal theory of relative monads PSSL 107
    Slides
    This talk was based on the material in this paper.
14. A 2-dimensional perspective on polymorphism ICE-TCS Seminar
    Slides
15. Relative monads and their many guises Octoberfest 2022
    Slides
    This talk was based on the material in this paper.
16. What is a proof? DIMEA and FORMELA Seminar
    Slides
17. The (relative) monad–theory correspondence Masaryk University Algebra Seminar
    Recording Slides
    This talk was based on the material in my thesis.
18. The (relative) monad–theory correspondence TallCat
    Slides
    This talk was based on the material in my thesis.
19. The formal theory of theories CT 20→21
    Recording Slides
    This talk was based on the material in my thesis.
20. Abstract clones for abstract syntax FSCD 2021
    Recording Slides
    This talk was based on the material in this paper.
21. Higher-order algebraic theories and relative monads Categories and Companions Symposium 2021
    Recording Slides
    This talk was based on the material in my thesis.
22. Higher-order algebraic theories and relative monads Masaryk University Algebra Seminar
    Recording Slides
    This talk was based on the material in my thesis.
23. Algebraic models of simple type theories: a polynomial approach LICS 2020
    Recording Slides
    This talk was based on the material in this paper.
24. Algebraic simple type theory: a polynomial approach Category Theory 2019
    Slides
    This talk was based on the material in this paper.