proposition: Lemma acti_to_acat_counit_is_pstrans : is_pstrans acti_to_acat_counit_data.
proof: Proof. repeat split ; intros ; intros ; use equality_of_2cells_in_ACAT ; intro ; intros ; simpl. - rewrite id_left ; apply id_right. - rewrite id_left ; apply (! id_left _). - rewrite ! id_left ; rewrite ! id_right ; apply (! functor_id _ _). 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.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 UniMath.Bicategories.MonoidalCategories.BicatOfActegories UniMath.Bicategories.MonoidalCategories.BicatOfActionsInBicat UniMath.Bicategories.MonoidalCategories.WhiskeredMonoidalFromBicategory UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Biequivalence UniMath.Bicategories.Transformations.PseudoTransformation