The opposite of a model category structure

instance HomotopicalAlgebra.instHasTwoOutOfThreePropertyOppositeWeakEquivalences (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] [(weakEquivalences C).HasTwoOutOfThreeProperty] : (weakEquivalences Cᵒᵖ).HasTwoOutOfThreeProperty

instance HomotopicalAlgebra.instIsStableUnderRetractsOppositeWeakEquivalences (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] [(weakEquivalences C).IsStableUnderRetracts] : (weakEquivalences Cᵒᵖ).IsStableUnderRetracts

instance HomotopicalAlgebra.instIsStableUnderRetractsOppositeFibrationsOfCofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] [(cofibrations C).IsStableUnderRetracts] : (fibrations Cᵒᵖ).IsStableUnderRetracts

instance HomotopicalAlgebra.instIsStableUnderRetractsOppositeCofibrationsOfFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] [(fibrations C).IsStableUnderRetracts] : (cofibrations Cᵒᵖ).IsStableUnderRetracts

instance HomotopicalAlgebra.instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] [(trivialCofibrations C).HasFactorization (fibrations C)] : (cofibrations Cᵒᵖ).HasFactorization (trivialFibrations Cᵒᵖ)

instance HomotopicalAlgebra.instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] [(cofibrations C).HasFactorization (trivialFibrations C)] : (trivialCofibrations Cᵒᵖ).HasFactorization (fibrations Cᵒᵖ)

@[instance_reducible]

instance HomotopicalAlgebra.instModelCategoryOpposite (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] : ModelCategory Cᵒᵖ

Equations

• One or more equations did not get rendered due to their size.