137 citations · 500 across the 20 of their papers we have counts for
4 papers · 1 filter
Semantics of higher inductive types
Peter LeFanu Lumsdaine, Mike Shulman
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have prove…
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…
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…
Parametricity, automorphisms of the universe, and excluded middle
Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine +1
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assumin…