English
There is a canonical isomorphism between the threefold curry of a product-then-composition functor and a nested composition of curries, whiskering, and projection.
Русский
Существует каноническое изоморфие между тройственным каррированием композиции через произведение и вложенным построением каррирования, отбивки и проекции.
LaTeX
$$$$ \\mathrm{curry}_3.\\mathrm{obj}\\big(F_1.\\mathrm{prod}(F_2.\\mathrm{prod}F_3)\\;\\mathrm{⋙}\\; G\\big) \\;\\cong\\; F_1.\\mathrm{⋙}\\mathrm{curry}_3.\\mathrm{obj}G.\\;\\;((\\mathrm{whiskeringLeft}_2 E).\\mathrm{obj}F_2).\\mathrm{obj}F_3. $$$$
Lean4
/-- Given functors `F₁ : C₁ ⥤ D₁`, `F₂ : C₂ ⥤ D₂`, `F₃ : C₃ ⥤ D₃`
and `G : D₁ × D₂ × D₃ ⥤ E`, this is the isomorphism between
`curry₃.obj (F₁.prod (F₂.prod F₃) ⋙ G) : C₁ ⥤ C₂ ⥤ C₃ ⥤ E`
and `F₁ ⋙ curry₃.obj G ⋙ ((whiskeringLeft₂ E).obj F₂).obj F₃`. -/
@[simps!]
def curry₃ObjProdComp (F₁ : C₁ ⥤ D₁) (F₂ : C₂ ⥤ D₂) (F₃ : C₃ ⥤ D₃) (G : D₁ × D₂ × D₃ ⥤ E) :
curry₃.obj (F₁.prod (F₂.prod F₃) ⋙ G) ≅ F₁ ⋙ curry₃.obj G ⋙ ((whiskeringLeft₂ E).obj F₂).obj F₃ :=
NatIso.ofComponents (fun X₁ ↦ NatIso.ofComponents (fun X₂ ↦ NatIso.ofComponents (fun X₃ ↦ Iso.refl _)))
