The singular simplicial set functor preserves homotopies

In this file, we define TopCat.Homotopy.toSSet, which shows that if two morphisms f : X ⟶ Y and g : X ⟶ Y in TopCat are homotopic (h : Homotopy f g), then so are their images by the functor TopCat.toSSet : TopCat ⥤ SSet. Indeed, if we apply the singular simplicial set functor to the morphism h.h : X ⊗ I ⟶ Y and use that this functor commutes with products, we obtain a morphism toSSet.obj X ⊗ toSSet.obj I ⟶ toSSet.obj Y: the homotopy toSSet.obj X ⊗ Δ[1] ⟶ toSSet.obj Y is deduced by using the morphism SSet.stdSimplex.toSSetObjI : Δ[1] ⟶ toSSet.obj I, which corresponds to the isomorphism SSet.stdSimplex.toTopObjIsoI|Δ[1]| ≅ TopCat.I by adjunction.

noncomputable def TopCat.Homotopy.toSSet {X Y : TopCat} {f g : X ⟶ Y} (h : Homotopy f g) : SSet.Homotopy (TopCat.toSSet.map f) (TopCat.toSSet.map g)

If two morphisms f : X ⟶ Y and g : X ⟶ Y in TopCat are homotopic, then so are their images by the functor TopCat.toSSet : TopCat ⥤ SSet.