[-- Attachment #1.1: Type: text/plain, Size: 926 bytes --] Dear all, It is my understanding that the interpretation of HoTT inside higher topoi is an ongoing field of research. Much of this business involves subtle strictness properties and things like contextual and syntactic categories. In the 1-topos case there is the Kripke-Joyal/Stack - semantics. These semantics are easy to use in practice. Naively, it seems one could lift the Kripke-Joyal semantics by not asking for truth but simply an inhabitant of a type. Has this been investigated at all? Is it ultimately fruitless? -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/1b613bab-505c-4880-9778-4e3206872294%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1281 bytes --]

[-- Attachment #1: Type: text/plain, Size: 4563 bytes --] Hi Alexander, I think what you are asking is "what is the internal language of an oo-topos". This is doesn't really make much sense as stated since we don't have a definition for "internal language" in an oo-topos. But we expect that once we can define such a notion, then it ought to be HoTT. This will require further work, but recently there have been some big strides towards this direction with Mike Shulman's work <https://arxiv.org/abs/1904.07004>. The Kripke-Joyal semantics of a topos of sheaves is essentially a dictionary between the "internal language" of this 1-topos and what it means externally. I have quotation marks here because I am not being very precise and phrases like "internal language" do have precise meanings which I don't care to look up right now. You are correct that these have been used in practice. Just look at Ingo Blechschmidt's work <https://rawgit.com/iblech/internal-methods/master/notes.pdf>. He discusses on pg. 199 briefly the thing that you consider. The thing to note with Mike's work is theorem 11.1, which shows that every oo-topos can be presented by a "type-theoretic model topos". Now you can think of Kripke-Joyal semantics as a "machine" that can translate between internal and external statements. Here is a page on the nlab <https://ncatlab.org/nlab/show/HoTT+methods+for+homotopy+theorists> that shows what this will probably end up looking like. To get an idea what such a machine might do, have a look at Charles Rezk's "translation" <https://faculty.math.illinois.edu/~rezk/freudenthal-and-blakers-massey.pdf> of a HoTT proof of Blakers-Massey into higher topos theory. The key point here is that this proof was not known in higher topos theory before. It is a very natural argument in HoTT however. I would say this is pretty fruitful. The reason I keep saying "probably" is because nobody has actually formally written down these semantics that I know of. Kripke-Joyal semantics are fairly technical already, just look at Ingo's thesis. And you are correct that with HoTT there are lot's of subtleties involved. So to answer you final question: yes it is being investigated and yes it seems to be fruitful. I will add however that apart from Ingo's work, I don't know of many people using Kripke-Joyal semantics to actually do algebraic geometry. It's true that Ingo discovered some new arguments (generic freeness) but these have yet to catch on with "regular" algebraic geometers. This is because even though it is a 200 page thesis, it only covers foundational aspects of the subject, i.e. the basics of scheme theory. There is much more work to be done before it gets mainstream. We will probably see algebraic topologists using the internal language of (oo-)toposes well before algebraic geometers do. Since we already have examples of these almost being done. These are just my thoughts on your question and is no means the word of an expert. Best, Ali Caglayan On Tue, Oct 8, 2019 at 4:07 PM Alexander Gietelink Oldenziel < a.f.d.a.gietelinkoldenziel@gmail.com> wrote: > Dear all, > > It is my understanding that the interpretation of HoTT inside higher topoi > is an ongoing field of research. Much of this business involves subtle > strictness properties and things like contextual and syntactic categories. > In the 1-topos case there is the Kripke-Joyal/Stack - semantics. These > semantics are easy to use in practice. Naively, it seems one could lift > the Kripke-Joyal semantics by not asking for truth but simply an inhabitant > of a type. > > Has this been investigated at all? Is it ultimately fruitless? > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/1b613bab-505c-4880-9778-4e3206872294%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/1b613bab-505c-4880-9778-4e3206872294%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DjTaw4CD3Lha4fkKFgcYLpypzzDa0J8pPT1eYnZV1qUaQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 5864 bytes --]

In the 1-category case, Kripke-Joyal is a specific formulation of the internal language of a 1-topos (or more general 1-category), involving a forcing relation relating objects of the topos to formulas in its internal logic. The existing work on internal languages for higher categories, including all of the links provided by Ali, is not actually Kripke-Joyal style but is a categorification of a different approach to internal languages that directly constructs objects corresponding to each formula, the connection being that the forcing relation is a representable functor and the interpretation objects are what represent it. I understood the question to be whether, in contrast to all of this existing work, there is also a Kripke-Joyal-style approach to internal languages of higher categories. I expect that probably there is, but I don't think such a thing has been written down yet, although I hear that Awodey and Gambino have been thinking about it. But my instinct is that a Kripke-Joyal approach wouldn't make the coherence questions any easier, since it's basically just a translation through the Yoneda lemma; any coherence technique that can be used for one version should also work for the other. On Tue, Oct 8, 2019 at 9:36 AM Ali Caglayan <alizter@gmail.com> wrote: > > Hi Alexander, > > I think what you are asking is "what is the internal language of an oo-topos". This is doesn't really make much sense as stated since we don't have a definition for "internal language" in an oo-topos. But we expect that once we can define such a notion, then it ought to be HoTT. This will require further work, but recently there have been some big strides towards this direction with Mike Shulman's work. > > The Kripke-Joyal semantics of a topos of sheaves is essentially a dictionary between the "internal language" of this 1-topos and what it means externally. I have quotation marks here because I am not being very precise and phrases like "internal language" do have precise meanings which I don't care to look up right now. > > You are correct that these have been used in practice. Just look at Ingo Blechschmidt's work. He discusses on pg. 199 briefly the thing that you consider. > > The thing to note with Mike's work is theorem 11.1, which shows that every oo-topos can be presented by a "type-theoretic model topos". Now you can think of Kripke-Joyal semantics as a "machine" that can translate between internal and external statements. Here is a page on the nlab that shows what this will probably end up looking like. > > To get an idea what such a machine might do, have a look at Charles Rezk's "translation" of a HoTT proof of Blakers-Massey into higher topos theory. The key point here is that this proof was not known in higher topos theory before. It is a very natural argument in HoTT however. I would say this is pretty fruitful. > > The reason I keep saying "probably" is because nobody has actually formally written down these semantics that I know of. Kripke-Joyal semantics are fairly technical already, just look at Ingo's thesis. And you are correct that with HoTT there are lot's of subtleties involved. > > So to answer you final question: yes it is being investigated and yes it seems to be fruitful. > > I will add however that apart from Ingo's work, I don't know of many people using Kripke-Joyal semantics to actually do algebraic geometry. It's true that Ingo discovered some new arguments (generic freeness) but these have yet to catch on with "regular" algebraic geometers. This is because even though it is a 200 page thesis, it only covers foundational aspects of the subject, i.e. the basics of scheme theory. There is much more work to be done before it gets mainstream. > > We will probably see algebraic topologists using the internal language of (oo-)toposes well before algebraic geometers do. Since we already have examples of these almost being done. > > These are just my thoughts on your question and is no means the word of an expert. > > Best, > Ali Caglayan > > > On Tue, Oct 8, 2019 at 4:07 PM Alexander Gietelink Oldenziel <a.f.d.a.gietelinkoldenziel@gmail.com> wrote: >> >> Dear all, >> >> It is my understanding that the interpretation of HoTT inside higher topoi is an ongoing field of research. Much of this business involves subtle strictness properties and things like contextual and syntactic categories. >> In the 1-topos case there is the Kripke-Joyal/Stack - semantics. These semantics are easy to use in practice. Naively, it seems one could lift the Kripke-Joyal semantics by not asking for truth but simply an inhabitant of a type. >> >> Has this been investigated at all? Is it ultimately fruitless? >> >> -- >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/1b613bab-505c-4880-9778-4e3206872294%40googlegroups.com. > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DjTaw4CD3Lha4fkKFgcYLpypzzDa0J8pPT1eYnZV1qUaQ%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQzEpWEtHZvNKPJxBnYPBxh2XhKB4jobVT0BZmn%3DvP42QQ%40mail.gmail.com.