proposition: Lemma bidisp_monbicat_disp_prebicat_ops : disp_prebicat_ops bidisp_monbicat_disp_prebicat_1_id_comp_cells.
proof: Proof. split. { intros; apply is_mon_nat_trans_identity. } repeat split; try red; cbn; unfold fmonoidal_preservestensordata, fmonoidal_preservesunit; intros; show_id_type. - rewrite functor_id. do 2 rewrite id_right. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, bifunctor_distributes_over_id. - cbn in *. apply (bifunctor_leftid y). - cbn in *. apply (bifunctor_rightid y). } apply pathsinv0, id_left. - rewrite functor_id. rewrite id_right. apply id_right. - etrans. 2: { apply cancel_postcomposition. apply pathsinv0, bifunctor_distributes_over_id. - cbn in *. apply (bifunctor_leftid y). - cbn in *. apply (bifunctor_rightid y). } apply id_right. - rewrite id_right. apply id_left. - etrans. 2: { apply cancel_postcomposition. apply pathsinv0, bifunctor_distributes_over_id. - cbn in *. apply (bifunctor_leftid y). - cbn in *. apply (bifunctor_rightid y). } rewrite functor_id. apply pathsinv0, id_left. - rewrite functor_id. apply idpath. - etrans. 2: { apply cancel_postcomposition. apply pathsinv0, bifunctor_distributes_over_id. - cbn in *. apply (bifunctor_leftid y). - cbn in *. apply (bifunctor_rightid y). } do 2 rewrite id_left. apply id_right. - rewrite id_left. apply id_right. - etrans. 2: { apply cancel_postcomposition. apply pathsinv0, bifunctor_distributes_over_id. - cbn in *. apply (bifunctor_leftid z). - cbn in *. apply (bifunctor_rightid z). } rewrite id_right. rewrite id_left. repeat rewrite assoc'. apply maponpaths. apply functor_comp. - rewrite id_right. rewrite assoc'. apply maponpaths. apply functor_comp. - etrans. 2: { apply cancel_postcomposition. apply pathsinv0, bifunctor_distributes_over_id. - cbn in *. apply (bifunctor_leftid z). - cbn in *. apply (bifunctor_rightid z). } rewrite id_right. rewrite id_left. repeat rewrite assoc'. apply maponpaths. apply pathsinv0, functor_comp. - rewrite id_right. repeat rewrite assoc'. apply maponpaths. apply pathsinv0, functor_comp. - apply (pr1 (is_mon_nat_trans_comp _ _ _ _ _ X X0)). - apply (pr2 (is_mon_nat_trans_comp _ _ _ _ _ X X0)). - apply (pr1 (is_mon_nat_trans_prewhisker _ X)). - apply (pr2 (is_mon_nat_trans_prewhisker _ X)). - apply (pr1 (is_mon_nat_trans_postwhisker X _)). - apply (pr2 (is_mon_nat_trans_postwhisker X _)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Examples.BicatOfCats UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors