English
For V a monoidal category and C a V-enriched ordinary category, there is a bijection homEquiv V between morphisms F1 ⟶ F2 and morphisms 𝟙_V ⟶ enrichedHom V F1 F2; this is natural in all arguments and compatible with composition.
Русский
Для V — моноидальная категория и C — V-обобщенная обычная категория существует биекция homEquiv V между морфизмами F1 ⟶ F2 и морфизмами 𝟙_V ⟶ enrichedHom V F1 F2; она естественна во всех переменных и согласована с композициями.
LaTeX
$$$\\text{homEquiv } V : (F_1 \\to F_2) \\simeq (\\mathbb{1}_V \\to \\mathrm{enrichedHom} V F_1 F_2).$$$
Lean4
@[simp]
theorem natIso_app {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i) (i : Discrete I) :
(Discrete.natIso f).app i = f i := by cat_disch
