The Internal Language of a 2-Topos

November 6, 2008

Posted by David Corfield

$MathML-enabled post (click for more details).$

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.

$MathML-enabled post (click for more details).$

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.

Posted at November 6, 2008 1:27 PM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1843

34 Comments & 0 Trackbacks

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

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.

In a regular category, where (regular epi, mono) is a factorization system and regular epis are stable under pullback, you can model regular logic, which has “true”, “and”, and “there exists” but nothing else.
In a coherent category, which is regular and moreover its subobject lattices Sub(X) have pullback-stable unions, you can model coherent logic, which has “true”, “and”, “there exists”, “or”, and “false”.
In a Heyting category, where the pullback functors $f^*:\mathrm{Sub}(X)\to \mathrm{Sub}(Y)$ have right adjoints (left adjoints are given by images, in any regular category) you can model full (finitary) first-order logic.
In a cartesian closed category, you can model $\lambda$ -calculus (that is, you have function types).
In a topos, you can model “higher-order logic” meaning that you have power types.

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 also happens 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).

Posted by: Mike Shulman on November 6, 2008 3:58 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

Mike wrote:

I actually think that the best place to start looking is to generalize the logic of weaker sorts of 1-categories first.

In fact that’s what Mike Stay is doing his thesis on. He’s a grad student of mine who is also working at Google. Paul-André Melliès is also involved in this project.

Right now we’re focusing on cartesian closed 2-categories and the ‘categorified $\lambda$ -calculus’, and more generally symmetric monoidal closed 2-categories and the ‘categorified linear $\lambda$ -calculus’… which gets us into the realm of categorified quantum logic. The idea is to categorify all aspects of the Rosetta stone.

It’s going slowly so far but it should be lots of fun. As you note, there are many other flavors of category, and corresponding flavors of logic, that deserve to be categorified. So, there’s no shortage of work to do.

Ultimately of course we should formalize the whole idea of a ‘flavor of category’ (perhaps using a pseudomonad on $Cat$ ), and then build a machine that can turn any such thing into a corresponding ‘flavor of $n$ -category’, and then another machine that coughs up the corresponding ‘flavor of logic’. But that’s a project for a highly energetic youngster — the Urs Schreiber of logic. I’ll rest content if I can convince lots of people something like this would be a good idea.

Posted by: John Baez on November 6, 2008 10:01 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

If you’re looking at cartesian-closed 2-categories, then I presume you know about the work of Neil Ghani and Robert Seely? I think one of the first papers was http://www.math.mcgill.ca/~rags/WkAdj/LICS.pdf and I don’t really know what happened after that.

Posted by: Andrej Bauer on November 7, 2008 8:39 AM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

Thanks! Yes, we know various references on this subject.

Posted by: John Baez on November 7, 2008 11:02 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

It sounds like we have a parallel with the categorified geometry case. Although Euclidean geometry arrived first on the scene, it turns out to be easier to categorify stripped down geometries first. In fact we haven’t even managed to find an equivalent for the inner product yet.

So now, before anyone had ever heard of regular or coherent logic, there was standard classical predicate logic. So maybe it would be easier to start categorifying the former.

All the same, I like Michael’s idea of coming in at the Heyting category level. Google hasn’t heard of “Heyting 2-category” (though if we wait a day or two it should find this thread). Is there a proposed definition yet?

How are you imagining “lattices Sub( $X$ ) of ffs into $X$ ”? In the case of the 2-category of categories, you’d think of categorified predicates as presheaves.

Posted by: David Corfield on November 7, 2008 9:09 AM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

Perhaps the question to start with is: in a fairly arbitrary 2-categorical setting, what is the analogue of the category of `subobjects’ of a given X. The subobject ‘lattice’ is that modulo the obvious equivalence.

As you point out, David, this IS the same basic problem as in generalising the Galois theoretic interpretation of covering spaces to the next (categorified) level. In trying to answer that I have never been sure if it was the subobjects or quotients (i.e. G-sets in the classical case) that needed generalising. I know this has been thrown around a lot `from table to table’ in this café, but has a concensus as to which is better emerged at all?

Posted by: Tim Porter on November 7, 2008 4:39 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

How are you imagining “lattices Sub( $X$ ) of ffs into $X$ ”? In the case of the 2-category of categories, you’d think of categorified predicates as presheaves.

So, actually, I wouldn’t. I think my argument is that in the case of a 1-topos, there is a fortuitous coincidence between (a) the subobjects which you use to represent the internal logic and (b) the things that your classifier classifies.

In general, I think that in an $n$ -topos, being an $n$ -category that acts like a universe of $(n-1)$ -categories, you’ll have a classifier that classifies fibrations whose fibers are $(n-2)$ -categories. Thus in a 1-topos, being a universe of sets (that is, 0-categories) you have a classifier that classifies subobjects (that is, fibrations whose fibers are (-1)-categories (truth values)). And in a 2-topos, being a universe of 1-categories, you have a classifier that classifies discrete fibrations (whose fibers are sets).

On the other hand, it seems to me that when doing logic, I always want my statements to have truth values that are, well, truth values. I’m well aware that people like to think of sets and discrete fibrations as “generalized truth values,” and I’m not denying there are useful insights to be gained in that way (such as the behavior of classifiers I noted above). However, I observe empirically that whether I am doing set theory, category theory, 2-category theory, or $\omega$ -category theory, when I ask a question like “does this functor have an adjoint?” or “are all definitions of $\omega$ -categories equivalent?” I still expect the answer to be a truth value, not a set or a category or an $\omega$ -category. I wouldn’t really know what to do with it if someone answered one of those questions with, say, a 12-element set.

Perhaps I’m just missing or misunderstanding something. But if not, then that means that even in an $n$ -topos, predicates should still have truth values, and therefore be represented by subobjects, not presheaves.

Google hasn’t heard of “Heyting 2-category” (though if we wait a day or two it should find this thread). Is there a proposed definition yet?

Here is my proposed definition, which I alluded to in my previous post.

A morphism (i.e. a 1-cell) $f:X\to Y$ in a 2-category $C$ is ff if $C(Z,X)\to C(Z,Y)$ is full and faithful for all $Z$ . It is eso if it is left orthogonal to all ffs, in the bicategorical sense. A 2-category $C$ is regular if it is finitely complete (in the pseudo/bicategorical sense), esos are preserved by (pseudo)pullback, and every morphism factors (up to iso) as an eso followed by an ff. Thus far is taken directly from Street.

Now for every $X\in C$ , the full sub-2-category of $C/X$ (the bicategorical slice) whose objects are ff is equivalent to a poset (its hom-categories are all either empty or contractible groupoids). Call that poset Sub(X). Since ffs are preserved by pullback, for any $f:X\to Y$ we have a functor $f^*:\mathrm{Sub}(Y)\to \mathrm{Sub}(X)$ . In a regular 2-category, the eso-ff factorization provides a left adjoint to $f^*$ , which we call $\exists_f$ .

A coherent 2-category is a regular one in which the posets Sub(X) all have finite joins which are preserved by the functors $f^*$ . A Heyting 2-category is a coherent one in which the functors $f^*$ all have right adjoints, called $\forall_f$ . As in the 1-categorical case this implies that the posets Sub(X) are all Heyting algebras, with structure preserved by the functors $f^*$ .

Posted by: Mike Shulman on November 7, 2008 9:14 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

Mike,

I’m not sure about truth values.

In the standard everyday mathematics, one has a question : does equation 1 have a solution? Initially the answer may seem to be Yes or No, but the `real’ question is not being asked. I think it is : describe the solution `object’ of equation 1. It may be empty, it may have a single element, it may naturally be a category rather than a set, and so on.

