English
Casting a Homotopy F : p0.Homotopy p1 to q0.q1 along equalities p0 = q0 and p1 = q1 yields a Homotopy q0.Homotopy q1.
Русский
Препространение гомотопии F : p0.Homotopy p1 вдоль равенств p0 = q0 и p1 = q1 даёт гомотопию q0.Homotopy q1.
LaTeX
$$$\forall {p_0 p_1 q_0 q_1 : Path x_0 x_1} \; (F : p_0.Homotopy p_1) \; (h_0 : p_0 = q_0) (h_1 : p_1 = q_1) \Rightarrow q_0.Homotopy q_1$$$
Lean4
/-- Casting a `Homotopy p₀ p₁` to a `Homotopy q₀ q₁` where `p₀ = q₀` and `p₁ = q₁`. -/
@[simps!]
def cast {p₀ p₁ q₀ q₁ : Path x₀ x₁} (F : Homotopy p₀ p₁) (h₀ : p₀ = q₀) (h₁ : p₁ = q₁) : Homotopy q₀ q₁ :=
ContinuousMap.HomotopyRel.cast F (congr_arg _ h₀) (congr_arg _ h₁)
