English
From a PreservesColimit₂ instance, obtain the isomorphism between the point of the colimit cocone for the uncurry construction and the image of the pair of colimits under G.
Русский
Из экземпляра PreservesColimit₂ следует изоморфизм между точкой cocone колимита для uncurry и образом пары колимитов под G.
LaTeX
$$$ (G.obj c1.pt).obj c2.pt \\cong c3.pt $$$
Lean4
instance [HasLimit K₁] [HasLimit K₂] [PreservesLimit₂ K₁ K₂ G] :
HasLimit <| uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G) where
exists_limit :=
⟨{ cone := _
isLimit :=
PreservesLimit₂.nonempty_isLimit_mapCone₂ (getLimitCone K₁).isLimit (getLimitCone K₂).isLimit |>.some }⟩
