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. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.BicatOfCatToUnivCat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor.