proposition: Proposition disp_univalent_2_1_disp_bicat_on_cat_to_univ_cat (HD : disp_univalent_2_1 D) : disp_univalent_2_1 disp_bicat_on_cat_to_univ_cat.
proof: Proof. use fiberwise_local_univalent_is_univalent_2_1. intros C₁ C₂ F CC₁ CC₂ FF GG. use weqhomot. - refine (weqfibtototal _ _ (λ τ, weqfibtototal _ _ (λ θ, weqdirprodf (weqimplimpl _ _ _ _) (weqimplimpl _ _ _ _))) ∘ make_weq _ (HD (pr1 C₁) (pr1 C₂) F F (idpath F) CC₁ CC₂ FF GG))%weq. + abstract (intro p ; refine (p @ _) ; apply maponpaths_2 ; apply cellset_property). + abstract (intro p ; refine (p @ _) ; apply maponpaths_2 ; apply cellset_property). + abstract (apply (pr2 D)). + abstract (apply (pr2 D)). + abstract (intro p ; refine (p @ _) ; apply maponpaths_2 ; apply cellset_property). + abstract (intro p ; refine (p @ _) ; apply maponpaths_2 ; apply cellset_property). + abstract (apply (pr2 D)). + abstract (apply (pr2 D)). - abstract (intro p ; induction p ; use subtypePath ; [ intro ; apply isaprop_is_disp_invertible_2cell | ] ; apply idpath). Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.DisplayedCats.Core UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfCats UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.BicatOfCatToUnivCat UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.DispPseudofunctor