English
If C has countable colimits, then for any countable category J, C has colimits of shape J.
Русский
Если в C существуют счётные колимиты, то для любой счётной категории J у C существуют колимиты формы J.
LaTeX
$$$ [\\operatorname{HasCountableColimits} \\mathcal{C}] \\Rightarrow [\\text{Countable } J] \\Rightarrow \\operatorname{HasColimitsOfShape J \\mathcal{C}} $$$
Lean4
instance [HasCountableColimits C] (J : Type*) [Category.{v} J] [CountableCategory J] : HasColimitsOfShape J C :=
have : HasColimitsOfShape (HomAsType J) C := HasCountableColimits.out (HomAsType J)
hasColimitsOfShape_of_equivalence (homAsTypeEquiv J)
