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.
> To view this discussion on the web visit
https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DjTaw4CD3Lha4fkKFgcYLpypzzDa0J8pPT1eYnZV1qUaQ%40mail.gmail.com.