# Start a new discussion

## Not signed in

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

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorDavid_Corfield
• CommentTimeMay 21st 2018

I added the suggestion that there is a version for HoTT.

• CommentRowNumber2.
• CommentAuthorThomas Holder
• CommentTimeJun 29th 2020

• Anders Kock, Universal Projective Geometry via Topos Theory , JPAA 9 (1976) pp.1-24.

• Anders Kock, Elementwise semantics in categories with pull-backs , arXiv:2004.14731 (2020). (abstract)

• CommentRowNumber3.
• CommentAuthorjulia9367
• CommentTimeApr 17th 2022
• (edited Apr 17th 2022)

I think it would be nice to add the specialisation of sheaf semantics for any topos of sheafs of sets on a site. In this case we have nice concrete interpretations of the logic. E.g.:

• it suffices to consider generalized elements of the form $x \in \mathcal{F}(U)$
• any formula is true if it is true on an open cover
• $\implies$ = implies on all open subsets
• $\neg$ = false on all open subsets
• $\neg\neg$ = false that (it is false on all open subsets) of all open subsets = true on a dense open subset

[1] is a beautiful application of this to scheme theory simplifying many statements and proofs.

[1]: Using the internal language of toposes in algebraic geometry, Ingo Blechschmidt, https://arxiv.org/abs/2111.03685