English
A homotopy between (n+1)-dimensional loops p and q, constant on the boundary, induces a homotopy between two paths in the space of n-dimensional paths.
Русский
Гомотопия между (n+1)-мерными петлями p и q, константная на границе, индуцирует гомотопию между двумя путями в пространстве n-мерных путей.
LaTeX
$$GenLoop.homotopyTo(i) : (p,q) → C(I × I, C(I^{j//j≠i},X))$$
Lean4
/-- Loop from a generalized loop by currying $I^N → X$ into $I → (I^{N\setminus\{j\}} → X)$. -/
@[simps]
def toLoop (i : N) (p : Ω^ N X x) : Ω (Ω^ { j // j ≠ i } X x) const
where
toFun
t :=
⟨(p.val.comp (Cube.insertAt i)).curry t, fun y yH =>
p.property (Cube.insertAt i (t, y)) (Cube.insertAt_boundary i <| Or.inr yH)⟩
source' := by ext t; refine p.property (Cube.insertAt i (0, t)) ⟨i, Or.inl ?_⟩; simp
target' := by ext t; refine p.property (Cube.insertAt i (1, t)) ⟨i, Or.inr ?_⟩; simp
