proposition: Proposition is_univalent_hor_cyl_twosided_disp_cat : is_univalent_twosided_disp_cat hor_cyl_twosided_disp_cat.
proof: Proof. intros h₁ h₂ k₁ k₂ p₁ p₂ s₁ s₂. induction p₁, p₂ ; cbn. use isweqimplimpl. - intros f. pose (p := pr1 f) ; cbn in p. rewrite uwhisker_square_id in p. rewrite dwhisker_square_id in p. exact p. - apply isaset_square_double_bicat. - use isaproptotal2. + intro. apply isaprop_is_iso_twosided_disp. + intros. apply isaset_square_double_bicat. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws