proposition: Lemma bifunctor_on_morphisms_comm {A B C : category} (F : A ⊠ B ⟶ C) {a a' : A} {b b' : B} (f : a --> a') (g : b --> b') : #F (f #, identity _) · #F (identity _ #, g) = #F (identity _ #, g) · #F (f #, identity _).
proof: Proof. rewrite <- !functor_comp. change ((?x #, ?y) · (?z #, ?w)) with (x · z #, y · w). rewrite !id_left, !id_right. reflexivity. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Core.Isos