English
If cofibrations and trivial fibrations form a weak factorization system, then the coproduct map coprod.map f1 f2 is a cofibration.
Русский
Если кофибрации и тривиальные фибрации образуют слабую факторизационную систему, тогда coprod.map f1 f2 — кофибрация.
LaTeX
$$$[IsWeakFactorizationSystem(\\mathrm{cofibrations}(C)) (\\mathrm{trivialFibrations}(C))] [\\mathrm{Cofibration}(f_1)] [\\mathrm{Cofibration}(f_2)] : \\mathrm{Cofibration}(\\mathrm{coprod.map} f_1 f_2).$$$
Lean4
instance [IsWeakFactorizationSystem (cofibrations C) (trivialFibrations C)] [h₁ : Cofibration f₁] [h₂ : Cofibration f₂]
[HasBinaryCoproduct X₁ X₂] [HasBinaryCoproduct Y₁ Y₂] : Cofibration (coprod.map f₁ f₂) :=
by
rw [cofibration_iff] at h₁ h₂ ⊢
apply MorphismProperty.colimMap
rintro (_ | _) <;> assumption
