Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeMay 30th 2017
   • (edited May 30th 2017)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have cross-linked the entries _[[forcing]]_ and _[[classifying topos]]_ just a tad more by 1. adding a half-sentence at the end of the paragraph in the Idea-section at "forcing" which mentions the word "classifying topos" 1. adding to "classifying topos" the references (grabbed from "forcing") on the relation between the two: [here](https://ncatlab.org/nlab/show/classifying+topos#ReferencesRelationToForcing). 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.

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

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

   2. 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.

2. • CommentRowNumber2.
   • CommentAuthorDavid_Corfield
   • CommentTimeMay 30th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexTo what extent can the 'forcing' of classifying ($(\infty, 1)$-)toposes be expressed in HoTT? E.g., when we see [here](https://nforum.ncatlab.org/discussion/6946/weiss-topology-and-goodwillie-calculus/?Focus=56173#Comment_56173) > 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?

   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?

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeMay 30th 2017
   • (edited May 30th 2017)
   • PermaLink
   Author: Urs
   Format: MarkdownItexMy 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](https://ncatlab.org/nlab/show/syntactic+category#UniversalProperty), 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](https://ncatlab.org/nlab/show/excisive+%28%E2%88%9E%2C1%29-functor#CharacterizationViaAGenericStableObject)_) in homotopy type theory by adding the above two axioms plus conditions that make the generic pointed object a [[stable homotopy 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.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeMay 30th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThat'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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeMay 30th 2017
   • (edited May 30th 2017)
   • PermaLink
   Author: Urs
   Format: MarkdownItexTo come back to #1 In one such discussion ([here](https://plus.google.com/+johncbaez999/posts/7n5UJgnRcFj)), 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.

   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.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeMay 30th 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, 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.

   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.

7. • CommentRowNumber7.
   • CommentAuthorDavid_Corfield
   • CommentTimeMay 31st 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIt [seems](https://mathoverflow.net/q/75836/447) 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 :)

   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 :)

8. • CommentRowNumber8.
   • CommentAuthorspitters
   • CommentTimeJun 2nd 2017
   • PermaLink
   Author: spitters
   Format: MarkdownItexThere was a bit of discussion with Lurie [here](https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-235) 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?

   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?

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeJun 2nd 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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.

   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.