- document
-
Ahrens, B.P. (author), Emmenegger, Jacopo (author), North, Paige Randall (author), Rijke, Egbert (author)C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky's construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between...journal article 2023
- document
-
Ahrens, B.P. (author), North, Paige Randall (author), van der Weide, Niels (author)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. From comprehension bicategories, we extract a core syntax, that is, judgment forms and...conference paper 2022