English
If there exists a homotopy between f0 and f1 relative to S, then there exists a homotopy between f1 and f0 relative to S, obtained by reversing the homotopy in time.
Русский
Если существует гомотопия между f0 и f1 относительно множества S, то существует гомотопия между f1 и f0 относительно S, полученная обращением времени.
LaTeX
$$$\forall X,Y,S, f_0,f_1: C(X,Y),\; F \in \mathrm{HomotopyRel}(f_0,f_1;S) \Rightarrow F^{\mathrm{symm}} \in \mathrm{HomotopyRel}(f_1,f_0;S).$$$
Lean4
/-- Given a `HomotopyRel f₀ f₁ S`, we can define a `HomotopyRel f₁ f₀ S` by reversing the homotopy.
-/
@[simps!]
def symm (F : HomotopyRel f₀ f₁ S) : HomotopyRel f₁ f₀ S
where
toHomotopy := F.toHomotopy.symm
prop' := fun _ _ hx ↦ F.eq_snd _ hx
