English
Under the assumptions that trivial cofibrations and fibrations form a weak factorization system and weak equivalences are stable under retracts and composition, the class of weak equivalences is multiplicative (closed under composition and contains identities).
Русский
При предположениях, что тривиальные кофибрации и фибрации образуют слабую факторизационную систему, а слабые эквивалентности устойчивы к ретракциям и под композицию, множество слабых эквивалентностей замыкается при композиции и содержит тождественные стрелки.
LaTeX
$$$(\text{weakEquivalences } C).IsMultiplicative$$$
Lean4
instance [IsWeakFactorizationSystem (trivialCofibrations C) (fibrations C)] [(weakEquivalences C).IsStableUnderRetracts]
[(weakEquivalences C).IsStableUnderComposition] : (weakEquivalences C).IsMultiplicative where
id_mem
_ := by
rw [← weakEquivalence_iff]
infer_instance
