English
For a bifunctor F : C × D ⥤ E there is a natural coherence relation expressing that applying F to a pair of morphisms (f,g) is the same as composing appropriate images in each coordinate: F.map ((f ≫ g) × 𝟙) ≫ F.map (f × 𝟙) = F.map (f × g).
Русский
Для бисюфункторa F : C × D ⥤ E существует естественное соотношение согласованности, выражающее, что применение F к паре морфизмов (f,g) эквивалентно композиции образов по координатам: F.map ((f ≫ g) × 𝟙) ≫ F.map (f × 𝟙) = F.map (f × g).
LaTeX
$$$F.map ((f \\gg g) \\times 𝟙 W) \\;\\; \\; = \\; F.map (f \\times 𝟙 W) \\;\\; \\; ≫ \\; F.map (f \\times g)$$$
Lean4
@[simp]
theorem map_comp_id (F : C × D ⥤ E) (X Y Z : C) (W : D) (f : X ⟶ Y) (g : Y ⟶ Z) :
F.map ((f ≫ g) ×ₘ 𝟙 W) = F.map (f ×ₘ 𝟙 W) ≫ F.map (g ×ₘ 𝟙 W) := by
rw [← Functor.map_comp, prod_comp, Category.comp_id]
