Theorems · Theorem · category theory

CategoryTheory.Limits.coprod.map_map

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A₁ B₁] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A₂ B₂]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) (CategoryTheory.Limits.coprod.map h k) =
    CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k)

Defined in

Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasBinaryCoproductCategoryTheory.Limits.HasBinaryCoproductCategoryTheory.Limits.HasBinaryCoproduct