Michael Shulman colimits in an n-pretopos

An $n$-pretopos has coproducts and quotients of $n$-congruences, which are important classes of colimits. From these we can construct some other colimits, such as the following.

Theorem

A 2-pretopos admits copowers with any finite category.

Proof

If $C$ is a finite category and $A\in K$ is an object, we build a finite 2-polycongruence with one copy of $A$ indexed by each object $c\in C$, and with the hom-object from $A_c$ to $A_d$ being $\sum_{C(c,d)} A ^{\mathbf{2}}$. It is easy to check that a quotient of this congruence is a copower $A\bullet C$.

However, an $n$-pretopos can fail to admit all finite colimits, for essentially the same reason as when $n=1$: some ostensibly “finite” colimits secretly involve infinitary processes. In a 1-category, this manifests in the construction of arbitrary coequalizers and pushouts, where we must first generate an equivalence relation by an infinitary process and then take its quotient. Likewise, a 2-pretopos can fail to admit pushouts, coinserters, coinverters, and coequifiers.

For 2-categories it is even easier to find counterexamples. The 1-pretopos $FinSet$ does in fact have all finite colimits, but the 2-pretopos $FinCat$ of finite categories does not have coinserters or coinverters. (It does have coequifiers, for the same reason that $FinSet$ has coequalizers). The category $FPCat$ of finitely presented categories, on the other hand, does have finite colimits, but fails to have finite limits.

You can also generate the equivalence relation using a higher-order process. Thus a topos (where higher-order processes occur) has all coequalisers, even if it's not a $W$-pretopos (where countably infinitary processes occur).

Incidentally, this is the example that first made me agree that predicativity was a reasonable constructive restriction. I just asked myself which way of generating an equivalence relation seemed more ‘constructive’.

—Toby

Indeed so. I noted at classifying cosieve that you can do the same thing in a 2-category if you have only a poset of truth values rather than a set. All this work on 2-toposes is actually making me more sympathetic to predicativism as well, because in the 2-dimensional case there isn’t really a “higher-order” version you can recourse to; you have to do things the “more constructive” way. Put differently, why is it okay to have a set (or poset) of all truth values, but not a category of all sets?

(Mathieu Dupont and I have been speculating about whether there could actually be a category of all sets; i.e. whether there could be a 2-pretopos having (exponentials, duality, and) a classifying discrete opfibration that classifies all discrete opfibrations. This would have marvelous consequences like that Set has all (not just small) limits and colimits, and so the adjoint functor theorem can be just true without any messing around with generators. But it is inconsistent with there being enough groupoids, or with Set being a topos, and hence also inconsistent with classical logic. I don’t really have very high hopes that it is consistent at all. Having a (1,2)-category of all posets appears to be inconsistent with just exponentials and duality.)

BTW, I assume that by “$\Pi$-pretopos” you meant “$\Pi$-pretopos with a NNO?” In my limited experience “$\Pi$-pretopos” means “locally cartesian closed pretopos” which certainly includes all toposes.

-Mike

Sorry, I removed the wrong letter from ‘$\Pi$-$W$-pretopos’. I meant a $W$-pretopos, that is a pretopos in which every polynomial functor has pullback-stable initial algebras in every slice category (which may follow from simply a pullback-stable NNO, I forget).

In my experience, when you can't find an inconsistency but you're sure that one exists, then the Burali-Forti paradox always works. There may be a simpler one, but Burali-Forti is the surest.

—Toby

I think that Burali-Forti works in this case to get a contradiction from having enough groupoids. But I can’t make it do anything else, because without cores, all I can construct is a poset of ordinals, which isn’t itself an ordinal because an ordinal is a set equipped with a certain sort of relation.

Why are you changing my $\Pi$s to characters that I can’t type?

-Mike

Sorry, I started to fix the ‘Π’s (and ‘$\Pi$’s), then realised that I was fixing some inappropriately and so changed them back (but apparently not always to what they had been before). And you can type that character, as Π. Actually, since you're using Ubuntu like me, you can install SCIM and use that to type it directly (the TeX input method is pretty neat). That said, ‘$\Pi$’ (also ‘$W$’), in math mode, is probably more appropriate, as it refers to closure under a type operation with that name.

I'll try to think about it and see if I can make a paradox work. I don't quite understand how you construct these posets that don't have underlying sets. Although it reminds of me of Paul Taylor's Abstract Stone Duality, where there is a topological space of truth values (in fact one free on a poset) but no underlying set of such.

—Toby

I can type Π but when I view the source that you’ve typed, I don’t see Π but rather an actual Pi-character.

-Mike

It produces the same output in the displayed XHTML. If you want to get Π in your Markdown source, either cut and paste from the display of Π, or install SCIM (or something along those lines) like I did. —Toby

Also, see the new page category of all sets regarding posets and categories that don’t have underlying sets.

-Mike

Will do. —Toby

I don’t want to get a Pi-character in my Markdown source; my point was rather that I wished you wouldn’t put it in yours! I thought the whole point of things like HTML entities like Π and TeX code like $\Pi$ was so that we could produce nice-looking math just by inputting ordinary ASCII text that can be read and edited without installing any fancy fonts or software.

-Mike

OK, fair enough, it's your web, so all special characters will be implemented as XHTML or SGML character entities (unless available through Instiki, of course). —Toby

However, once we have some infinitary structure, this problem goes away.

Theorem

A countably-extensive $n$-pretopos has all countable colimits.