English
If fibrations satisfy a weak factorization system with trivial cofibrations, then the product map prod.map f1 f2 is a fibration.
Русский
Если фибрации удовлетворяют слабой факторизационной системе с тривиальными кофибрациями, то prod.map f1 f2 — фибрация.
LaTeX
$$$[IsWeakFactorizationSystem(\\mathrm{trivialCofibrations}(C)) (\\mathrm{fibrations}(C))] [\\mathrm{Fibration}(\\mathrm{prod.map} f_1 f_2)].$$$
Lean4
instance [IsWeakFactorizationSystem (trivialCofibrations C) (fibrations C)] [h₁ : Fibration f₁] [h₂ : Fibration f₂]
[HasBinaryProduct X₁ X₂] [HasBinaryProduct Y₁ Y₂] : Fibration (prod.map f₁ f₂) :=
by
rw [fibration_iff] at h₁ h₂ ⊢
apply MorphismProperty.limMap
rintro (_ | _) <;> assumption
