Mathlib SSet: homotopies are edges of the internal hom

To prove facts about SSet.Homotopy f g (a map X ⊗ Δ[1] ⟶ Y), curry it: MonoidalClosed.curry H.h : Δ[1] ⟶ (ihom X).obj Y, and yonedaEquiv of that is an Edge from yonedaEquiv (curry (fst X Δ[0] ≫ f)) to the same for g. The face proofs go through δ_yonedaEquiv (Z.δ i (yonedaEquiv φ) = yonedaEquiv (stdSimplex.δ i ≫ φ), by φ.naturality), ← curry_natural_left, and X ◁ stdSimplex.δ 1 = fst X Δ[0] ≫ ι₀. That last one is proved by CartesianMonoidalCategory.hom_ext with whiskerLeft_snd, Mathlib's stdSimplex.δ_one_eq_const and comp_const. For the converse, ι₀ = lift (𝟙 X) (isTerminalObj₀.from X) ≫ fst ≫ ι₀, then uncurry_natural_left. The rel field for bot subcomplexes: ext _ ⟨⟨_, h⟩, _⟩; simp at h. Mathlib already has KanComplex ((ihom A).obj X), so symmetry and transitivity of homotopy into a Kan complex come from edges in a Kan complex.