Hi Alexander,

I think what y=
ou 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 hav=
e a definition for "internal language" in an oo-topos. But we exp=
ect that once we can define such a notion, then it ought to be HoTT. This w=
ill require further work, but recently there have been some big strides tow=
ards this direction with Mike =
Shulman's work.

The Kripke-Joyal semantics=
of a topos of sheaves is essentially a dictionary between the "intern=
al language" of this 1-topos and what it means externally. I have quot=
ation 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 hav=
e been used in practice. Just look at Ingo Blechschmidt's work. He dis=
cusses on pg. 199 briefly the thing that you consider.

The thing to note with Mike's work is theorem 11.1, which shows th=
at every oo-topos can be presented by a "type-theoretic model topos&qu=
ot;. Now you can think of Kripke-Joyal semantics as a "machine" t=
hat can translate between internal and external statements. Here is a pa=
ge 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" o=
f a HoTT proof of Blakers-Massey into higher topos theory. The key point he=
re 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 kn=
ow of. Kripke-Joyal semantics are fairly technical already, just look at In=
go's thesis. And you are correct that with HoTT there are lot's of =
subtleties involved.

So to answer you final qu=
estion: yes it is being investigated and yes it seems to be fruitful.

=
I will add however that apart from Ingo's work, I d=
on't know of many people using Kripke-Joyal semantics to actually do al=
gebraic geometry. It's true that Ingo discovered some new arguments (ge=
neric freeness) but these have yet to catch on with "regular" alg=
ebraic geometers. This is because even though it is a 200 page thesis, it o=
nly covers foundational aspects of the subject, i.e. the basics of scheme t=
heory. 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. Sinc=
e we already have examples of these almost being done.

These are just my thoughts on your question and is no means the word o=
f an expert.

Best,

Ali Caglayan<=
br>

On Tue, Oct 8, 2019 at 4:07 PM Alexander Gietelink=
Oldenziel <a.f.=
d.a.gietelinkoldenziel@gmail.com> wrote:

Dear all,<= div>It is my understanding that the interpretation of HoTT inside higher to= poi is an ongoing field of research. Much of this business involves subtle = strictness properties and things like contextual and syntactic categories.= =C2=A0In the 1-topos case there is the Kripke-Joyal/Stack - sema= ntics. These semantics are easy to use in practice.=C2=A0 Naively, it seems= one could lift the Kripke-Joyal semantics by not asking for truth but simp= ly an inhabitant of a type.=C2=A0Has this been in= vestigated at all? Is it ultimately fruitless?

You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.

To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com.

To view this discussion on the web visit ht= tps://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 &= quot;Homotopy Type Theory" group.

To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.

To view this discussion on the web visit https://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DjTaw4CD3Lha4fkKFgcYLpy= pzzDa0J8pPT1eYnZV1qUaQ%40mail.gmail.com.

--00000000000038da2f059468c5ff--