English
Let F be a homotopy between f0 and f1 and G be a homotopy between g0 and g1. Then F.prodMk G is a homotopy between f0.prodMk g0 and f1.prodMk g1, acting pointwise by (F p, G p).
Русский
Пусть F — гомотопия между f0 и f1, и G — гомотопия между g0 и g1. Тогда F.prodMk G — гомотопия между f0.prodMk g0 и f1.prodMk g1, действующая по точкам как (F p, G p).
LaTeX
$$$$ F : f_0 \sim f_1 , \ G : g_0 \sim g_1 \Rightarrow F.ProdMk G : (f_0 \prodMk g_0) \sim (f_1 \prodMk g_1) $$$$
Lean4
/-- If we have a `Homotopy f₀ f₁` and a `Homotopy g₀ g₁`, then we can compose them and get a
`Homotopy (g₀.comp f₀) (g₁.comp f₁)`.
-/
@[simps!, deprecated comp (since := "2025-05-12")]
def hcomp {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Y, Z)} (F : Homotopy f₀ f₁) (G : Homotopy g₀ g₁) :
Homotopy (g₀.comp f₀) (g₁.comp f₁) :=
G.comp F
