English
If H is a homotopy between boundary-fixed loops p and q, then the associated homotopy between their toLoop images is given by homotopyTo i H.
Русский
Если H — гомотопия между петлями p и q фиксированными на границе, то соответствующая гомотопия между их образами через toLoop задаётся как homotopyTo i H.
LaTeX
$$homotopyTo(i,H) : C(I × I, C(I^{ j // j ≠ i }, X))$$
Lean4
/-- A homotopy between `n+1`-dimensional loops `p` and `q` constant on the boundary
seen as a homotopy between two paths in the space of `n`-dimensional paths. -/
def homotopyTo (i : N) {p q : Ω^ N X x} (H : p.1.HomotopyRel q.1 (Cube.boundary N)) :
C(I × I, C(I^{ j // j ≠ i }, X)) :=
((⟨_, ContinuousMap.continuous_curry⟩ : C(_, _)).comp <| (cCompInsert i).comp H.toContinuousMap.curry).uncurry
