English
Horizontal composition is associative with respect to vertical composition in CatEnrichedOrdinary: hComp (hComp η θ) κ equals hComp η (hComp θ κ) up to the associator.
Русский
Горизонтальная композиция ассоциируется по отношению к вертикальной композиции в CatEnrichedOrdinary: hComp (hComp η θ) κ = hComp η (hComp θ κ) через ассоциатор.
LaTeX
$$$hComp( hComp(\\eta, \\theta), \\kappa) = \\mathrm{eqToHom}(\\mathrm{assoc}(f,g,h)) ≫ hComp(\\eta, hComp(\\theta, \\kappa)) ≫ eqToHom(assoc...)^{−1}$$$
Lean4
theorem hComp_assoc {a b c d : CatEnrichedOrdinary C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f')
(θ : g ⟶ g') (κ : h ⟶ h') :
hComp (hComp η θ) κ = eqToHom (assoc f g h) ≫ hComp η (hComp θ κ) ≫ eqToHom (assoc f' g' h').symm :=
by
ext
simp only [hComp, base_mk, Hom.base_comp, Hom.base_eqToHom, ← heq_eq_eq, heq_eqToHom_comp_iff, heq_comp_eqToHom_iff,
eqToHom_comp_heq_iff, comp_eqToHom_heq_iff]
conv => enter [1, 2]; exact ((id_comp _).trans (comp_id _)).symm
conv => enter [2, 1]; exact ((id_comp _).trans (comp_id _)).symm
iterate 4 rw [← CatEnriched.hComp_comp, id_eq_eqToHom, CatEnriched.eqToHom_hComp_eqToHom]
simp [CatEnriched.hComp_assoc_heq]
