∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {P : C(X, Y) → Prop}
  {f₀ f₁ g₀ g₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X),
  (F.cast h₀ h₁) a = F a