Theorems · Theorem · category theory

CategoryTheory.CommaMorphism.w

∀ {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),
  CategoryTheory.CategoryStruct.comp (L.map self.left) Y.hom =
    CategoryTheory.CategoryStruct.comp X.hom (R.map self.right)

Defined in

Mathlib.CategoryTheory.Comma.Basic

Cited by

24 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category