English
Let Z be fibrant and f: X → Y a cofibration and weak equivalence; the map g ↦ g.precomp f gives a bijection on RightHomotopyClass(Y,Z) → RightHomotopyClass(X,Z).
Русский
Пусть Z фибривант и f: X→Y — кофибрация и слабая эквивалентность; отображение g ↦ g.precomp f образует биекцию между RightHomotopyClass(Y,Z) и RightHomotopyClass(X,Z).
LaTeX
$$$\operatorname{Bij}\Big( \lambda g\in \operatorname{RightHo}(Y,Z),\; g\circ f\Big)$$$
Lean4
instance [CategoryWithWeakEquivalences C] [(weakEquivalences C).IsStableUnderComposition] [hf : WeakEquivalence f]
[hg : WeakEquivalence g] : WeakEquivalence (f ≫ g) :=
(weakEquivalence_iff _).2 ((weakEquivalences C).comp_mem _ _ hf.mem hg.mem)
