instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType

English

For a fixed S in LightProfinite, the functor category of CostructuredArrow toLightProfinite.op S has all small colimits in Type.

Русский

Для фиксированного S в LightProfinite композиции CostructuredArrow toLightProfinite.op S имеет все малые колимиты в Type.

LaTeX

$$$\\text{HasColimitsOfShape}(\\text{CostructuredArrow toLightProfinite.op S},\\mathbf{Type})$$$

Lean4

instance (S : LightProfinite.{u}ᵒᵖ) : HasColimitsOfShape (CostructuredArrow toLightProfinite.op S) (Type u) :=
  hasColimitsOfShape_of_equivalence (asEquivalence (CostructuredArrow.pre Skeleton.incl.op _ S))

Похожие утверждения