THE SIMPLICIAL MODEL OF UNIVALENT FOUNDATIONS

131 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

An experimental library of formalized Mathematics based on the univalent foundations (2015, background): “I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).”
Univalent categories and the Rezk completion (2013, methodology): “Using this interpretation, Voevodsky has extended dependent type theory with an additional axiom, called the Univalence Axiom, which was originally suggested by the model of the theory in the category of simplicial sets [11], and should also be valid in other homotopical models such as categories of”
The Frobenius condition, right properness, and uniform fibrations (2015, methodology): “of our results, we solve an open problem in the univalent foundations programme, namely that of proving a constructive version of the fact that pushforward along Kan ﬁbrations preserves Kan ﬁbrations [9, 28]. We also obtain a new proof of the right properness of the Quillen model structure for Kan c”