147 citations · 398 across the 15 of their papers we have counts for
Showing 2019Show all
3 papers · 1 filter
math.AT2019★ 11 cited
The constructive Kan-Quillen model structure: two new proofs
Nicola Gambino, Christian Sattler, Karol Szumiło
We present two new proofs of Simon Henry's result that the category of simplicial sets admits a constructive counterpart of the classical Kan-Quillen model structure. Our proofs ar…
math.CT2019★ 8 cited
Models of Martin-Löf type theory from algebraic weak factorisation systems
Nicola Gambino, Marco Federico Larrea
We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Löf type theory. This is done by showing that th…
math.CT2019★ 15 cited
Towards a constructive simplicial model of Univalent Foundations
Nicola Gambino, Simon Henry
We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of univalent foundations. For this, we prove constructive counterpar…