proposition: Lemma bicate_lassociator_fun_natural {a b c d : bicate_id_comp} : is_nat_trans (functor_composite (pair_functor (functor_identity _) (compose_functor b c d)) hcomp_functor) (functor_composite (precategory_binproduct_assoc (hom a b) (hom b c) (hom c d)) (functor_composite (pair_functor (compose_functor a b c) (functor_identity _)) hcomp_functor)) bicate_lassociator_fun.
proof: Proof. red; cbn. intros (f1, (f2, f3)) (g1, (g2, g3)). unfold precategory_binproduct_mor, hom_ob_mor. simpl. unfold precategory_binproduct_mor, hom_ob_mor. simpl. intros (x1, (x2, x3)). simpl. unfold bicate_lassociator_fun. simpl. apply hcomp_lassoc. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.HorizontalComposition UniMath.Bicategories.WkCatEnrichment.prebicategory UniMath.Bicategories.WkCatEnrichment.Notations UniMath.Bicategories.Core.Bicat