The constructive Kan-Quillen model structure: two new proofs

Abstract

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 are entirely self-contained and avoid complex combinatorial arguments on anodyne extensions. We also give new constructive proofs of the left and right properness of the model structure.

Revised version, 52 pages. Minor improvements in exposition. New statements Lemma 1.1.1 and Lemma 1.2.1. Accepted for publication in Quarterly Journal of Mathematics