Recent joint work [1] with Nicola Gambino and Sina Hazratpour is presented.  Kripke-Joyal semantics extends the basic Kripke semantics for intuitionistic propositional logic (IPL) and first-order logic (IFOL) to the higher-order logic used in topos theory (IHOL).  It provides a systematic way to interpret propositions of IHOL into any Grothendieck topos and to test them for validity under the interpretation.  We extend the interpretation to the dependent type theory of Martin-Löf (MLTT), using the formalism of natural models [2].  A Kripke completeness theorem for MLTT is also given.  Prior cases of presheaf semantics for MLTT are subsumed, including the presheaf models of homotopy type theory (HoTT) of Voevodsky et al. and Coquand et al. 

[1] Steve Awodey, Nicola Gambino, Sina Hazratpour, Kripke-Joyal forcing for type theory and uniform fibrations, arXiv:2110.14576, 2021.

[2] Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer Science, pp. 241–286, 2016.