Semantics for two-dimensional type theory
Benedikt Ahrens, Paige Randall North, Niels van der Weide · 2022
We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature.