proposition: Lemma full_naturality_condition {F G : bifunctor_data A B C} {α : binat_trans_data F G} (αn : is_binat_trans α) {a1 a2 : A} {b1 b2 : B} (f : A⟦a1,a2⟧) (g : B⟦b1,b2⟧) : (f ⊗^{F} g)·(α a2 b2) = (α a1 b1)·(f ⊗^{G} g).
proof: Proof. unfold functoronmorphisms1. rewrite assoc'. rewrite (pr1 αn a2 _ _ g). rewrite assoc. rewrite (pr2 αn a1 a2 b1 f). apply assoc'. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.ProductCategory