English
In a monoidal closed category with X, Y closed, for f: X → Y and g: Y → Z, the currying of the composite f ≫ g equals the left unitor inverse composed with the tensor of the curries of f and g followed by the evaluation map.
Русский
В замкнутой моноидальной категории, если X и Y замкнуты и есть стрелы f: X → Y, g: Y → Z, то curry'(f ≫ g) = λ^{-1} ∘ (curry'(f) ⊗ curry'(g)) ∘ comp_{X,Y,Z}.
LaTeX
$$$ curry'(f \circ g) = (\lambda_{\mathbf{1}_C})^{-1} \circ (curry'(f) \otimes Curry'(g)) \circ comp_{X Y Z} $$$
Lean4
theorem curry'_comp {X Y Z : C} [Closed X] [Closed Y] (f : X ⟶ Y) (g : Y ⟶ Z) :
curry' (f ≫ g) = (λ_ (𝟙_ C)).inv ≫ (curry' f ⊗ₘ curry' g) ≫ comp X Y Z := by
rw [tensorHom_def_assoc, whiskerLeft_curry'_comp, MonoidalCategory.whiskerRight_id, Category.assoc, Category.assoc,
Iso.inv_hom_id_assoc, ← unitors_equal, Iso.inv_hom_id_assoc, curry'_ihom_map]
