English
In CatEnrichedOrdinary, composing a vertical 2-cell η with the identity on f yields a morphism equal to the usual composition with identities: hComp (𝟙 (𝟙 a)) η = eqToHom (id_comp f) ≫ η ≫ eqToHom (id_comp f').symm.
Русский
В CatEnrichedOrdinary композиция 2-мерного морфизма η с единицей на f дает обычное сочетание с единицами: hComp (𝟙 (𝟙 a)) η = eqToHom (id_comp f) ≫ η ≫ eqToHom (id_comp f').symm.
LaTeX
$$$hComp(\\mathbf{1}(\\mathbf{1} a), \\eta) = \\mathrm{eqToHom}(\\mathrm{id\\_comp}\n f) \\;\\gg\\; \\eta \\;\\gg\\; \\mathrm{eqToHom}(\\mathrm{id\\_comp}\\, f')^{-1}$$$
Lean4
theorem id_hComp {a b : CatEnrichedOrdinary C} {f f' : a ⟶ b} (η : f ⟶ f') :
hComp (𝟙 (𝟙 a)) η = eqToHom (id_comp f) ≫ η ≫ eqToHom (id_comp f').symm :=
by
ext
simp only [hComp, Hom.base_id, base_mk, ← heq_eq_eq, eqToHom_comp_heq_iff, comp_eqToHom_heq_iff]
rw [homEquiv_id]; simp [CatEnriched.id_hComp_heq]
