Theorems · Theorem · category theory

CategoryTheory.CommaMorphism.w_assoc

∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} (self : CategoryTheory.CommaMorphism X Y) {Z : T}
  (h : R.obj Y.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.map self.left) (CategoryTheory.CategoryStruct.comp Y.hom h) =
    CategoryTheory.CategoryStruct.comp X.hom (CategoryTheory.CategoryStruct.comp (R.map self.right) h)

Defined in

Mathlib.CategoryTheory.Comma.Basic

Cited by

1 results in Mathlib

Foundations

Depth 6 from the axioms · uses Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category