Proposition is_univalent_disp_cat_of_strict_twosided_disp_cat_hor_id : is_univalent_disp disp_cat_of_strict_twosided_disp_cat_hor_id. Proof. use is_univalent_disp_from_fibers. intros CD I₁ I₂. use isweqimplimpl. - intro F. use subtypePath. { intro. apply isaprop_hor_id_laws. } use total2_paths_f. + use funextsec. exact (pr11 F). + use funextsec ; intro x. use funextsec ; intro y. use funextsec ; intro f. rewrite !transportf_sec_constant. rewrite transportf_hor_id_data. rewrite !toforallpaths_funextsec. rewrite assoc_two_disp_alt. rewrite transport_f_f_disp_mor2. etrans. { do 2 apply maponpaths. exact (is_natural_preserves_hor_id (pr1 F) f). } rewrite two_disp_post_whisker_f. rewrite transport_f_f_disp_mor2. rewrite assoc_two_disp. unfold transportb_disp_mor2. rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. apply maponpaths_2. apply idtoiso_twosided_disp_concat. } unfold transportb_disp_mor2. rewrite two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. rewrite pathsinv0l. cbn. rewrite (id_two_disp_left (D := pr12 CD)). unfold transportb_disp_mor2. rewrite transport_f_f_disp_mor2. apply transportf_disp_mor2_idpath. - apply isaset_hor_id. - use isaproptotal2. + intro. apply isaprop_is_z_iso_disp. + intros. apply isaprop_preserves_hor_id. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.StrictTwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TransportLaws. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Basics.StrictDoubleCatBasics.