English
If trivial cofibrations and fibrations form a weak factorization system and weak equivalences are stable under retracts, then any isomorphism is a weak equivalence.
Русский
Если тривиальные кофибрации и фибрации образуют слабую факторизационную систему, а слабые эквивалентности устойчивы к ретракциям, то любой изоморфизм является слабой эквивалентностью.
LaTeX
$$$\forall f,\ \mathrm{IsIso}(f) \Rightarrow \mathrm{WeakEquivalence}(f)$$$
Lean4
instance [IsWeakFactorizationSystem (trivialCofibrations C) (fibrations C)] [(weakEquivalences C).IsStableUnderRetracts]
[IsIso f] : WeakEquivalence f :=
by
have h := MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) f
rw [weakEquivalence_iff]
exact MorphismProperty.of_retract (RetractArrow.ofLeftLiftingProperty h.fac) h.hi.2
