English
The homEquiv respects composition: the homEquiv of f ≫ g equals the unit-adjusted tensor of homEquiv f and homEquiv g composed with enrichedComp.
Русский
Гомэквивалентность сохраняет композицию: homEquiv(f ∘ g) равен единичному одновременному преобразованию левого унитора умноженному на tensor и на EnrichedComp.
LaTeX
$$$\\mathrm{homEquiv}_V(f \\circ g) = (\\lambda_{\\mathbb{1}_V})^{-1} \\circ (\\mathrm{homEquiv}_V f \\otimes \\mathrm{homEquiv}_V g) \\circ \\mathrm{enrichedComp}_V(F_1,F_2,F_3)$$$
Lean4
@[reassoc (attr := simp)]
theorem enriched_comp_id [HasEnrichedHom V F₁ F₂] [HasEnrichedHom V F₂ F₂] :
(ρ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedHom V F₁ F₂ ◁ enrichedId V F₂ ≫ enrichedComp V F₁ F₂ F₂ = 𝟙 _ :=
by
ext j
rw [assoc, assoc, enrichedComp_π, id_comp, tensorHom_def', assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
enrichedId_π, whisker_exchange_assoc, MonoidalCategory.whiskerRight_id, assoc, assoc, Iso.inv_hom_id_assoc]
dsimp
rw [e_comp_id, comp_id]
