From Possible Worlds to Homotopy - 
Kripke models were invented as a way of understanding non-standard systems of logic, essentially by interpreting them as standard logic varying in a parameter. The parameter can be understood as time (temporal logic), space (intuitionistic logic), or more colorfully “possible worlds” (modal logic). The same idea can be extended from the simple propositional logic of Boolean algebra to the very expressive systems of type theory on which modern computer proof systems are based.  A “Kripke model” of type theory varying over, say, the simplex category Δ from algebraic topology actually gives something familiar: namely the standard model of homotopy theory.