3 results
Peter LeFanu Lumsdaine.
We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the […]
Published on September 17, 2010
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-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them […]
Published on September 11, 2018
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 a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by […]
Published on March 5, 2019