Theorems · Theorem · category theory

CategoryTheory.Limits.CatCospanTransform.pentagon

∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''}
  {τ : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''} {A'''' : Type u₁₃} {B'''' : Type u₁₄}
  {C'''' : Type u₁₅} [inst_12 : CategoryTheory.Category.{v₁₃, u₁₃} A'''']
  [inst_13 : CategoryTheory.Category.{v₁₄, u₁₄} B''''] [inst_14 : CategoryTheory.Category.{v₁₅, u₁₅} C'''']
  {F'''' : CategoryTheory.Functor A'''' B''''} {G'''' : CategoryTheory.Functor C'''' B''''}
  {σ : CategoryTheory.Limits.CatCospanTransform F''' G''' F'''' G''''},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (ψ.associator φ τ).hom σ)
      (CategoryTheory.CategoryStruct.comp (ψ.associator (φ.comp τ) σ).hom
        (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (φ.associator τ σ).hom)) =
    CategoryTheory.CategoryStruct.comp ((ψ.comp φ).associator τ σ).hom (ψ.associator φ (τ.comp σ)).hom

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category