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. 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.
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.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.Bicategories.WkCatEnrichment.prebicategory. Require Import UniMath.Bicategories.WkCatEnrichment.Notations. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.