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?