Lean4
/-- Constructor for `ModelCategory C` which assumes a formulation of axioms
using weak factorizations systems. -/
def mk' [CategoryWithFibrations C] [CategoryWithCofibrations C] [CategoryWithWeakEquivalences C] [HasFiniteLimits C]
[HasFiniteColimits C] [(weakEquivalences C).HasTwoOutOfThreeProperty]
[IsWeakFactorizationSystem (cofibrations C) (trivialFibrations C)]
[IsWeakFactorizationSystem (trivialCofibrations C) (fibrations C)] : ModelCategory C
where
cm3a :=
⟨fun {A B X Y f w h hw} ↦ by
rw [← weakEquivalence_iff] at hw
have hf := factorizationData (trivialCofibrations C) (fibrations C) f
have : Cofibration hf.i := by simpa only [cofibration_iff] using hf.hi.1
have : WeakEquivalence hf.i := by simpa only [weakEquivalence_iff] using hf.hi.2
let φ : pushout hf.i h.i.left ⟶ Y := pushout.desc (hf.p ≫ h.i.right) w (by simp)
have : Fibration hf.p := by simpa only [fibration_iff] using hf.hp
have : WeakEquivalence (pushout.inr _ _ ≫ φ) := by simpa [φ]
have := weakEquivalence_of_precomp (pushout.inr _ _) φ
have hp : RetractArrow hf.p φ :=
{ i := Arrow.homMk (pushout.inl _ _) h.i.right
r := Arrow.homMk (pushout.desc (𝟙 _) (h.r.left ≫ hf.i) (by simp)) h.r.right }
have := mk'.cm3a_aux hp
rw [← weakEquivalence_iff, ← hf.fac]
infer_instance⟩
cm3b := by
rw [← rlp_eq_of_wfs (trivialCofibrations C) (fibrations C)]
infer_instance
cm3c := by
rw [← llp_eq_of_wfs (cofibrations C) (trivialFibrations C)]
infer_instance
cm4a i p _ _ _ := hasLiftingProperty_of_wfs i p (mem_trivialCofibrations i) (mem_fibrations p)
cm4b i p _ _ _ := hasLiftingProperty_of_wfs i p (mem_cofibrations i) (mem_trivialFibrations p)
