3
$\begingroup$

This is a vague question, and I apologize in advance for it. I do not need a definite answer, I am happy to just get some general ideas.

An elementary topos can model higher order logic over a dependent type theory (the first type theory in the last chapter of Bart Jacob's book), and that is already sufficient for a lot of mathematics. I have also seen that the stack semantic (paper by Mike Shulman) adds clauses to the Kripke-Joyal Semantic of a topos, which allow to interpret unbounded quantification over types (∀X:Type, ∃X:Type).

I have recently witnessed someone (Ingo Blechschmidt) start an informal argument in the internal language of a sheaf topos (the Zariski topos) like this: Internal to the Zariski topos we can form the category of finitely presented $\mathbb A$-algebras, and the category of internal presheaves on them. I have been told that the right way to make the internal language expressive enough to allow such talk is to extend the internal language, so that it can talk about locally internal categories in $Zar$ (certain Grothendieck fibrations above $Zar$), or even about all fibrations above $Zar$. The type theory which Ingo sketched looked a lot like the logic of a 2-category which you can find in Mike Shulman's part of the nLab.

Here is my confusion: If someone told me that they would like to form for example the category of groups internal to the Zariski topos

Group = ΣG:Type, Σm:G×G→G, Σe:1→G, ...

then I would have guessed that they need to add universes to their semantic, and I would have suspected that they need some set-theoretic Grothendieck-universes from the outside to make that happen (I don't know much about universes in type theory). The extension of the model from the Zariski topos (sheaves on $Ring_{fp}^{op}$) to Zariski-stacks (2-sheaves on $Ring_{fp}^{op}$), that is from a 1- to a 2-categorical world, seemingly goes in an orthogonal direction. (Altough it is also a size increase, since the 2-category $Cat_\kappa$ in which the 2-sheaves take values must be larger than the 1-category $Set_\kappa$, here $\kappa$ is a fixed cardinal). On the other hand, the extension to stacks makes sense, since intuitively the stack $R\mapsto \mathrm{Mod}_R$ should be the interpretation of Vect and the self indexing should be the interpetation of Type.

Questions: Can I also construct the Zariski topos internal to the Zariski topos by adding support for universes to my semantic? Would the resulting theory and its external semantic be essentially different? What is its relation to the (let me call it) language of fibrations over $Zar$?

(I am asking on this side, since I have been told that proofassistant.stackexchange was supposed to be also about categorical logic and the semantic of type theories.)

$\endgroup$
1
  • $\begingroup$ a type theory which can, at least, talk about locally internal categories (but has no constructors for them) is described in ingo blechschmidt's master thesis. $\endgroup$
    – Nico
    Dec 22, 2022 at 12:36

1 Answer 1

2
$\begingroup$

I am not a topos theorist, but here are my 2cts as a type theorist, so take it with a grain of salt. If you have universes in your ambient topos, whatever it is, then you can define internally there the topos of (pre)sheaves over some (internal) category[1]. I assume you do not care about universes in the internal topos, so this problem only occurs for the ambient topos. So I believe that this boils down to having universes in $\mathsf{Zar}$.

It is easy to inherit universes in a presheaf topos from the ambient metatheory. Now, there are complications when you want to get a reasonable notion of universes in a sheaf topos. For it to work, you either have to build very non-constructive universes, or you have to replace Set-valued sheaves by sheaves living in an univalent type theory. The first way is more compatible with the classical view of topos theory, while the second requires a complete change of metatheory. Unfortunately, I don't know how well-behaved the universe structure must be to internalize the (pre)sheaf construction so maybe this is asking a bit too much.

As for the relation between the internal and the external topos, I have no idea but I'm pretty sure it depends on what you believe $\mathsf{Set}$ to be.

[1] If you want to do this in intensional type theory, it is much less trivial and requires some serious tinkering.

$\endgroup$
1
  • $\begingroup$ I mostly agree with this, but let me make one comment --- for Nico's purposes, the (constructive!) universes of sheaves outlined by Thomas Streicher in his paper "Universes in toposes" will work fine, so there is no need to resort to the non-constructive universes from the paper of Gratzer, Shulman, and Sterling. $\endgroup$ Dec 31, 2022 at 8:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.