English
Given F1 : C ⥤ D, F2 : C' ⥤ D' and G : D × D' ⥤ E, there is a natural isomorphism in the functor category: curry.obj((F1.prod F2).comp G) ≅ F1 ∘ curry.obj G ∘ (whiskeringLeft C' D' E).obj F2.
Русский
Пусть F1 : C ⥤ D, F2 : C' ⥤ D' и G : D × D' ⥤ E; существует каноническое естественное изоморождение в категории функторов: curl.obj((F1×F2)∘G) ≅ F1 ∘ curl.obj G ∘ (whiskeringLeft C' D' E).obj F2.
LaTeX
$$$\text{curry.obj}((F_1 \prod F_2) \circ G) \cong F_1 \circ \text{curry.obj} G \circ (\mathrm{whiskeringLeft}\, C'\, D'\, E) .\mathrm{obj} F_2$$$
Lean4
/-- Given functors `F₁ : C ⥤ D`, `F₂ : C' ⥤ D'` and `G : D × D' ⥤ E`, this is the isomorphism
between `curry.obj ((F₁.prod F₂).comp G)` and
`F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂` in the category `C ⥤ C' ⥤ E`. -/
@[simps!]
def curryObjProdComp {C' D' : Type*} [Category C'] [Category D'] (F₁ : C ⥤ D) (F₂ : C' ⥤ D') (G : D × D' ⥤ E) :
curry.obj ((F₁.prod F₂).comp G) ≅ F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂ :=
NatIso.ofComponents (fun X₁ ↦ NatIso.ofComponents (fun X₂ ↦ Iso.refl _))
