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 construction 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 advantages 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 framework and we use it to produce, completely constructively (even predicatively), weak versions of various standard model categories, including the Kan-Quillen model structure, the 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.

80 pages ; Change to v2 : typos corrected and minor improvement. Some numbering have changed

References in corpus (7)

• Higher Topos Theory
• Towards a constructive simplicial model of Univalent Foundations
• The constructive Kan-Quillen model structure: two new proofs
• W-Types with Reductions and the Small Object Argument
• Regular polygraphs and the Simpson conjecture
• Algebraic models of homotopy types and the homotopy hypothesis
• A constructive account of the Kan-Quillen model structure and of Kan's Ex${}^{\infty }$ functor

Cited by in corpus (8)

• Towards a constructive simplicial model of Univalent Foundations
• The Gray tensor product for 2-quasi-categories
• A model 2-category of enriched combinatorial premodel categories
• A constructive account of the Kan-Quillen model structure and of Kan's Ex${}^{\infty }$ functor
• Representable diagrammatic sets as a model of weak higher categories
• Computads for generalised signatures
• The derivator of setoids
• Constructive homotopy theory of marked semisimplicial sets