Lemma equality_of_ACTI_endofunctors {a b : psfunctor_bicat ACTI ACTI} {f g : (psfunctor_bicat ACTI ACTI)⟦a,b⟧} (α β : prebicat_cells (psfunctor_bicat ACTI ACTI) f g) : (∏ x : ACTI, ∏ x0 : pr11 ((pr111 a) x), (pr11 ((pr111 α) x)) x0 = (pr11 ((pr111 β) x)) x0) -> α = β. Proof. intro p. use total2_paths_f. 2: { apply proofirrelevance ; apply isapropunit. } use total2_paths_f. 2: { use total2_paths_f ; (apply proofirrelevance ; try (apply isapropdirprod) ; apply isapropunit). } use total2_paths_f. 2: { apply proofirrelevance ; repeat (apply impred_isaprop ; intro) ; apply cellset_property. } apply funextsec ; intro. use equality_of_2cells_in_ACTI. intro. apply p. 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.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. Require Import UniMath.Bicategories.MonoidalCategories.BicatOfActegories. Require Import UniMath.Bicategories.MonoidalCategories.BicatOfActionsInBicat. Require Import UniMath.Bicategories.MonoidalCategories.WhiskeredMonoidalFromBicategory. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Biequivalence. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Import BifunctorNotations. Section ActegoryFromObject. End ActegoryFromObject. Section FromActegoriesToActionsInCat. Import MonoidalNotations. End FromActegoriesToActionsInCat. Section FromActionInCatToActegories. End FromActionInCatToActegories.