137 citations · 500 across the 20 of their papers we have counts for
Showing 2012Show all
3 papers · 1 filter
math.LO2012★ 72 cited
The Simplicial Model of Univalent Foundations (after Voevodsky)
Chris Kapulkin, Peter LeFanu Lumsdaine
We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categori…
math.AT2012★ 17 cited
Univalence in Simplicial Sets
Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky
We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations.
math.CT2012★ 10 cited
On the Bourbaki-Witt Principle in Toposes
Andrej Bauer, Peter LeFanu Lumsdaine
The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. W…