Theorems · Theorem · category theory

CategoryTheory.Functor.map_comp_assoc

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v_1, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v_2, u₂} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  {W : D} (h : F.obj Z ⟶ W),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) h)

Defined in

Mathlib.CategoryTheory.Functor.Basic

Cited by

72 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category