English
Explicit canonical isomorphism equality between bifunctorComp₂₃ and the currying expression holds componentwise; i.e., the map respects composition in each variable.
Русский
Является каноническим равенством изоморфий между bifunctorComp₂₃ и выражением каррирования, сохраняющее композицию по каждому аргументу.
LaTeX
$$$$ \\text{Eq}\\big( \\mathrm{bifunctorComp}_{23} F G_{23} , \\; \\mathrm{curry.obj}(\\mathrm{curry.obj}(\\mathrm{prod.associator} \\cdot \\mathrm{uncurry.obj}(\\ldots))) \\big). $$$$
Lean4
/-- `bifunctorComp₂₃` can be described in terms of the curryfication of functors. -/
@[simps!]
def bifunctorComp₂₃Iso (F : C₁ ⥤ C₂₃ ⥤ E) (G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃) :
bifunctorComp₂₃ F G₂₃ ≅
curry.obj (curry.obj (prod.associator _ _ _ ⋙ uncurry.obj (uncurry.obj G₂₃ ⋙ F.flip).flip)) :=
NatIso.ofComponents (fun _ ↦ NatIso.ofComponents (fun _ ↦ NatIso.ofComponents (fun _ ↦ Iso.refl _)))
