@[simp]
theorem
category_theory.bifunctor.map_id
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[category_theory.category C]
[category_theory.category D]
[category_theory.category E]
(F : C × D ⥤ E)
(X : C)
(Y : D) :
@[simp]
theorem
category_theory.bifunctor.map_id_comp
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[category_theory.category C]
[category_theory.category D]
[category_theory.category E]
(F : C × D ⥤ E)
(W : C)
{X Y Z : D}
(f : X ⟶ Y)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.bifunctor.map_comp_id
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[category_theory.category C]
[category_theory.category D]
[category_theory.category E]
(F : C × D ⥤ E)
(X Y Z : C)
(W : D)
(f : X ⟶ Y)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.bifunctor.diagonal
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[category_theory.category C]
[category_theory.category D]
[category_theory.category E]
(F : C × D ⥤ E)
(X X' : C)
(f : X ⟶ X')
(Y Y' : D)
(g : Y ⟶ Y') :
@[simp]
theorem
category_theory.bifunctor.diagonal'
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[category_theory.category C]
[category_theory.category D]
[category_theory.category E]
(F : C × D ⥤ E)
(X X' : C)
(f : X ⟶ X')
(Y Y' : D)
(g : Y ⟶ Y') :