proposition: Lemma bidisp_actbicat_disp_prebicat_ops : disp_prebicat_ops bidisp_actbicat_disp_prebicat_1_id_comp_cells.
proof: Proof. repeat split; cbn; unfold bidisp_actbicat_disp_2cell_struct, comp_lineator, identity_lineator. - intros. apply is_linear_nat_trans_identity. - intros C D F ActC ActD lin v c. cbn. unfold comp_lineator_data, identity_lineator_lax. cbn. unfold identity_lineator_data. rewrite functor_id. do 2 rewrite id_right. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, (bifunctor_leftid ActD). } apply pathsinv0, id_left. - intros C D F ActC ActD lin v c. cbn. unfold comp_lineator_data, identity_lineator_lax. cbn. unfold identity_lineator_data. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, (bifunctor_leftid ActD). } apply id_right. - intros C D F ActC ActD lin v c. cbn. unfold comp_lineator_data, identity_lineator_lax. cbn. unfold identity_lineator_data. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, (bifunctor_leftid ActD). } rewrite functor_id. apply pathsinv0, id_left. - intros C D F ActC ActD lin v c. cbn. unfold comp_lineator_data, identity_lineator_lax. cbn. unfold identity_lineator_data. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, (bifunctor_leftid ActD). } do 2 rewrite id_left. apply id_right. - intros C1 C2 C3 C4 F G H ActC1 ActC2 ActC3 ActC4 Fl Gl Hl v x. cbn. unfold comp_lineator_data, identity_lineator_lax. cbn. unfold comp_lineator_data. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, (bifunctor_leftid ActC4). } rewrite id_right. rewrite id_left. repeat rewrite assoc'. apply maponpaths. apply functor_comp. - intros C1 C2 C3 C4 F G H ActC1 ActC2 ActC3 ActC4 Fl Gl Hl v x. cbn. unfold comp_lineator_data, identity_lineator_lax. cbn. unfold comp_lineator_data. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, (bifunctor_leftid ActC4). } rewrite id_right. rewrite id_left. repeat rewrite assoc'. apply maponpaths. apply pathsinv0, functor_comp. - intros C D F G H α β ActC ActD Fl Gl Hl linα linβ v x. cbn. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, (bifunctor_leftcomp ActD). } rewrite assoc. etrans. { apply cancel_postcomposition. apply (linα v x). } repeat rewrite assoc'. apply maponpaths. apply linβ. - intros C D E F G1 G2 β ActC ActD ActE Fl G1l G2l linβ v x. cbn. unfold comp_lineator_data. assert (aux := linβ v (F x)). etrans. 2: { rewrite assoc. apply cancel_postcomposition. exact aux. } clear aux. repeat rewrite assoc'. apply maponpaths. apply nat_trans_ax. - intros C D E F1 F2 G α ActC ActD ActE F1l F2l Gl linα v x. cbn. unfold comp_lineator_data. etrans. { rewrite assoc'. apply maponpaths. apply pathsinv0, functor_comp. } etrans. { do 2 apply maponpaths. apply linα. } rewrite functor_comp. repeat rewrite assoc. apply cancel_postcomposition. apply pathsinv0, lineator_linnatleft. 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 UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories