### The Internal Language of a 2-Topos

#### Posted by David Corfield

I probably ought to be much better prepared before I start this venture, but let’s give it a go anyway. A 2-topos $(\mathcal{K}, (-)^{\circ}, \tau)$ is a finitely complete cartesian closed 2-category $\mathcal{K}$ equipped with a duality involution $(-)^{\circ}$ and a classifying discrete opfibration $\tau: \Omega_{\bullet} \to \Omega$. We can worry about what these terms mean as we go along.

So we ‘just’ have to imitate Lambek and Scott’s *Introduction to higher order categorical logic*. On p. 143 they tell us that the internal language of a topos $\mathcal{T}$ has as types
the objects of $\mathcal{T}$, including the special types $1$, the terminal object, $\Omega$, the
subobject classifier, and $N$, the natural numbers object, if $\mathcal{T}$ has one.

So, the internal language of a 2-topos $\mathcal{K}$ has as types the objects of $\mathcal{K}$, including the special types $1$, the terminal object, $\Omega$, the discrete opfibration classifier, and $N$, the categorified natural numbers object, if $\mathcal{K}$ has one.

L & S then continue by saying that the internal language

has terms of type $A$ in the variables $x_i$ of type $A_i (i = 1,..., m)$ polynomial expressions $\phi(x_1,..., x_m) : 1 \to A$ in the indeterminate arrows $x_i : 1 \to A_i$ over $\mathcal{T}$.

Then give examples,

variables of type $A$ are indeterminate arrows $1 \to A$.

Presumably, then, we’d want for each type $A$ a countable number of $A$-typed variables

$x_1^A, x_2^A, x_3^A, ...$

and a countable number of doubly indexed variables, $y_{i j}^A$, indeterminate 2-morphisms between

$x_i^A$ and $x_j^A$.

Next, according to L & S, in the 1-topos case we have

$*$ is $1 \to 1$.

So we can have

$*$ is $1 \to 1$, and $*^'$ as the identity 2-morphism $id_*$.

Leaving out the natural numbers object, we now have

$\langle a, b \rangle$ is $1 \overset {\langle a, b \rangle}{\rightarrow} A \times B$.

To this we can add $\langle y_{i j}^A, y_{k l}^B \rangle$ between $\langle x_i^A, x_k^B \rangle$ and $\langle x_j^A, x_l^B \rangle$.

Now

$a = a'$ is $1 \overset{\langle a, a^' \rangle}{\rightarrow} A \times A \overset{\delta_A} {\rightarrow} \Omega$, where $\delta_A \equiv char \langle 1_A, 1_A \rangle$.

In the case of Set, that last arrow is picking out the diagonal of $A$. In the case of the 2-topos of categories, you could imagine categorifying this by a bifunctor $\delta_A$ from $A^{op} \times A$ to Set, such that $\delta_A (a, a')$ is the set of isomorphisms between $a$ and $a'$.

There’s much more work to be done, including categorfying $a \in \alpha$ as something like a fibre functor, but perhaps I’ll stop to draw breath here to make sure nobody’s going to tell me that someone has done all this perfectly in some paper on the ArXiv.

## Re: The Internal Language of a 2-Topos

I haven’t seen anyone write this down, but it’s something I’ve thought about as well. (And I’m actually currently using something related in a paper I’m writing.) While I don’t disagree with what you’ve written so far (especially with having two types of variables), I actually think that the best place to start looking is to generalize the logic of weaker sorts of 1-categories first. I don’t remember what Lambeck and Scott do, but my reference for the logic of categories nowadays is

Sketches of an Elephant, wherein he describes a correspondence between levels of structure a category can have and the sorts of logic that can be modeled therein.It’s a fact that if you define a topos to be a category with finite limits and power objects, then it is automatically cartesian closed and a Heyting category. However, for purposes of interpreting internal logic, what matters about a topos is that it is a Heyting category, which

alsohappens to be cartesian closed and have power objects. It’s not obvious to me that Weber’s definition of a 2-topos implies that a 2-topos is automatically a “Heyting 2-category”, so if what we’re interested in is an internal logic, I would be inclined to include that in the definition explicitly, until and unless someone manages to prove that it follows automatically.The reason you need this sort of structure to model logic is that what you want to do is represent every formula $\varphi(x)$, with a free variable of type $x\in X$, say, as a

subobject$\{ x\mid \varphi(x)\}$ of $X$. Then you use the operations on subobjects that exist in the category to build up $\{x\mid \varphi(x)\}$ in the same way that $\varphi$ is built up from connectives and quantifiers. So to have “and” you need intersections of subobjects, for “or” you need unions, for “there exists” you need images, and so on. And it all needs to be stable under pullback so that you can add new variables without messing up what you had already.The relevant notion of “regular 2-category” can be found in Street’s paper “A characterization of bicategories of stacks.” (See also his “Two-dimensional sheaf theory.”) Basically the idea is that you replace “mono” with “(representably) full and faithful.” Then you have to replace “regular epi” with the class of maps that are left orthogonal, in a bicategorical sense, to these, which it turns out to make sense to call “eso” since in Cat they are the essentially surjective functors. So a regular 2-category has finite limits, (eso,ff) is a factorization system, and esos are stable under pullback.

I’ve never seen anyone go on from there, but the direction to take is fairly clear. You have lattices Sub(X) of ffs into X, and you can then add structure up to first-order logic in the same way, by asking that these have pullback-stable unions and dual images. This will allow you to represent the truth of any formula by a ff in the same way, although you have to think about atomic formulas. In the 1-categorical case, atomic formulas such as $x=y$ are represented by equalizers. We probably don’t want to use equalizers in a 2-category, since they ask objects to be equal. Iso-inserters ($\approx$ pseudo-equalizers) are not ff, but equifiers (setting two 2-cells equal) are ff. So the language is naturally restricted to talking about equality of arrows, but not equality of objects.

After we have all that, then I would think about adding type constructors for the cartesian closed structure, duality involution, and the discrete opfibration classifier. The first two don’t seem too hard, but I haven’t thought at all about the third (which, of course, is probably where the real meat is).