English
There exists a canonical isomorphism between the limit of the uncurry of whiskeringLeft₂ applied to K1, K2, G and the application of G to the limits of K1 and K2. This isomorphism reflects how taking a limit commutes with the bifunctor G when whiskering is involved.
Русский
Существует каноническое изоморфизм между пределом uncurry.obj(whiskeringLeft₂ C|>.obj K1|>.obj K2|>.obj G) и объектом (G.obj(limit K1)).obj(limit K2). Этот изоморфизм описывает, как пределы взаимодействуют с бифунктором G при использовании whiskering.
LaTeX
$$$\\lim(\\mathrm{uncurry.obj}(\\mathrm{whiskeringLeft₂}~C~|>.obj~K_1~|>.obj~K_2~|>.obj~G)) \\cong (G.obj \\ lim K_1).obj(\\ lim K_2)$$$
Lean4
/-- Extract the isomorphism between
`colim (uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G))` and
`(G.obj (colim K₁)).obj (colim K₂)` from a `PreservesLimit₂` instance, provided the relevant
limits exist. -/
noncomputable def isoLimitUncurryWhiskeringLeft₂ :
limit (uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)) ≅ (G.obj <| limit K₁).obj (limit K₂) :=
isoObjConePointsOfIsLimit G (limit.isLimit _) (limit.isLimit _) (limit.isLimit _) |>.symm
