Lemma bidisp_actbicat_disp_prebicat_ops : disp_prebicat_ops bidisp_actbicat_disp_prebicat_1_id_comp_cells. 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.
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. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Import BifunctorNotations.