English
In a setting where cofibrations and trivial fibrations form a weak factorization system, every isomorphism is a fibration.
Русский
В системе, где кофибрации и тривиальные фибрации образуют слабую факторизационную систему, любая изоморфная стрелка является фибрацией.
LaTeX
$$$\forall X,Y\,(f:X\to Y),\, \mathrm{IsIso}(f) \Rightarrow \mathrm{Fibration}(f)$$$
Lean4
instance [IsWeakFactorizationSystem (cofibrations C) (trivialFibrations C)] [IsIso f] : Fibration f :=
by
have := (cofibrations C).rlp_of_isIso f
rw [cofibrations_rlp] at this
simpa only [fibration_iff] using this.1
