English
If h is a RightHomotopyRel between f and g, then there exists a LeftHomotopyRel f g obtained by choosing a suitable cylinder on X.
Русский
Если h является RightHomotopyRel между f и g, то существует LeftHomotopyRel f g, получаемый выбором подходящего цилиндра на X.
LaTeX
$$$\text{RightHomotopyRel}(f,g) \Rightarrow \text{LeftHomotopyRel}(f,g)$$$
Lean4
/-- When two morphisms `X ⟶ Y` with `Y` fibrant are related by a right homotopy,
this is a choice of a left homotopy relative to any good cylinder object for `X`. -/
noncomputable def leftHomotopy (h : RightHomotopyRel f g) (Q : Cylinder X) [Q.IsGood] : Q.LeftHomotopy f g :=
let P := h.exists_good_pathObject.choose
have h := h.exists_good_pathObject.choose_spec.2.some
have h' := h.exists_good_pathObject.choose_spec.1
have sq : CommSq (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f) := { }
{ h := sq.lift ≫ P.p₁
h₀ := by
have := coprod.inl ≫= sq.fac_left
rw [Q.inl_i_assoc, coprod.inl_desc] at this
simp [reassoc_of% this]
h₁ := by
have := coprod.inr ≫= sq.fac_left
rw [Q.inr_i_assoc, coprod.inr_desc] at this
simp [reassoc_of% this, P] }
