done
]]>fixed citation
]]>citation
]]>citation
]]>fixing citation
]]>added K-J for HoTT by Awodey, Gambino, Hazratpour, 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.:
[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
]]>Added references to
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)
I added the suggestion that there is a version for HoTT.
]]>