English
There is a canonical equivalence between morphisms X ⟶ Y and arrows 𝟙 ⟶ (ihom X).obj Y, given by curry' and uncurry'.
Русский
Существуют каноническое эквивалентность между морфизмами X ⟶ Y и стрелками 𝟙 ⟶ (ihom X).obj Y, задаваемая curry' и uncurry'.
LaTeX
$$$ {X Y : C} [Closed X] : (X \\to Y) \\simeq (\\mathbf{1}_C \\to (\\mathrm{ihom} X).obj Y). $$$
Lean4
@[reassoc]
theorem curry'_whiskerRight_comp {X Y Z : C} [Closed X] [Closed Y] (f : X ⟶ Y) :
curry' f ▷ _ ≫ comp X Y Z = (λ_ _).hom ≫ (pre f).app Z :=
by
rw [← cancel_epi (λ_ _).inv, Iso.inv_hom_id_assoc]
apply uncurry_injective
rw [uncurry_pre, comp_eq, ← curry_natural_left, ← curry_natural_left, uncurry_curry, compTranspose_eq,
associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, whiskerLeft_curry'_ihom_ev_app,
comp_whiskerRight_assoc, triangle_assoc_comp_right_assoc, whiskerLeft_inv_hom_assoc]
