I'm an independent researcher working on programming languages. I would love to hear that this is all already known by simpler means, or that I'm wrong. I first opened this can of worms in the Before Times and have finally come around to finish it.

A Turing category is a category-theoretic way to talk about Turing-complete computation. A typical programming language has a collection of programs $A$ represented as (say) syntax trees, along with an composition function $k : A \times A \to A$ which runs programs in sequence. Its Turing category is the free category whose Turing object is $A$ and Kleene composition is $k$. (This might make more sense through a native-type-theoretic view.)

We can imagine a category of Turing categories, but we need structure-preserving maps. We might say that a functor $F : \mathcal{C} \to \mathcal{D}$ is a compiler when it sends Turing objects $A_\mathcal{C} \mapsto A_\mathcal{D}$, so that for any object $X \in \mathcal{C}$, let $Y = F(X) \in \mathcal{D}$, and the diagram:

$\require{AMScd}$ \begin{CD} A_\mathcal{C} @> F >> A_\mathcal{D} \\ @A s_{\mathcal{C},X} AA @V r_{\mathcal{D},Y} VV \\ X @> F >> Y \end{CD}

commutes up to equivalence. ($s$ freezes values as code and $r$ evaluates code to produce values.) This diagram captures the typical notion of compiler correctness: A program compiled from $\mathcal{C}$ to $\mathcal{D}$ should have equivalent behavior on all inputs. But notice that any functor which maps Turing objects to Turing objects must make this diagram commute up to equality! Proof: Take two copies of the diagram for the universal property (from nLab, linked above), one for $\mathrm{id}_X \in \mathrm{Mor}(\mathcal{C})$ and for $\mathrm{id}_Y \in \mathrm{Mor}(\mathcal{D})$; draw $F$ connecting them, and find the above square.

A few of us noticed that we can continue this pattern upwards to compiler compilers. A compiler compiler should have equivalent behavior on all compilers, but compilers are just ordinary Turing-complete programs, so we just repeat the above proof. Indeed, Turing categories seem to be objects in an ∞-category. Specifically, let **Tomb** be the ∞-category whose:

- Objects are Turing categories with a distinguished Turing object
- 1-arrows are Cartesian closed functors which send Turing objects to Turing objects
- 2-arrows are such functors restricted to 1-arrows
- …

(We need to distinguish a Turing object per category because Turing categories are allowed to have more than one of them.) Tomb is so-called because composition of tombstone diagrams gives both the composition of 1-arrows and also both compositions of 2-arrows.

The practical rationale behind imagining Tomb is that we can think of its contents as long sequences of compilers for real-world programming languages, and we can imagine applying an n-arrow as changing the n'th language in the sequence without changing the behavior of the final program.

Turing objects are normally infinite. But curiously, the axioms allow for a Turing object which has just one element; the resulting Turing category has only one program. This gives us a terminal object in Tomb. We have products, but I'm not sure about sums, because of halting/partiality; we might have to pick products or sums. We can encode internal homs by noting that compilers can be found as programs in most Turing categories. So, I think that Tomb is Cartesian closed.

How much further can we go? **Can we find Tomb to be an ∞-topos?**