proposition: Proposition is_univalent_disp_cat_of_strict_twosided_disp_cat_hor_comp : is_univalent_disp disp_cat_of_strict_twosided_disp_cat_hor_comp.
proof: Proof. use is_univalent_disp_from_fibers. intros CD Cm₁ Cm₂. use isweqimplimpl. - intro F. use subtypePath. { intro. apply isaprop_hor_comp_laws. } use total2_paths_f. + use funextsec ; intro x. use funextsec ; intro y. use funextsec ; intro z. use funextsec ; intro f. use funextsec ; intro g. exact (pr11 F x y z f g). + use funextsec ; intro x₁. use funextsec ; intro x₂. use funextsec ; intro y₁. use funextsec ; intro y₂. use funextsec ; intro z₁. use funextsec ; intro z₂. use funextsec ; intro vx. use funextsec ; intro vy. use funextsec ; intro vz. use funextsec ; intro h₁. use funextsec ; intro k₁. use funextsec ; intro h₂. use funextsec ; intro k₂. use funextsec ; intro s₁. use funextsec ; intro s₂. rewrite !transportf_sec_constant. rewrite (transportf_hor_comp_data s₁ s₂). unfold transportf_hor_comp_data_path. rewrite !toforallpaths_funextsec. rewrite assoc_two_disp_alt. rewrite transport_f_f_disp_mor2. etrans. { do 2 apply maponpaths. apply (is_natural_preserves_hor_comp (pr1 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_comp. - use isaproptotal2. + intro. apply isaprop_is_z_iso_disp. + intros. apply isaprop_preserves_hor_comp. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Categories.CategoryOfSetCategories UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.StrictTwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness UniMath.CategoryTheory.TwoSidedDisplayedCats.TransportLaws UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics UniMath.Bicategories.DoubleCategories.Basics.StrictDoubleCatBasics