English
Naturality of coprodComparison in both arguments: coprodComparison F A B ≫ F.map (coprod.map f g) = coprod.map (F.map f) (F.map g) ≫ coprodComparison F A' B'.
Русский
Естественность coprodComparison по обоим аргументам: coprodComparison F A B ≫ F.map (coprod.map f g) = coprod.map (F.map f) (F.map g) ≫ coprodComparison F A' B'.
LaTeX
$$$ \\operatorname{coprodComparison} F A B \\; \\circ F(\\operatorname{coprod.map} f g) = \\operatorname{coprod.map}(F f)(F g) \\circ \\operatorname{coprodComparison} F A' B' $$$
Lean4
/-- Naturality of the coprod_comparison morphism in both arguments. -/
@[reassoc]
theorem coprodComparison_natural (f : A ⟶ A') (g : B ⟶ B') :
coprodComparison F A B ≫ F.map (coprod.map f g) = coprod.map (F.map f) (F.map g) ≫ coprodComparison F A' B' := by
rw [coprodComparison, coprodComparison, coprod.map_desc, ← F.map_comp, ← F.map_comp, coprod.desc_comp, ← F.map_comp,
coprod.inl_map, ← F.map_comp, coprod.inr_map]
