72 citations · 159 across the 26 of their papers we have counts for
5 papers · 1 filter
Algebraic Presentations of Type Dependency
Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North +1
C-systems were defined by Cartmell as the algebraic structures that correspond exactly to generalised algebraic theories. B-systems were defined by Voevodsky in his quest to formul…
The Univalence Principle
Benedikt Ahrens, Paige Randall North, Michael Shulman +1
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based,…
Bicategories in Univalent Foundations
Benedikt Ahrens, Dan Frumin, Marco Maggesi +2
We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent…
Displayed Categories
Benedikt Ahrens, Peter LeFanu Lumsdaine
We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but instead of having…
Univalent categories and the Rezk completion
Benedikt Ahrens, Chris Kapulkin, Michael Shulman
We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this syst…