proposition: 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: 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.
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