English
Equality of lifts is equivalent to equality of the lifted homotopy and the base homotopy data; i.e., lifting is determined by p and the lift of H_0.
Русский
Равенство подъёмов эквивалентно равенству подъемной гомотопии и базовых данных гомотопии; подъём задано через p и подъём H_0.
LaTeX
$$$$\Gamma = cov.liftHomotopy(H,f,H_0) \iff (p \circ \Gamma = H) \land (\forall a, \Gamma(0,a)=f(a)).$$$$
Lean4
theorem eq_liftHomotopy_iff (H' : I × A → E) :
H' = cov.liftHomotopy H f H_0 ↔ (∀ a, Continuous (H' ⟨·, a⟩)) ∧ p ∘ H' = H ∧ ∀ a, H' (0, a) = f a :=
by
refine ⟨?_, fun ⟨H'_cont, H'_lifts, H'_0⟩ ↦ funext fun ⟨t, a⟩ ↦ ?_⟩
· rintro rfl; refine ⟨fun a ↦ ?_, cov.liftHomotopy_lifts H f H_0, cov.liftHomotopy_zero H f H_0⟩
simp_rw [liftHomotopy_apply]; exact (cov.liftPath _ _ <| H_0 a).2
· apply congr_fun ((cov.eq_liftPath_iff _).mpr ⟨H'_cont a, _, H'_0 a⟩) t
ext ⟨t, a⟩; exact congr_fun H'_lifts _
