English
If you have a relative homotopy F: HomotopyRel f0 f1 S and equalities f0=g0, f1=g1, you can transport F to a relative homotopy between g0 and g1.
Русский
Имея относительную гомотопию F: HomotopyRel f0 f1 S и равенства f0=g0, f1=g1, можно перенести F к относительной гомотопии между g0 и g1.
LaTeX
$$$F : \mathrm{HomotopyRel}(f_0,f_1;S),\ h_0: f_0=g_0,\ h_1: f_1=g_1 \Rightarrow F.cast\,h_0\,h_1 : \mathrm{HomotopyRel}(g_0,g_1;S).$$$
Lean4
/-- Casting a `HomotopyRel f₀ f₁ S` to a `HomotopyRel g₀ g₁ S` where `f₀ = g₀` and `f₁ = g₁`.
-/
@[simps!]
def cast {f₀ f₁ g₀ g₁ : C(X, Y)} (F : HomotopyRel f₀ f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) : HomotopyRel g₀ g₁ S
where
toHomotopy := Homotopy.cast F.toHomotopy h₀ h₁
prop' t x hx := by simpa only [← h₀, ← h₁] using F.prop t x hx
