Weak model categories in classical and constructive mathematics

Abstract

We introduce a notion of “weak model category” which is a weakening of the notion of Quillen model category, still sufficient to define a homotopy category, Quillen adjunctions, Quillen equivalences, and most of the usual constructions of categorical homotopy theory. Both left and right semi-model categories are weak model categories, and the opposite of a weak model category is again a weak model category. The main advantage of weak model categories is that they are easier to construct than Quillen model categories. In particular we give some simple criteria on two weak factor-ization systems for them to form a weak model category. The theory is developed in a very weak constructive, even predicative, framework and we use it to give constructive proofs of the existence of weak versions of various standard model categories, includ-ing the Kan–Quillen model structure, Lurie’s variant of the Joyal model structure on marked simplicial sets, and the Verity model structure for weak complicial sets. We also construct semi-simplicial versions of all these.