English
The functor enriched identities compose correctly with enrichment: the left unitor compatibility holds with enrichedId and functorEnrichedComp.
Русский
Обогащённая идентичность компонуется корректно с обогащением: совместимость с левой единичной существующей единицей и enrichedComp.
LaTeX
$$$\\rho_{(\\mathrm{functorEnrichedHom}(V,F_1,F_2))}^{-1} \\circ (\\mathrm{functorEnrichedId}(V,F_1) \\triangleright \\mathrm{functorEnrichedHom}(V,F_1,F_2)) \\circ \\mathrm{functorEnrichedComp}(V,F_1,F_1,F_2) = \\mathrm{id}$$$
Lean4
@[reassoc]
theorem functorEnriched_assoc [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₂ F₃]
[HasFunctorEnrichedHom V F₃ F₄] [HasFunctorEnrichedHom V F₁ F₃] [HasFunctorEnrichedHom V F₂ F₄]
[HasFunctorEnrichedHom V F₁ F₄] :
(α_ _ _ _).inv ≫ functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄ ≫ functorEnrichedComp V F₁ F₃ F₄ =
functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄ ≫ functorEnrichedComp V F₁ F₂ F₄ :=
by
ext j
dsimp
rw [enriched_assoc]
