Definition map1cells_disp_univalent_2_1 : disp_univalent_2_1 map1cells_disp_bicat. Proof. apply fiberwise_local_univalent_is_univalent_2_1. intros F G η F₁ G₁ η₁ η₁'. use isweqimplimpl. - intro m ; cbn in *. apply funextsec ; intro X. apply funextsec ; intro Y. apply funextsec ; intro f. pose (pr1 m X Y f) as n. cbn in n. rewrite id2_rwhisker, lwhisker_id2 in n. rewrite id2_left, id2_right in n. apply subtypePath. + intro. apply isaprop_is_invertible_2cell. + apply n. - repeat (apply impred_isaset ; intro). use isaset_total2. + apply D. + intro. apply isasetaprop. apply isaprop_is_invertible_2cell. - apply isaproptotal2. + intro. apply (@isaprop_is_disp_invertible_2cell (ps_base C D)). + intros. repeat (apply funextsec ; intro). apply D. Defined.
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.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.