I can give a simple example. I was looking at a comma category arising in the study of the ordinal sum which I write as $\oplus$ . The category in question consisted of all pairs $([p],[q])$ of ordinals together with maps $[p]\oplus[q]\to [n]$ , where $n$ was fixed in advance. The combinatorial structure of that category was crucial. If I had asked: `is that category empty?’, the truth value would tell me very little. Does that category have a terminal object? The answer is no, but that is not the real answer as the question was not really the right one!!

Perhaps the point is that `Does that category have a terminal object?’ is not a categorified question as `Does this functor have an adjoint? is not. `What is the structure of the category of adjoints to that functor? is. Your question :“are all definitions of ω-categories equivalent?” is not categorified, but `what is the structure of the collection of equivalences between the various definitions of $\omega$ -category?’ is getting near to be. The usual question is a question about that object. Something like `is it connected’?

In other words $n$ -categorified questions could have $n-1$ -categories as their truth values. The usual truth values are then observations about those categorified truth values.

I think your comment goes a long way towards saying what a categorified question may formally (and actually) be, but I think that the solution is already in our ordinary mathematical usage.

Posted by: Tim Porter on November 8, 2008 8:03 AM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

Tim,

You make some very good points. I find the idea of categorified questions very intriguing, and I would definitely like to see a precise development of such a line of thought. In some ways it does definitely seem to correspond to what we do in mathematics.

I am having a hard time imagining a world of mathematics in which we could only ask and answer categorified questions. As you say, “the usual truth values are then observations about those categorified truth values.” So it seems that once we ask a categorified question and get a categorified truth value as an answer, we’ll still want to then ask an ordinary question about that truth value and get an ordinary truth value as an answer. Or maybe we’d need to go down the ladder one step at a time, from $n$ -truth values to $(n-1)$ -truth values, and so on. Regardless, it doesn’t seem to me that we can banish the usual uncategorified truth values altogether.

But perhaps that should be modeled by saying that just as the lattice of subobjects of any object of a 1-topos is a Heyting algebra (a 0-topos), so should the category of discrete fibrations over any object of a 2-topos be itself a 1-topos, and the pullback functors should be logical? That would definitely be an interesting sort of structure. The “logic” of such a beast would then probably be a sort of dependent-types thing.

Here’s another thing that makes me worry about discrete-fibrations-as-truth-values, though. Consider the question “is a set $X$ a group?”, which is clearly in need of categorification. It seems that the answer to the categorified version of this question should be the collection of group structures on $X$ , which is in fact (equivalent to) a set. Now if “is a group” were an ordinary predicate on a set $A$ , we would have an extension $\{X\in A \mid X \;\text{ is a group}\}$ , equipped with a monic to $A$ . So by analogy, it seems that in categorified logic, we should have a discrete fibration over Set whose fiber over $X$ is the set of group structures on $X$ . However, we do not; the forgetful functor from groups to sets has discrete fibers, but it is not a fibration.

Perhaps I’m still just confused somewhere, though, and you can straighten me out. As I said, I do like the idea of “categorified questions.”

Posted by: Mike Shulman on November 8, 2008 7:25 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

I was wondering about the group and forgetful functor example. I probably should know but why does it fail to be a fibration?

Having, for $X$ in a 2-topos, $Sub(X)$ as a 1-topos squares nicely with $Sub(X)$ as some category of presheaves in the 2-topos of categories.

It looks like what we’re discussing here is a generalisation of the question of what is a sub-2-group. The latter spreads over several posts, including one intense bout starting here.

Next comment Mathieu Dupont writes:

I am convinced that the good notions of subobjects in a groupoid enriched category (and perhaps more generally in a 2-category) are faithful and fully faithful arrows, which I would call respectively “subobjects” and “full subobjects”.

Posted by: David Corfield on November 10, 2008 9:23 AM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

I was wondering about the group and forgetful functor example. I probably should know but why does it fail to be a fibration?

Well, if it were a fibration, then since its fibers are discrete, it would be a discrete fibration. That would mean that for any group $G$ , any set $X$ , and any set function $f:X\to G$ , there would exist a unique group structure on $X$ making $f$ into a group homomorphism. But that is clearly absurd; if we take for instance $G=1$ then it would imply there is a unique group structure on every set.

I agree that faithful functors are also quite important. But I just can’t bring myself to say that the forgetful functor $\mathrm{Grp}\to\mathrm{Set}$ exhibits Grp as a “subcategory” of Set. I also note that if we regard a 1-category as a 2-category with only identity 2-cells, then every morphism is faithful; thus calling faithful functors “subobjects” is not a conservative extension of the established notion of subobject in a 1-category.

Faithful functors share some of the properties of injections, but I think they are different in enough ways that they deserve to be treated as a new sort of thing that appears under categorification, rather than being shoehorned into the existing notion of “subobject”.

Of course, that’s just a terminological question. Whether or not faithful functors or discrete fibrations are called “subobjects” is independent of what role they should play in the definition of a 2-topos.

Posted by: Mike Shulman on November 10, 2008 7:08 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

Lawvere seems to be against you, Michael, or am I misunderstanding him when he says properties of groups are nothing but their representations as permutations.

If it’s right to have two kinds of variable, as I suggest in my post, perhaps we have the possibility to express two types of question – those expecting a truth value as answer and those expecting a set.

Posted by: David Corfield on November 10, 2008 10:09 AM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

It’s not clear to me that what Lawvere is talking about is very related. But I guess that insofar as his hyperdoctrines allow $PX$ to be a category, rather than a poset, and he still calls their objects “attributes” or “properties”, he could be interpreted as subscribing to the view that a “truth value” could be something with internal structure, like a set.

I definitely agree that it’s right to have two kinds of variable, and that some questions expect a set, a category, or something else as an answer instead of a truth value. I think I’m just saying that there are still questions that expect an ordinary truth value as an answer, and the logic of a 2-topos should be able to deal with them.

And also, as I said, I’m not convinced that all categorified questions can be answered by a fibration. For instance, there are “degenerate” categorified questions whose answer is essentially just an ordinary truth value, and thus should be represented by an ordinary subobject—but not every ordinary subobject is a fibration. The question “does a functor have an adjoint” suggested by Tim is of this form, since adjoints are unique up to unique isomorphism when they exist, and the subobject is that full subcategory of those objects in its codomain at which it has a partially defined adjoint. But the inclusion of a full subcategory is only a fibration if the subcategory is a sieve, and there’s no reason for the domain of a partially defined adjoint to be a sieve.

Posted by: Mike Shulman on November 10, 2008 8:19 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

You mentioned dependent types. Is it possible that our sought after logic has already been discovered by type theorists? I see Jacobs wrote about a first and higher order dependent type theory, but have no access to the book.

Posted by: David Corfield on November 10, 2008 8:56 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

Here’s a thought that just occurred to me, which I find kind of interesting. What I’ve been trying to say with the example of groups is that by using discrete fibrations as the answers to categorified questions, we essentially restrict ourselves to questions whose answers are functorial in their parameters, whereas not all questions have this property. Could we replace discrete fibrations by something more general?

(Small) discrete fibrations are, of course, classified by the universal discrete fibration $\mathrm{Set}_* \to \mathrm{Set}$ . But there is also “sort of” a universal faithful functor with discrete fibers, namely $\mathrm{Rel}_*\to\mathrm{Rel}$ . Here Rel is the category of sets and relations, and $\mathrm{Rel}_*$ is the category of pointed sets and basepoint-preserving relations. Every faithful functor into $X$ with (small) discrete fibers is a pullback of this functor along an essentially unique map from $X$ to Rel. The only catch is that the map from $X$ to Rel will in general be only be a lax functor (regarding Rel as a locally-posetal 2-category).

There is also “sort of” a universal faithful functor, whose codomain is a category of posets and suitable relations between them (with the same caveat). Likewise there is a universal discrete functor if we allow the codomain to be a bicategory (the bicategory of spans), a universal arbitrary functor whose codomain is the bicategory of profunctors, and a universal fibration whose codomain is the 2-category Cat (for the last one the classifying maps are pseudofunctors). About the only thing there doesn’t seem to be is a universal full-and-faithful functor!

Posted by: Mike Shulman on November 10, 2008 11:59 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

This is from more than ten years ago so I’m not sure if anyone is still following, but…

Mike said: “About the only thing there doesn’t seem to be is a universal full and faithful functor!”

There is however a universal full subobject (ie fully faithful, injective on objects functor). This is given by $1 \to I$ , where $I$ is the free living isomorphism. More generally, if $\mathcal{E}$ is a topos then $\mathbf{Cat}(\mathcal{E})$ will have $\mathbf{codisc}\left(\top\right)$ as a universal full subobject, and $\mathbf{disc}\left(\top\right)$ as a universal “inclusion of a collection of connected components”, as can be checked directly from the adjoint strings $\pi_{0} \dashv disc \dashv Ob \dashv codisc$ .

Posted by: Adrian Miranda on October 18, 2019 5:47 AM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

Ugh, this is probably a bit tricky. You should probably worry about getting the basic taxonomy right. I am not sure Lambek and Scott’s talk about indeterminate arrows is really helpful. Have a look at MacLane and Moerdijks “Sheaves in Geometry and Logic”, the chapter on the internal language, for another exposition.

The taxonomy should be:

1. A type is an object in the topos

2. A term t(x,y,z) of type A with variables x:B, y:C, z:D is a 1-morphism from object B \times C \times D to A.

3. In particular, a variable x of type A is interpreted as the identity morphism on A.

4. What corresponds to 2-morphisms? I think the language should contain the notion of reduction. A reduction from term t to term u is then a 2-morphism between corresponding morphisms.

5. I think that if your 2-category has equifiers then you can internalize 2-cells and think of them as ordinary terms (and not special ‘reductions’).

Another thing worth mentioning is that you should never ever interpret a term or a formula without a context which tells you which variables are allowed to be free. For example, the term f(x,y) has a different meaning in context x:A,y:B than in context x:A,y:B,z:C.

P.S. A note to the moderators: it is extremely annoying that your commenting system wants me to write XHTML valid code. I am not a validating XML parser, so I just deleted all the nice HTML tags to get past the system.

Posted by: Andrej Bauer on November 6, 2008 4:00 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

Andrej wrote:

A note to the moderators: it is extremely annoying that your commenting system wants me to write XHTML valid code. I am not a validating XML parser, so I just deleted all the nice HTML tags to get past the system.

The moderators don’t run the technology here; we just post articles. Someday we may move to an environment that’s easier to deal with, but we’re all pretty lazy and reasonably happy here, so it probably won’t happen soon.

I agree that XML is annoying. Here are four tips to keep from running afoul of it:

All HTML commands should be in lower case. Not <UL>, but <ul>, and so on.
When you begin something, you have to end it. So, every <ul> needs to end with a </ul>.
<blockquote> needs a line of space after it, and </blockquote> needs a line of space before it.
Keep it simple.

More advice can be found here, and that’s also the best place to complain or ask questions.

Posted by: John Baez on November 6, 2008 9:40 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

A 2-topos $(\kappa, (-)^*, \tau)$ is a finitely complete cartesian closed 2-category $\kappa$ equipped with a duality involution $(-)^*$ as a classifying discrete opfibration $\tau: \Omega_\bullet \to \Omega$ .

Hm, what’s the systematics here? If I wanted to say 7-topos (say under the provision that it is a strict 7-category, for simplicity) would it just be hopeless from this point of view, or is it at least clear what kind of conditions one would impose?

My impression had originally been that the idea of a topos (as far as its logical aspects are concerned, as in this post here) is really all centered around the classifier $\tau$ , and that all other axioms are essentially just there to make the statement sensible and true.

But now that i read Mike Shulman’s comment #, I see that this is potentially a misleading point of view (?)

I am still recovering from the amazement # that the 0-, 1- and 2-classifying fibrations in $0Cat$ , $1Cat$ an $2Cat$ , respectively, are the the horizonatal morphisms of the kind

$\array{ n Cat_* &\to& n Cat^{I} &\stackrel{codom}{\to}& n Cat \\ \downarrow && \downarrow^{dom} \\ pt &\to& n Cat }$

with the square the pullback diagram.

That clearly suggests what to expect for the classifying fibration for general $n$ .

What is a bit counterintuitive is that only for $n=0$ does this have the naive appearance really of a subobject inclusion (with $0 Cat_* \to 0 Cat$ being $\{1\} \hookrightarrow \{0,1\}$ ) while for $n \geq 1$ this is a forgetful functor – indeed a fibration.

Posted by: Urs Schreiber on November 6, 2008 10:39 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

Urs wrote:

Hm, what’s the systematics here? If I wanted to say 7-topos (say under the provision that it is a strict 7-category, for simplicity) would it just be hopeless from this point of view, or is it at least clear what kind of conditions one would impose?

I think we’re still at a very early stage of understanding $n$ -topoi. I don’t feel Weber’s definition of 2-topos is ‘carved in stone’. But to me the most exciting (and weird) thing about it is the recognition that we need a duality structure generalizing the familiar concept of the ‘opposite’ of a category, where we turn around the arrows:

$op : Cat \to Cat^{co}$

We need this to talk about contravariant functors internal to a 2-topos.

And, note that if we march down this road, we’ll need our 3-topoi to have a duality structure generalizing the (less) familiar concept of the ‘co’ of a 2-category, where we turn around the 2-arrows:

$co: 2Cat \to 2Cat^{rev}$

And so on. It’s a cool example of the ‘microcosm principle’: $n$ -categorical structures tend to make sense only internal to $(n+1)$ -categories with similar structures. (For example, monoids make sense in monoidal categories, which make sense in monoidal 2-categories, etc.)

I also like this stuff because I like the mysteries of ‘ $n$ -categories with duals’ In applications to logic, duality is closely related to negation. In game-theoretic approaches to logic it’s related to the switching the 2 players in a 2-player game. In applications to physics, duality is closely related to antimatter and the operation of ‘charge conjugation’: switching matter and antimatter. There’s something very general at work here, which has not fully been understood.

Posted by: John Baez on November 7, 2008 9:10 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

Or, as the Onion put it:

Posted by: Tom Leinster on November 7, 2008 10:20 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

But to me the most exciting (and weird) thing about it is the recognition that we need a duality structure generalizing the familiar concept of the ‘opposite’

That sounds interesting. I should look at the definition, but: can you tell me in a few words why we “need” the duality structure in an $n$ -topos? What is it needed for? What doesn’t work if we do not have it?

Posted by: Urs Schreiber on November 7, 2008 10:25 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

Urs wrote:

I should look at the definition, but: can you tell me in a few words why we “need” the duality structure in an $n$ -topos? What is it needed for? What doesn’t work if we do not have it?

As I said, we need it to talk about contravariant functors. Category theory without contravariant functors is quite limited! We need contravariant functors to talk about negation in logic, and we need contravariant functors to talk about antiparticles in physics (or mathematically speaking, duals of vector spaces and duals of group representations).

But I think Weber wants contravariant functor because you need them to state the Yoneda embedding theorem, which (as you know) is one of the basic tools in category theory.

Posted by: John Baez on November 7, 2008 10:55 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

I think we’re still at a very early stage of understanding $n$ -topoi.

There is Lurie’s Higher topos theory.

What does that fail to accomplish?

Posted by: Urs Schreiber on November 7, 2008 10:27 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

There is Lurie’s Higher topos theory.

What does that fail to accomplish?

In the language we’re using here, it’s only about $(\infty,1)$ -toposes.

Furthermore, it’s only about Grothendieck $(\infty,1)$ -toposes—those that arise as sheaves (or stacks) on some site. He doesn’t go into their internal logic at all.

Posted by: Mike Shulman on November 7, 2008 10:33 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

Nice picture, Tom. Looks like the Tao is down today.

Posted by: John Baez on November 8, 2008 8:21 AM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

