English
The class of trivial cofibrations is closed under retracts, in any setting with weak equivalences and cofibrations having the relevant stability properties.
Русский
Класс тривиальных кофибраций замкнут относительно retracts в обстановке слабых эквивалентностей и кофибраций с соответствующими свойствами устойчивости.
LaTeX
$$$\operatorname{IsStableUnderRetracts}\big(\operatorname{trivialCofibrations}(C)\big)$$$
Lean4
instance [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [(cofibrations C).IsStableUnderRetracts]
[(weakEquivalences C).IsStableUnderRetracts] : (trivialCofibrations C).IsStableUnderRetracts :=
by
dsimp [trivialCofibrations]
infer_instance
