English
Let F and G be functors between Cartesian monoidal categories. Then the natural transformation describing the product comparison for the composite F ∘ G is equal to the composite of the individual product-comparison natural transformations after appropriate whiskering, i.e. prodComparisonBifunctorNatTrans (F ∘ G) equals whiskering of prodComparisonBifunctorNatTrans F by G composed with whiskering of prodComparisonBifunctorNatTrans G by F.
Русский
Пусть F и G — функторы между декартовыми моёндальными категориями. Тогда натуральное преобразование, описывающее произведение сравнения для композиции F ∘ G, равно композиции соответствующих преобразований prodComparison после соответствующего отбрасывания по whiskering.
LaTeX
$$$\mathrm{prodComparisonBifunctorNatTrans}(F \circ G) = \mathrm{Functor.whiskerRight}(\mathrm{prodComparisonBifunctorNatTrans} F)\big((\mathrm{Functor.whiskeringRight} \;\_\;\_\;\_).\mathrm{obj} G\big) \; \circ \\; \mathrm{Functor.whiskerLeft} F\big(\mathrm{Functor.whiskerRight}(\mathrm{prodComparisonBifunctorNatTrans} G)\big((\mathrm{Functor.whiskeringLeft} \;\_\;\_\;\_).\mathrm{obj} F\big)\big)$$
Lean4
theorem prodComparisonBifunctorNatTrans_comp :
prodComparisonBifunctorNatTrans (F ⋙ G) =
Functor.whiskerRight (prodComparisonBifunctorNatTrans F) ((Functor.whiskeringRight _ _ _).obj G) ≫
Functor.whiskerLeft F
(Functor.whiskerRight (prodComparisonBifunctorNatTrans G) ((Functor.whiskeringLeft _ _ _).obj F)) :=
by ext; simp [prodComparison_comp]
