Model categories #
We introduce a typeclass ModelCategory C expressing that C is equipped with
classes of morphisms named "fibrations", "cofibrations" and "weak equivalences"
with satisfy the axioms of (closed) model categories.
As a given category C may have several model category structures, it is advisable
to define only local instances of ModelCategory, or to set these instances on type synonyms.
References #
- [Daniel G. Quillen, Homotopical algebra][Quillen1967]
- Paul G. Goerss, John F. Jardine, Simplicial Homotopy Theory
class
HomotopicalAlgebra.ModelCategory
(C : Type u)
[CategoryTheory.Category.{v, u} C]
:
Type (max u v)
A model category is a category equipped with classes of morphisms named cofibrations, fibrations and weak equivalences which satisfies the axioms CM1/CM2/CM3/CM4/CM5 of (closed) model categories.
- categoryWithFibrations : CategoryWithFibrations C
- categoryWithCofibrations : CategoryWithCofibrations C
- categoryWithWeakEquivalences : CategoryWithWeakEquivalences C
- cm2 : (weakEquivalences C).HasTwoOutOfThreeProperty
- cm3a : (weakEquivalences C).IsStableUnderRetracts
- cm3b : (fibrations C).IsStableUnderRetracts
- cm3c : (cofibrations C).IsStableUnderRetracts
- cm4a {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p] : CategoryTheory.HasLiftingProperty i p
- cm4b {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [Fibration p] [WeakEquivalence p] : CategoryTheory.HasLiftingProperty i p
- cm5a : (trivialCofibrations C).HasFactorization (fibrations C)
- cm5b : (cofibrations C).HasFactorization (trivialFibrations C)