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. unfold functoronmorphisms1. rewrite assoc'. rewrite (pr1 αn a2 _ _ g). rewrite assoc. rewrite (pr2 αn a1 a2 b1 f). apply assoc'. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import  UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.ProductCategory. Import BifunctorNotations. Import BifunctorNotations. Section FunctorsFromProductCategory. Import BifunctorNotations. End FunctorsFromProductCategory. Import BifunctorNotations. Import BifunctorNotations. Import BifunctorNotations.