Theorems · Theorem · category theory

CategoryTheory.Limits.prod.pentagon

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.associator W X Y).hom
        (CategoryTheory.CategoryStruct.id Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator W (X ⨯ Y) Z).hom
        (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W)
          (CategoryTheory.Limits.prod.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator (W ⨯ X) Y Z).hom
      (CategoryTheory.Limits.prod.associator W X (Y ⨯ Z)).hom

Defined in

Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasBinaryProducts