The n-Category Café

Well, of course (as you probably know) we have to be a bit careful about what’s left when we “discard power sets.” For instance, if we start with “Set is a well-pointed category with finite limits and power objects and the axiom of choice” (one version of ETCS), and we discard power objects (and choice), we won’t be left with a very good definition of $Set$. The predicative version of ETCS says that $Set$ is a well-pointed pretopos, possibly locally cartesian closed (depending on the sort of predicativist you are). There seems to be some debate about whether to use classical logic either, although if you want function sets then you have to use intuitionistic logic, since a cartesian closed Boolean category is an elementary topos.

But regarding the particular matter at hand, I believe that for the basic theory of Grothendieck (0,1)-toposes, it should be enough to just assume that $Set$ is a well-pointed pretopos. Obviously we won’t be able to use the parts of topos theory that invoke subobject classifiers, but if we assume function sets in $Set$ then we’d be able to use the parts that invoke cartesian closure.

Hmm, I just thought of another interesting connection between higher topos theory and predicativism. Subobject classifiers in 1-topoi generalize to “(truncated-)object classifiers” in (n,1)-topoi, except that for $n\gt 1$ you can’t classify all objects, only some cardinality-bounded collection of them. So it might be reasonable to consider the claim that $Set$ (and likewise any 1-topos) has, not a single subobject classifier, but a family of them which jointly “exhast all subobjects”. I think people have considered that sort of axiom before also, in the direction of “predicative elementary topos”. (Similarly, I believe the proof that an (n,1)-topos has object classifiers uses the existence of arbitrarily large regular cardinals, which is not a theorem constructively but has to be taken as an additional axiom.)

The moment you said this here:

Obviously we won’t be able to use the parts of topos theory that invoke subobject classifiers,

I had this very same thought:

Subobject classifiers in 1-topoi generalize to “(truncated-)object classifiers” in $(n,1)$-topoi, except that for $n \gt 11$ you can’t classify all objects, only some cardinality-bounded collection of them.

So maybe the axioms of elementary toposes deserve some refinement after all:

So it might be reasonable to consider the claim that Set (and likewise any 1-topos) has, not a single subobject classifier, but a family of them which jointly “exhast all subobjects”.

That sounds like it would make a lot of things fall nicely into place.

That reminds me, I need to think about and understand explicit descriptions of $k$-truncated object classifiers in more general $(n,1)$-toposes than $(n-1)Grpd$. Have you thought about that?

I realize that probably we wouldn’t get all that far without function sets, since otherwise $Set$ isn’t locally small or complete, we don’t have a good adjoint functor theorem, and our geometric morphisms probably don’t have right adjoint parts. I think a $\Pi$-pretopos with “object classifiers” has been studied by someone under a name like “stratified pseudo-topos”, but I can’t remember who it was at the moment.

I need to think about and understand explicit descriptions of k-truncated object classifiers in more general (n,1)-toposes

I would guess that it’s just something like, for each $U$ in the site $C$, consider the category of k-sheaves on $C/U$ of cardinality below some bound. As $U$ varies that should form a (k+1)-sheaf on $C$ which is an object of the (n,1)-topos in question when n is sufficiently larger than k.

[I’ve picked this up very late, but I hope the comment is still of interest.]

I thank Bas for mentioning my programme. I want to elaborate on that by explaining how topos theory did make me a predicativist.

The realm of geometric logic is essentially that fragment of the internal mathematics of Grothendieck toposes that is preserved by the inverse image functors of geometric morphisms. (In fact that is pretopos structure + some other stuff, so this provides one answer to Mike’s original thought of Grothendieck toposes as being “some kind of” pretopos.)

The wonderful thing about this fragment is that if you use it to reason about points of a point-free space X, then the reasoning applies not only to global points (maps 1 -> X), of which there may be insufficient, but also to generalized points (maps W -> X) such as the generic point (Id: X -> X). This overcomes most of the disadvantages that arise from the insufficiency of points in a non-spatial space.

In short, if your reasoning is geometric you can deal with point-free spaces as though they had enough points.

This is a huge improvement on having to work explicitly with the frames or their presentations, and for a decade or two now I have been doing my best to work geometrically wherever possible.

Since geometric reasoning does not include powersets, I have found that that in effect makes me a predicativist and I have found it very easy to participate in predicative mathematics such as formal topology.

To repeat, topos theory did make me a predicativist.

Note that geometric reasoning does not even include exponentials (function types). This sounds terribly weak, but in practice there are ways round. One important observation is that the exponential of sets, although not another set, is a locale. What underlies this is that the exponential of sets has a natural topology that is non-discrete. You can see this very clearly if you think of equality of functions: it is of a different nature from the equality on the sets, and it is not open in the function space topology.

Bas also mentioned Joyal’s Arithmetic Universes. These are pretoposes equipped with parametrized list objects. The idea is that the infinitary disjunctions of geometric logic can (in practical examples) be eliminated in favour of finitary disjunctions and existential quantification over types such as N and Q constructible within AUs.

Here the lack of exponentials is impossible to fudge: they are not just absent from the logic, they are completely absent from the categories (AUs instead of Grothendieck toposes). Milly Maietti and I have started to explore how to work in these, in “An induction principle for consequence in arithmetic universes”.

Yes. For example: given a set X, and a collection R of subsets of X, how do you construct the smallest topology making every subset in R open?

