English
Characterize the forward direction of the isomorphism between the colimit and the constructed cocone: a compatibility relation with the canonical injections holds.
Русский
Характеризуется прямая часть изоморфизма между колимитом и сконструированным cocone: выполняется совместимость с каноническими инъекциями.
LaTeX
$$$(G.map (colimit.ι K1 j1)).app(K2.j2) \\cdot (G.obj colim(K1)).map (colimit.ι K2 j2) \\cdot (iso).hom = colimit.ι (uncurry.obj(\\dots)) j$$$
Lean4
instance [HasColimit K₁] [HasColimit K₂] [PreservesColimit₂ K₁ K₂ G] :
HasColimit <| uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G) where
exists_colimit :=
⟨{ cocone := _
isColimit :=
PreservesColimit₂.nonempty_isColimit_mapCocone₂ (getColimitCocone K₁).isColimit
(getColimitCocone K₂).isColimit |>.some }⟩
