proposition: Lemma precomp_convertor_data_is_nat_trans : is_nat_trans _ _ precomp_convertor_nat_trans_data.
proof: Proof. red. intros x x' f. unfold odot_x_odot_y_functor, odot_x_otimes_y_functor, precomp_odot. cbn. apply hcomp_lassoc. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory UniMath.Bicategories.MonoidalCategories.Actions UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfCats