English
The inverse relation matches the symmetric At version: fromLoop i (toLoop i p).symm = symmAt i p.
Русский
Обратность соответствует симметрической версии: fromLoop i (toLoop i p).symm = symmAt i p.
LaTeX
$$$\\mathrm{fromLoop}(i)(\\mathrm{toLoop}(i) p)^{\\mathrm{symm}} = \\mathrm{symmAt}(i,p)$$$
Lean4
/-- The 1-dimensional generalized loops based at `x` are in bijection with loops at `x`. -/
def genLoopEquivOfUnique (N) [Unique N] : Ω^ N X x ≃ Ω X x
where
toFun
p :=
Path.mk ⟨fun t => p fun _ => t, by continuity⟩ (GenLoop.boundary _ (fun _ => 0) ⟨default, Or.inl rfl⟩)
(GenLoop.boundary _ (fun _ => 1) ⟨default, Or.inr rfl⟩)
invFun
p :=
⟨⟨fun c => p (c default), by continuity⟩,
by
rintro y ⟨i, iH | iH⟩ <;> cases Unique.eq_default i <;> apply (congr_arg p iH).trans
exacts [p.source, p.target]⟩
left_inv p := by ext y; exact congr_arg p (eq_const_of_unique y).symm
