English
If f0 is left-homotopic to f1 via P and f1 is left-homotopic to f2 via P', then f0 is left-homotopic to f2 via P.trans P', assuming X is cofibrant.
Русский
Если f0 гомотопно эквивалентен f1 через P, а f1 через P' к f2, то существует левая гомотопия между f0 и f2 через P.trans P' при условии, что X кофибривант.
LaTeX
$$$\text{LeftHomotopy}(f_0,f_2)\;\text{exists via } (P\trans P')$$$
Lean4
/-- If `f₀ : X ⟶ Y` is homotopic to `f₁` relative to a cylinder `P`,
and `f₁` is homotopic to `f₂` relative to a good cylinder `P'`,
then `f₀` is homotopic to `f₂` relative to the cylinder `P.trans P'`
when `X` is cofibrant. -/
noncomputable abbrev trans [IsCofibrant X] {f₀ f₁ f₂ : X ⟶ Y} (h : P.LeftHomotopy f₀ f₁) {P' : Cylinder X} [P'.IsGood]
(h' : P'.LeftHomotopy f₁ f₂) [HasPushout P.i₁ P'.i₀] : (P.trans P').LeftHomotopy f₀ f₂ :=
Precylinder.LeftHomotopy.trans h h'
