Theorems · Theorem · category theory

CategoryTheory.Limits.FormalCoproduct.powerMap_comp

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {U V W : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V)
  (g : V ⟶ W) (α : Type t) [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C],
  CategoryTheory.Limits.FormalCoproduct.powerMap (CategoryTheory.CategoryStruct.comp f g) α =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap f α)
      (CategoryTheory.Limits.FormalCoproduct.powerMap g α)

Defined in

Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasProductsOfShape