proposition: Lemma disp_prebicat_of_univ_disp_cats_laws : disp_prebicat_laws disp_prebicat_of_univ_disp_cats_data.
proof: Proof. repeat split ; red ; intros; intros ; apply (@disp_nat_trans_eq) ; intros ; apply pathsinv0 ; unfold transportb ; (etrans ; [ apply disp_nat_trans_transportf | ]). - apply pathsinv0. etrans. { apply id_left_disp. } apply pathsinv0; unfold transportb. apply maponpaths_2. apply homset_property. - apply pathsinv0. etrans. { apply id_right_disp. } apply pathsinv0; unfold transportb. apply maponpaths_2. apply homset_property. - apply pathsinv0. etrans. { apply assoc_disp. } apply pathsinv0; unfold transportb. apply maponpaths_2. apply homset_property. - apply transportf_set. apply homset_property. - apply pathsinv0. etrans. { cbn. apply disp_functor_id. } unfold transportb. apply maponpaths_2. apply homset_property. - apply transportf_set. apply homset_property. - cbn. etrans. { apply maponpaths. apply disp_functor_comp. } etrans. { apply transport_f_f. } apply transportf_set. apply homset_property. - cbn. etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. etrans. { apply maponpaths. apply id_right_disp. } etrans. { apply transport_f_f. } apply pathsinv0. etrans. { apply id_left_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. set (RR := @disp_nat_trans_ax_var _ _ _ _ _ _ _ _ _ φφ). etrans. { apply maponpaths. apply RR. } etrans. { apply transport_f_f. } apply transportf_set. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_left_disp. } etrans. { apply maponpaths. apply disp_functor_id. } etrans. { apply transport_f_f. } apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply assoc_disp_var. } etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } etrans. { apply maponpaths. apply disp_functor_id. } etrans. { apply transport_f_f. } apply pathsinv0. etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } apply maponpaths_2. apply homset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Adjunctions UniMath.CategoryTheory.DisplayedCats.Equivalences UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq UniMath.CategoryTheory.DisplayedCats.EquivalenceOverId UniMath.CategoryTheory.DisplayedCats.DisplayedCatEq UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispAdjunctions UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.DisplayedBicats.Examples.FullSub UniMath.Bicategories.DisplayedBicats.Examples.Sigma UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat