English
There is a natural equivalence between arrows X → Y and arrows 𝟙 ⟶ (ihom X).obj Y, given by curry' and uncurry'.
Русский
Существуют естественные биекции между стрелками X → Y и стрелками 𝟙 ⟶ (ihom X).obj Y, задаваемые curry' и uncurry'.
LaTeX
$$$ \\forall X,Y \\; [Closed X],\\ (X \\to Y) \\simeq (\\mathbf{1}_C \\to (\\mathrm{ihom}\\ X).obj Y). $$$
Lean4
/-- Right unitality of the enriched structure -/
@[reassoc (attr := simp)]
theorem comp_id (x y : C) [Closed x] [Closed y] : (ρ_ ((ihom x).obj y)).inv ≫ _ ◁ id y ≫ comp x y y = 𝟙 _ :=
by
apply uncurry_injective
rw [uncurry_natural_left, uncurry_natural_left, comp_eq, uncurry_curry, compTranspose_eq,
associator_inv_naturality_right_assoc, ← rightUnitor_tensor_inv_assoc, whisker_exchange_assoc, ←
rightUnitor_inv_naturality_assoc, ← uncurry_id_eq_ev y y]
simp only [Functor.id_obj]
rw [← uncurry_natural_left]
simp [id_eq, uncurry_id_eq_ev]
