Theorems · Definition · category theory

CategoryTheory.Limits.sigmaObj

{β : Type w} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (f : β → C) → [CategoryTheory.Limits.HasCoproduct f] → C

sigmaObj f computes the coproduct of a family of elements f. (It is defined as an abbreviation for colimit (Discrete.functor f), so for most facts about sigmaObj f, you will just use general facts about colimits.)

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Products

Cited by

302 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 80 definitions · uses propext, Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasCoproduct