Lemma actions_disp_prebicat_ops : disp_prebicat_ops actions_disp_prebicat_1_id_comp_cells. Proof. repeat split. - intros A A' F actn actn' ζ a v. red. cbn. rewrite binprod_id. rewrite id_right. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, functor_id. } apply pathsinv0, id_left. - intros A A' F actn actn' ζ a v. red. cbn. rewrite id_right. rewrite binprod_id. etrans. 2: { apply cancel_postcomposition, pathsinv0, functor_id. } rewrite id_left. rewrite functor_id. apply id_right. - intros A A' F actn actn' ζ a v. red. cbn. rewrite binprod_id. etrans. 2: { apply cancel_postcomposition, pathsinv0, functor_id. } do 2 rewrite id_left. apply id_right. - intros A A' F actn actn' ζ a v. red. cbn. rewrite binprod_id. etrans. 2: { apply cancel_postcomposition, pathsinv0, functor_id. } rewrite functor_id. rewrite id_left. apply idpath. - intros A A' F actn actn' ζ a v. red. cbn. rewrite binprod_id. etrans. 2: { apply cancel_postcomposition, pathsinv0, functor_id. } do 2 rewrite id_left. apply id_right. - intros A1 A2 A3 A4 F1 F2 F3 actn1 actn2 actn3 actn4 ζ1 ζ2 ζ3 a v. red. cbn. rewrite binprod_id. etrans. 2: { apply cancel_postcomposition, pathsinv0, functor_id. } rewrite id_right, id_left. rewrite <- assoc. apply maponpaths. apply functor_comp. - intros A1 A2 A3 A4 F1 F2 F3 actn1 actn2 actn3 actn4 ζ1 ζ2 ζ3 a v. red. cbn. rewrite binprod_id. etrans. 2: { apply cancel_postcomposition, pathsinv0, functor_id. } rewrite id_right, id_left. rewrite <- assoc. apply maponpaths. apply pathsinv0, functor_comp. - intros A A' F1 F2 F3 η η' actn actn' ζ1 ζ2 ζ3 Hypη Hypη' a v. red. cbn. rewrite <- (id_left (id v)). rewrite binprod_comp. etrans. 2: { apply cancel_postcomposition, pathsinv0, functor_comp. } assert (Hypηinst := Hypη a v). assert (Hypη'inst := Hypη' a v). red in Hypηinst, Hypη'inst. etrans. { rewrite assoc. apply cancel_postcomposition. exact Hypηinst. } etrans. { rewrite <- assoc. apply maponpaths. exact Hypη'inst. } apply assoc. - intros A1 A2 A3 F G1 G2 η actn1 actn2 actn3 ζ ζ1 ζ2 Hypη a v. red. cbn. assert (Hypηinst := Hypη (pr1 F a) v). red in Hypηinst. unfold ActionBasedStrongFunctorCategory.ζ in Hypηinst. cbn in Hypηinst. etrans. 2: { rewrite assoc. apply cancel_postcomposition. exact Hypηinst. } do 2 rewrite <- assoc. apply maponpaths. apply nat_trans_ax. - intros A1 A2 A3 F1 F2 G η actn1 actn2 actn3 ζ1 ζ2 ζ Hypη a v. red. cbn. assert (Hypηinst := Hypη a v). red in Hypηinst. unfold ActionBasedStrongFunctorCategory.ζ in Hypηinst. cbn in Hypηinst. etrans. { rewrite <- assoc. apply maponpaths. apply pathsinv0, functor_comp. } etrans. { do 2 apply maponpaths. exact Hypηinst. } clear Hypηinst. rewrite functor_comp. do 2 rewrite assoc. apply cancel_postcomposition. assert (ζnatinst := nat_trans_ax (pr1 ζ) (pr1 F1 a,, v) (pr1 F2 a,, v) (pr1 η a,, id₁ v)). apply pathsinv0, ζnatinst. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.Bicategories.MonoidalCategories.Actions. Require Import UniMath.Bicategories.MonoidalCategories.ActionBasedStrength. Require Import UniMath.Bicategories.MonoidalCategories.ActionBasedStrongFunctorCategory. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Import Bicat.Notations.