Theorems · Definition · category theory

CategoryTheory.Limits.sigmaFunctor

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] → CategoryTheory.Functor C (CategoryTheory.Functor (Type w) C)

The functor C ⥤ Type w ⥤ C which sends X : C and α : Type w to the coproduct of copies of X indexed by α.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Products

Cited by

3 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasCoproducts