English
In a closed monoidal category, the inverse of the left distributivity morphism ∂L is given by an explicit uncurry of the curry of the coprod.inl and coprod.inr maps; i.e., left distributivity is controlled by the closed structure.
Русский
В замкнутой моноидальной категории обратное распределение задаётся явным образом через карри и карри-раскрытие копрод-инл и копрод-инр, а значит левое распределение управляемо закрытой структурой.
LaTeX
$$$ (leftDistrib X Y Z)^{-1} = \\operatorname{uncurry}(\\operatorname{coprod.desc}(\\operatorname{curry}(\\operatorname{coprod.inl}), \\operatorname{curry}(\\operatorname{coprod.inr})))$$$
Lean4
/-- The inverse of distributivity isomorphism from the closed monoidal structure -/
theorem leftDistrib_inv [MonoidalClosed C] {X Y Z : C} :
(leftDistrib X Y Z).inv = uncurry (coprod.desc (curry coprod.inl) (curry coprod.inr)) :=
by
rw [← curry_eq_iff]
ext <;> simp [← curry_natural_left]
