Lemma bidisp_monlaxbicat_disp_prebicat_ops : disp_prebicat_ops bidisp_monlaxbicat_disp_prebicat_1_id_comp_cells. 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)). - assert (aux := pr1 X (pr1 f a0) (pr1 f a')). unfold fmonoidal_preservestensordata in aux. etrans. 2: { rewrite assoc. apply cancel_postcomposition. exact aux. } clear aux. repeat rewrite assoc'. apply maponpaths. apply nat_trans_ax. - assert (aux := pr2 X). red in aux. unfold fmonoidal_preservesunit in aux. rewrite <- aux. repeat rewrite assoc'. apply maponpaths. apply nat_trans_ax. - etrans. { rewrite assoc'. apply maponpaths. apply pathsinv0, functor_comp. } etrans. { do 2 apply maponpaths. apply (pr1 X). } unfold fmonoidal_preservestensordata. rewrite functor_comp. repeat rewrite assoc. apply cancel_postcomposition. apply pathsinv0, preservestensor_is_nattrans_full. + apply (fmonoidal_preservestensornatleft (gg : fmonoidal_lax _ _ g)). + apply (fmonoidal_preservestensornatright (gg : fmonoidal_lax _ _ g)). - rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, functor_comp. } apply maponpaths. apply (pr2 X). 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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Import BifunctorNotations.