English
In any model category C, the pair of trivial cofibrations and fibrations forms a Weak Factorization System.
Русский
В любой модельной категории C пара тривиальные кофибрации и фибрации образует слабую факторизационную систему.
LaTeX
$$$\operatorname{IsWeakFactorizationSystem}(\operatorname{trivialCofibrations} C, \operatorname{fibrations} C)$$$
Lean4
instance : MorphismProperty.IsWeakFactorizationSystem (trivialCofibrations C) (fibrations C) :=
MorphismProperty.IsWeakFactorizationSystem.mk' _ _
(fun {A B X Y} i p hi hp ↦ by
obtain ⟨_, _⟩ := mem_trivialCofibrations_iff i |>.mp hi
rw [← fibration_iff] at hp
infer_instance)
