I think it’s pretty easy to see (using facts from HTT) that any $(\infty,1)$-topos of presheaves on a 1-category $C$ classifies flat $(\infty,1)$-functors out of $C$, which necessarily land inside the 0-truncated objects of any $(\infty,1)$-topos.

]]>There was a bit of discussion with Lurie here about geometric type theory inspired by the work of Vickers and Maietti. Let’s start simple. Consider Mike’s models of inverse categories. Do they classify what we expect them to classify? Has this even been worked out for Sierpinski space?

]]>It seems that forcing relations aren’t the only ones between set universes, and that one could go so far as to view the set multiverse as a category

where all the models of set theory appear as the objects, and all of the known ways that they can relate appear as morphisms, including elementary embeddings, the forcing extension relation, embeddings from one model to an inner model of another, the end-extension relation, and so on.

Maybe taking on the challenge of making category theoretic sense of some larger picture like this would be profitable. Another job for Jesse :)

]]>Thanks, Mike. Yeah, I am faintly aware of this subtlety. Shouldn’t have said “is precisely”.

In any case, all the more do I wish somebody would write a useful presentation of these relations.

]]>To come back to #1

In one such discussion (here), John Baez writes:

]]>So, I could learn the topos-theoretic approach and read Fourman’s paper to see how it connects to the classical approach. Or, maybe the references you mention work that out. I just don’t want to be trapped in a world where I understand forcing but can only talk about it to topos theorists.

That’s close to right, but there’s a subtlety to remember. The syntactic category of HoTT is (conjecturally) an *elementary* $\infty$-topos, whereas the classifying topos of a theory is supposed to be a *Grothendieck* $\infty$-topos. Moreover, the former has (conjecturally) a universal property with respect to *logical* functors, whereas the latter has a universal property with respect to *geometric* morphisms.

The precise thing to say is that classifying toposes, in the sense usually understood, only exist for *geometric theories*: theories presented by axioms that use only the strurcture preserved by inverse image functors of geometric morphisms, i.e. finite limits and arbitrary colimits (including unions of subobjects). The “1-theories” of this sort are geometric logic; probably there is a somewhat more general kind of “geometric $\infty$-logic”. But an arbitrary set of axioms in HoTT, involving type constructors like $\Pi$s, doesn’t have a classifying topos. Moreover, the classifying topos of a geometric theory is not the syntactic category of the dependent type theory containing those axioms; instead we take the syntactic category of the *geometric* theory containing those axioms, and use it as a site to build a topos of sheaves.

My understanding is that this is precisely right. The passage of going from an $\infty$-topos $\mathbf{H}$ to the $\infty$-topos

$\mathbf{H}[X_\ast] \coloneqq [\infty Grpd^{\ast/}_{fin}, \mathbf{H}]$which has a pointed object freely adjoined (namely the 0-sphere $S^0 \in \infty Grpd_{fin}$ under the Yoneda embedding) should correspond to adding to the internal language of $\mathbf{H}$ the axioms

$\begin{aligned} & \vdash X \colon Type \\ & \vdash e \colon X \end{aligned} \,.$This should be just an $\infty$-version of the story of the univeral property of the syntactic category here, modulo the usual caveats that apparently type theorists forgot to write out the proofs that are needed here to make this fully precise.

My understanding is that this is what drives for example the idea by Eric Finster et al. on axiomatizing the tangent $\infty$-topos

$T \mathbf{H} \simeq \mathbf{H}[X_\ast]/(\Sigma \Omega (X^{S_\ast}_\ast) \to X^{S_\ast}_\bullet)_S$(see at *Characterization via a generic stable object*)

in homotopy type theory by adding the above two axioms plus conditions that make the generic pointed object a stable homotopy type.

]]>To what extent can the ’forcing’ of classifying ($(\infty, 1)$-)toposes be expressed in HoTT? E.g., when we see here

the classifying $\mathbf{H}$-topos for pointed objects, the result of going to the internal logic of $\mathbf{H}$ and decreeing

Let there be a pointed object!

is this expressible as some kind of declaration of an element of some type?

]]>I have cross-linked the entries *forcing* and *classifying topos* just a tad more by

adding a half-sentence at the end of the paragraph in the Idea-section at “forcing” which mentions the word “classifying topos”

adding to “classifying topos” the references (grabbed from “forcing”) on the relation between the two: here.

I imagine any categorical logician who would write a pedagogical exposition at *forcing* on how this concept appears from the point of view of topos theory could have some effect on the community. The issue keeps coming up in discussions I see, and so if we had a point to send people to really learn about the relation (instead of just being bluntly old that there is one) that might have an effect.