Ha, ha, ha!

Posted by: Eugenia Cheng on November 8, 2008 1:32 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

/me removes his hat and shakes your hand.

I don’t know whether I’m more upset you made the pun or that I didn’t think of it first.

Posted by: John Armstrong on November 8, 2008 3:59 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

I wrote #:

What is a bit counterintuitive is that only for $n = 0$ does [the classifier morphism] have the naive appearance really of a subobject inclusion (with $0Cat_* \hookrightarrow 0Cat$ being $\{1\} \hookrightarrow \{0,1\}$ ) while for $n \geq 1$ this is a forgetful functor – indeed a fibration.

Now Mike Shulman in a way confirms that this kind of puzzlement is justified #

I think my argument is that in the case of a 1-topos, there is a fortuitous coincidence between (a) the subobjects which you use to represent the internal logic and (b) the things that your classifier classifies.

But then: do we need both? Or do 1-topoi generalize in two different directions:

on the one hand: $n$ -categories with universal fibrations, on the other hand $n$ -categories with internal logic?

What does one have to do with the other, apart from the coincidence, if that’s what it is, that the universal 0-fibration is an inclusion of the singleton into the 2-element set?

Posted by: Urs Schreiber on November 7, 2008 10:18 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

There’s definitely room for difference of opinion here. My current feeling is that there is really only one categorification of (elementary) 1-toposes (although the details of that definition are still negotiable). My point is just that the definition of 1-topos we should be categorifying is not “a topos is a category with power objects” but something like “a 1-topos is a Heyting category which additionally is cartesian closed and has a subobject classifier”. Then the resulting categorification would be “a 2-topos is a Heyting 2-category which additionally is cartesian closed, has some sort of duality, and has a discrete fibration classifier.”

A Heyting 2-category is not a categorification of a 1-topos, only of a Heyting 1-category. To be a topos, you should be cartesian closed and have a classifier of some sort. It’s just that in the 2-world, the thing you should classify is different, and having those classifiers doesn’t automatically imply the Heyting structure any more. (Actually, it might; I haven’t tried to see what you can prove or looked for counterexamples. But I doubt it.)

Perhaps it is worth pointing out that it’s unreasonable to expect a 2-topos to have a classifier for subobjects (meaning ffs)? For instance, Cat doesn’t have one. (Gpd does, however, which suggests that $(n,1)$ -toposes are much more similar to 1-toposes than $n$ -toposes are.) Thus, there is no danger of anyone trying to define a 2-topos to be a Heyting 2-category with a subobject classifier, instead of a fibration classifier.

One might argue that there is a useful notion of 2-topos which has a fibration classifier, but which doesn’t have internal logic. Most of the examples of 2-toposes that I know do have internal logic. But even if the weaker notion does turn out to be useful, I might push to reserve the term “2-topos” for the ones that do have internal logic, to strengthen the analogy with 1-toposes.

Posted by: Mike Shulman on November 7, 2008 10:58 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

In Computads and Multitopic Sets indeterminates representing $n$ -morphisms for different $n$ are introduced.

Posted by: David Corfield on November 21, 2008 12:03 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

I should take a look at Michael Warren’s thesis - Homotopy Theoretic Aspects of Constructive Type Theory. Already in the Introduction, ‘higher-dimensional identity types’ make an appearance.

Posted by: David Corfield on January 6, 2009 11:12 AM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

The place to follow up on these discussions is Mike Shulman’s project on nLab.

Posted by: David Corfield on January 30, 2009 4:45 PM | Permalink | Reply to this

Re: The Internal Language of a 2-Topos

$MathML-enabled post (click for more details).$

The place to follow up on these discussions is Mike Shulman’s project on nLab.

Or, at least, to follow up on my take on it. As I say in the introduction, I don’t mean to exclude the possibility of a “categorified logic” such as you and Tim were proposing. I think it would be very interesting. It’s just not what I’m doing right now.

Posted by: Mike Shulman on January 31, 2009 9:02 PM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

November 6, 2008