proposition: Lemma is_invertible_2cell_unit' : is_invertible_2cell (Adjunctions.left_adjoint_unit counit_left_adjoint_data).
proof: Proof. repeat (use tpair) ; try (exact tt). - intro. use tpair. + exists (λ _, identity _). abstract ( intro ; intros ; simpl ; rewrite id_left ; apply id_right ). + abstract ( intro ; intros ; simpl ; unfold comp_lineator_data ; unfold identity_lineator_data ; cbn ; rewrite (bifunctor_leftid (_ ,, pr122 x)) ; apply id_right ). - abstract ( intro ; intros ; use equality_of_2cells_in_ACAT ; intro ; simpl ; rewrite ! id_left ; rewrite id_right ; apply (! functor_id _ _) ). - abstract ( use equality_of_ACAT_endofunctors ; intro ; intro ; simpl ; apply id_right ). - abstract (use equality_of_ACAT_endofunctors ; intro ; intro ; simpl ; apply id_right). 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