Weak model categories in classical and constructive mathematics

Simon Henry

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 factorization 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, including 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.

Keywords: Model categories, constructive mathematics, simplicial sets, semi-simplicial sets, complicial sets

2020 MSC: 55U35, 55U40, 18N40, 18N50, 18N65

Theory and Applications of Categories, Vol. 35, 2020, No. 24, pp 875-958.

Published 2020-06-12.

http://www.tac.mta.ca/tac/volumes/35/24/35-24.pdf

TAC Home