72 citations · 159 across the 26 of their papers we have counts for
Showing 2017Show all
2 papers · 1 filter
math.LO2017★ 4 cited
Categorical structures for type theory in univalent foundations
Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categori…
math.CT2017★ 5 cited
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…