English
The map induced by the right projection agrees with the canonical path-quotient construction.
Русский
Отображение, индуцируемое правым проецированием, совпадает с каноническим путево-гомотопическим построением.
LaTeX
$$$$ (projRight A B).map p = Path.Homotopic.projRight p $$$$
Lean4
/-- Proof that `H.evalAt x = H(0 ⟶ 1, x ⟶ x)`, with the appropriate casts -/
theorem evalAt_eq (x : X) :
⟦H.evalAt x⟧ =
hcast (H.apply_zero x).symm ≫
(πₘ (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x))) ≫
hcast (H.apply_one x).symm.symm :=
by
dsimp only [prodToProdTopI, uhpath01, hcast]
refine (@conj_eqToHom_iff_heq (πₓ Y) _ _ _ _ _ _ _ _ (FundamentalGroupoid.ext <| H.apply_one x).symm).mpr ?_
simp only [map_eq]
apply Path.Homotopic.hpath_hext; intro;
rfl
-- Finally, we show `d = f(p) ≫ H₁ = H₀ ≫ g(p)`
