I ask this, although I don't conduct any research in the area, or even plan to. -- There seems to be general agreement that the axioms for higher categories grow very rapidly in complexity as the order $n$ of the category grows to infinity. I am referring to the ''algebraic style'' axioms here, axiomatising a ''maximally weak'' notion of $n$-category. I assume this makes enough sense to make the following question meaningful: 



> 
> is it known (or guessed at) whether there is a Turing-machine that computes these axioms (taking the order $n$ of the category as input)? 
> 
> 
> 



Are the axioms for higher category-theory effectively computable?
**Yes.**


…at least, for Leinster’s reformulation of Batanin’s definition of globular operadic weak ω-category (and hence also for the finite-dimensional versions of this). Showing this is essentially a matter of repeatedly applying one lemma: if $\mathbf{T}$ is an essentially algebraic theory with a computable presentation, then the free $\mathbf{T}$-structure on a computably presented object is again computably presented. By “computably presented”, I mean essentially that the sets of operations and axioms are all computably enumerable.


In the Leinster/Batanin definition, one starts with strict $\omega$-categories (certainly a computably presentable theory, by the standard explicit axiomatisaion); by their observation above, their monad $T$ is computably presentable; from this, one can show that the theory of $T$-operads is computably presentable; similarly, then, the theory of $T$-operads-with-contraction; so the free $T$-operad-with-contraction $L$ is computably presentable. 


But now the operations of the theory of weak $\omega$-categories are the elements of $L$; and the axioms are given by elements of “powers” of $L$, in the monoidal structure $\otimes$ built by $T$ and pullbacks; so these sets are all computably enumerable, so we’re done.




---


From here on I’m a little beyond my comfort zone, and wouldn’t want to swear that the details hold up: someone who knows realizability toposes better than I do can probably tell better whether I’ve missed some subtlety.


A nice way to look at the above argument could be to say: develop the theory of weak $\omega$-categories in $\newcommand{\Eff}{\mathcal{E}\textit{ff}} \Eff$, the effective topos — that is, repeat all the normal definitions in the internal logic of $\Eff$, to get an internal theory $\mathbf{T}^{\Eff}\_\omega$. (Possibly $\mathbf{PER}$ or some other category of ‘computably presented sets and functions’ might work better than $\Eff$.)


Now, the global sections functor $\Gamma \colon \Eff \to \mathbf{Sets}$ is a *left exact left adjoint*, so in particular, it will commute with pullbacks and with most ‘free object’ constructions — so, with all the ingredients used in the definition of the theory of weak $\omega$-categories. So when we hit $\mathbf{T}^{\Eff}\omega$ with $\Gamma$, we just recover the original external theory $\mathbf{T}\omega$. That is, $\mathbf{T}^{\Eff}\omega$ is a computable presentation of $\mathbf{T}\_\omega$


Intuitively, we’re ‘shadowing’ every construction we do in $\mathbf{Sets}$ with a computable presentation, by performing the same constructions in parallel up in $\Eff$.


This approach should also work for most other theories of higher categorical structures — power-sets and non-finite exponentiation are the main logical constructions not preserved by $\Gamma$, and off the top of my head, only the definitions of higher categories which involve topological constructions will require these.


