Definition is_univalent_disp_disp_hom {B : bicat} (D : disp_bicat B) (HD : disp_univalent_2_1 D) {x y : B} (xx : D x) (yy : D y) : is_univalent_disp (disp_hom xx yy). Proof. intros f g p ff gg. induction p. use weqhomot. - exact (disp_inv2cell_weq_disp_z_iso D _ _ ∘ make_weq _ (HD x y f f (idpath _) xx yy ff gg))%weq. - abstract (intro p ; induction p ; use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ] ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.