English
A compatibility result for curry' with whiskering on the right by Pre and MonoidalClosed structures; it expresses equality of two ways of composing curry' with a map.
Русский
Совместимость curry' с правым развёртыванием через Pre и моноидальные структуры; выражает равенство двух способов композиции curry' с отображением.
LaTeX
$$$ \\forall {X Y Z : C} [Closed X] [Closed Y] (f : X \\to Y) :\\n curry' f \\; \\triangleright _ \\; \\circ\\; comp X Y Z = (\\lambda_\\,\\_).hom \\circ (\\mathrm{pre} f).app Z. $$$
Lean4
@[reassoc]
theorem whiskerLeft_curry'_comp {X Y Z : C} [Closed X] [Closed Y] (f : Y ⟶ Z) :
_ ◁ curry' f ≫ comp X Y Z = (ρ_ _).hom ≫ (ihom X).map f :=
by
rw [← cancel_epi (ρ_ _).inv, Iso.inv_hom_id_assoc]
apply uncurry_injective
rw [uncurry_ihom_map, comp_eq, ← curry_natural_left, ← curry_natural_left, uncurry_curry, compTranspose_eq,
associator_inv_naturality_right_assoc, whisker_exchange_assoc]
dsimp
rw [whiskerLeft_curry'_ihom_ev_app, whiskerLeft_rightUnitor_inv, MonoidalCategory.whiskerRight_id_assoc,
Category.assoc, Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc, ]
