Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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?
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.
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.
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.
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.
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 :)
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?
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.
1 to 9 of 9