Theorems · Theorem · category theory

CategoryTheory.Bifunctor.map_comp_id

∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor (C × D) E) (X Y Z : C) (W : D) (f : X ⟶ Y) (g : Y ⟶ Z),
  F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id W)))
      (F.map (CategoryTheory.Prod.mkHom g (CategoryTheory.CategoryStruct.id W)))

Defined in

Mathlib.CategoryTheory.Products.Bifunctor

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category