English
Given F : p.Homotopy q, define a homotopy p.symm.Homotopy q.symm by precomposing with path symmetry on the second coordinate.
Русский
Пусть F : p.Homotopy q; тогда задаётся гомотопия p.symm.Homotopy q.symm, полученная предварительным преобразованием второй координаты.
LaTeX
$$$\text{For } F : p.Homotopy q,\; F^{\mathrm{symm}_2} : p.symm.Homotopy q.symm$$$
Lean4
/-- Suppose `F : Homotopy p q`. Then we have a `Homotopy p.symm q.symm` by reversing the second
argument.
-/
@[simps]
def symm₂ {p q : Path x₀ x₁} (F : p.Homotopy q) : p.symm.Homotopy q.symm
where
toFun x := F ⟨x.1, σ x.2⟩
map_zero_left := by simp [Path.symm]
map_one_left := by simp [Path.symm]
prop' t x
hx := by
rcases hx with hx | hx
· rw [hx]
simp
· rw [Set.mem_singleton_iff] at hx
rw [hx]
simp
