3
$\begingroup$

What is an internal language of the Sierpiński topos, which is defined as arising from the category $\mathsf{Set}^{\to}$, the category of arrows in $\mathsf{Set}$? Or more generally, is there a rough description of the internal language of sheaf topoi?

I think that this language should consist of the ordinary higher order intuitionistic logic, plus two operators $\bullet,\circ$, corresponding to the two monads coming from the adjunction $\mathsf{dom} \vdash \mathrm{id}_{(-)} \vdash \mathsf{cod}$. Another description is to think of $f : A \to B$ in $\mathsf{Set}$ as a multiset, whose elements are $b \in B$, and the multiplicity is defined as the cardinality of $f^{-1}(b)$. Then $\mathrm{id}_{(-)} \circ \mathsf{dom}$ represents the operation that takes a multiset and forgets that equal elements were equal; $\mathrm{id}_{(-)} \circ \mathsf{cod}$ takes a multiset and removes multiplicities.

More generally, for a sheaf category $\mathsf{Sh}(X)$, is it sufficient to assume operations $\circ_U, \bullet_U$ for each open set $U \subseteq X$?

Improve this question
$\endgroup$
8
  • 4
    $\begingroup$ I'm not sure what it is that you call an "internal language", but that's not what people usualy refer to. "The internal logic" of a topos is an interpretation of some (intuitionistic) structural set theory where set are interpreted as objects of the topos. But it doesn't have additional operation corresponding to the sort of thing you describe (beyond constants symbol for the objects and morphisms of the topos). A meaningful question here is whether the operations you describe can be added to the internal logic, but that seem weaker than what you want to ask. $\endgroup$
    – Simon Henry
    Commented Jun 9, 2022 at 16:00
  • $\begingroup$ @SimonHenry I'm actually pretty confused by your comment. You are describing the "internal language of toposes" and what this question is asking is about the "internal language of toposes equipped with a geometric morphism into the Sierpinski topos". The question is clearly meaningful as-written. $\endgroup$
    – Jonathan Sterling
    Commented Jul 31, 2022 at 9:03
  • $\begingroup$ @JonathanSterling If you understand what the question mean - I'd be happy to here your explanation, but it is definitely not clear to me. I know what the internal language is, but I don't what to answer to the question "what is the internal language of a given topos" beyong the obvious "well, it has a type for each of the topos etc...". Given the way you rephrase the question, I feel you want to interpret it as a classifying topos - but I'm not sure this is a correct way of interpreting what the author is asking, as this point of view only see the geometric part of the theory... $\endgroup$
    – Simon Henry
    Commented Jul 31, 2022 at 9:11
  • $\begingroup$ ...e.g. in the Sierpinski topos $\neg \neg U$ is true, while in a topos with a geometric morphism to the Sierpinski topos it is not always. Also these "operator" the OP mention wouldn't clearly make sense in a general topos over the Sierpinski topos. More generally, how would you answer the question "what is the internal language of the topos of Sets" ? $\endgroup$
    – Simon Henry
    Commented Jul 31, 2022 at 9:13
  • 2
    $\begingroup$ @JonathanSterling : I disagree with your interpretation - the original post never mentioned geometric morphisms and the construction he talks about are clearly not preserved by geometric morphism. Given that the internal logic isn't preserved by geometric morphism, introducing them here is a rather strange things to do. In any case - the discusion we are having now somehow prove my point that the original question is not precise enough. $\endgroup$
    – Simon Henry
    Commented Aug 3, 2022 at 12:28

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .