proposition: Lemma BinProduct_of_functors_commutes_law : is_nat_trans _ _ BinProduct_of_functors_commutes_data.
proof: Proof. intros c c' f. cbn. unfold BinProduct_of_functors_mor. etrans. 2: { apply pathsinv0, postcompWithBinProductArrow. } apply BinProductArrowUnique. - rewrite assoc'. etrans. { apply maponpaths. apply BinProductPr1Commutes. } etrans. { apply BinProductOfArrowsPr2. } apply idpath. - rewrite assoc'. etrans. { apply maponpaths. apply BinProductPr2Commutes. } etrans. { apply BinProductOfArrowsPr1. } apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.FunctorCategory UniMath.Combinatorics.StandardFiniteSets