Predicative answer (“bottom-up”): take R. Throw in all unions of sets in R. Throw in all finite intersections. Throw in all unions. Throw in all finite intersections. Repeat (possibly transfinitely) until you have a topology.

Impredicative answer (“top-down”): consider the set of all topologies on X making every subset in R open. This set is closed under arbitrary intersection. So take the intersection of everything in it.

Good question. I think predicativity can also roughly be described under the heading of “constructive”, in the informal sense of “giving a construction”, even if it doesn’t necessarily imply intuitionistic logic. An impredicative definition like “let $R$ be the intersection of all equivalence relations containing $S$” is certainly not as “constructive” a way to define $R$ as the predicative version “let $x R y$ mean that there is a finite sequence $(x=x_0,x_1,\dots,x_n=y)$ such that for all $0\le i\lt n$, either $x_i S x_{i+1}$ or $x_{i+1} S x_i$.” In particular, a constructive predicative proof can often have an algorithm formally extracted from it via the Curry-Howard correspondence for $\lambda$-calculus or Martin-Löf type theory. So perhaps one answer is that predicativity may be noticed by someone trying to make their proofs effectively computable.

One could of course try to make the same argument for predicativity as Johnstone does for constructivity. I have to say that I find a lot of impredicative proofs and definitions more elegant than their predicative versions (to the extent that I occasionally waste time wishing that we could make (n,1)-toposes more like (0,1)-toposes, rather than the other way round), but others may disagree.

Yes, certainly! A predicative definition (predicativism is more about definitions, while constructivism is more about proofs, although of course these can't be completely disentangled) has a much more concrete feel than an impredicative definition.

Compare these two (nonconstructive) proofs of the (classical) Intermediate Value Theorem (and so much for my claim that predicativism is more about definitions, since this example is a proof).

Theorem: If $f\colon [0,1] \to \mathbb{R}$ is continuous, $f(0) \lt 0$, and $f(1) \gt 0$, then $f(c) = 0$ for some $c$.

Proof 1: Let $c$ be $\sup \{ x \;|\; f(x) \leq 0 \}$, which exists (in $[0,1]$) since $[0,1]$ is compact. If $f(c) \lt 0$ or $f(c) \gt 0$, we use continuity to derive a contradiction (skipped here). Therefore, $f(c) = 0$.

Proof 2: Let $a_0$ be $0$, let $b_0$ be $1$, and inductively define:

• $c_n = (a_n + b_n)/2$,
• $a_{n+1} = a_n$ if $f(c_n) \gt 0$ but $a_{n+1} = c_n$ if $f(c_n) \geq 0$,
• $b_{n+1} = b_n$ if $f(c_n) \lt 0$ but $b_{n+1} = c_n$ if $f(c_n) \leq 0$.

Then $(c_n)_n$ is a Cauchy sequence (by elementary algebra, skipped here), so has a limit $c$ (in $[0,1]$, since that is Cauchy complete), and $f(c) = 0$ (again by contradiction and continuity, skipped).

Proof 1 is impredicative and abstract, while Proof 2 is predicative and concrete. In Proof 1, $c$ is basically defined as the largest number that will do; in Proof 2, $c$ is explicitly constructed. You could try to program a computer to calculate $c$ (to any desired degree of accuracy) using Proof 2 as a guide; good luck trying that with Proof 1! (Because Proof 2 is not constructive, your program may eventually have to give up and round off when trying to decide the sign of $f(c_n)$, but it'll be good enough for many purposes. Trying to overcome this limitation leads to various constructive versions of the IVT.)

Here's another example (a definition finally, and incidentally constructively valid either way).

We may define a smooth (or whatever) manifold as a set equipped with a covering collection of mutually compatible charts (called an atlas) and we wish to define the maximal atlas $M(A)$ associated to the original atlas $A$. (This is allegedly useful since two atlases with the same maximal atlas are be regarded as defining the same manifold structure, so that we may formally define a smooth manifold as a set equipped with a maximal smooth atlas. Whether this is actually useful is another matter.)

Definition 1: $M(A)$ is the union of all those atlases $M$ with the property that every chart in $M$ is compatible with every chart in $A$.

Definition 2: $M(A)$ is the collection of all charts $C$ such that $C$ is compatible with every chart in $A$.

(In both cases, we should go on to prove the desired claims about $M(A)$, beginning with the fact that it is an atlas at all.)

I have seen Definition 1 in textbooks. Definition 2 strikes me as obviously superior: both simpler and more concrete. While Definition 1 is impredicative, Definition 2 is predicative. (Predicatively, $M(A)$ may be a proper class even if $A$ is not, which kind of obviates the motivation for defining $M(A)$, but that was a silly motivation anyway. And even if you impredicatively accept that $M(A)$ is a small set, Definition 2 is still more concrete.)

As I said, there is a close connection between predicativity and geometricity, preservation under geometric morphisms. By working directly with a theory, rather then the set, or topological space, of its models, we deal with a more robust notion. This saves a lot of bookkeeping.

In another direction, there have been heated discussions on the FOM-list on predicativity (in this context combined with classical logic). Nik Weaver claims that the spaces in functional analysis that have a name are all predicatively definable, illustrating his point that real mathematicians (functional analysists) do not use impredicativity. As a warning I should add that there is a distinction between predicative (roughly, upto $\Gamma_0$ and generalized predicative (roughly, no power set).

Bas