The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond.

翻译：模态逻辑的研究在克里普克语义引入后取得了巨大发展。然而，编程语言与类型论的最新进展催生了模态研究的第二条路径，即通过范畴语义进行研究。本文展示了两者之间的对应关系。