Theorems · Definition · category theory

CategoryTheory.Limits.FormalCoproduct.power

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Limits.FormalCoproduct C →
      (α : Type t) → [CategoryTheory.Limits.HasProductsOfShape α C] → CategoryTheory.Limits.FormalCoproduct C

Given U : FormalCoproduct C and a type α, this is the formal coproduct indexed by all i : α → U.I of the products of the objects U.obj (i a) for all a : α.

Defined in

Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Cited by

27 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasProductsOfShape