Definition BothCategoriesUnivalent: is_univalent (Signature_category C D D') × is_univalent (Strong_Functor_category (Mon_endo' C (homset_property C)) (domain_action C (homset_property C) D' (homset_property D')) (target_action C (homset_property C) D (homset_property D)) (functor_category_has_homsets _ _ (homset_property D))). Proof. split. - exact (is_univalent_Signature_category C D D'). - set (univalentA' := make_univalent_category [C, D, homset_property D] (is_univalent_functor_category C D (univalent_category_is_univalent D))). change (is_univalent (Strong_Functor_category (Mon_endo' C (homset_property C)) (domain_action C (homset_property C) D' (homset_property D')) (target_action C (homset_property C) D (homset_property D)) (homset_property univalentA'))). assert (target := target_action C (homset_property C) D (homset_property D)). assert (test1 : pr1 univalentA' = [C, D, homset_property D]). { apply idpath. } clear test1. set (test2 := pr22 univalentA'). cbn in test2. unfold functor_category_has_homsets in test2. set (test3 := pr2 bicat_of_cats C (univalent_category_to_category D)). cbn in test3. unfold isaset_cells_prebicat_of_cats in test3. assert (test4 : test3 = test2). { apply idpath. } clear test2 test3 test4. } *) set (what_we_want_without_last_argument := is_univalent_Strong_Functor_category (Mon_endo' C (homset_property C)) (hom(C:=bicat_of_cats) C D') univalentA' (domain_action C (homset_property C) D' (homset_property D'))). (* exact what_we_want. Defined.
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.PointedFunctors. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.Bicategories.MonoidalCategories.PointedFunctorsMonoidal. Require Import UniMath.Bicategories.MonoidalCategories.Actions. Require Import UniMath.Bicategories.MonoidalCategories.ConstructionOfActions. Require Import UniMath.Bicategories.MonoidalCategories.ActionOfEndomorphismsInBicat. Require Import UniMath.Bicategories.MonoidalCategories.ActionBasedStrength. Require Import UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory. Require Import UniMath.Bicategories.MonoidalCategories.ActionBasedStrongFunctorCategory. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SignatureCategory. Require Import UniMath.CategoryTheory.Core.Univalence. Import Bicat.Notations. Section Signature_From_ActionBased_Strength. End Signature_From_ActionBased_Strength. Section ActionBased_Strength_From_Signature. End ActionBased_Strength_From_Signature.