Proposition lift_disp_prebicat_laws : disp_prebicat_laws lift_disp_prebicat_data. Proof. repeat split ; intro ; intros ; rewrite lift_transportb. - refine (disp_id2_left _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_id2_right _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_vassocr _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_lwhisker_id2 _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_id2_rwhisker _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_lwhisker_vcomp _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_rwhisker_vcomp _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_vcomp_lunitor _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_vcomp_runitor _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_lwhisker_lwhisker _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_rwhisker_lwhisker _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_rwhisker_rwhisker _ _ _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_vcomp_whisker _ _ _ _ _ _ _ _ _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_lunitor_linvunitor _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_linvunitor_lunitor _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_runitor_rinvunitor _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_rinvunitor_runitor _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_lassociator_rassociator _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_rassociator_lassociator _ _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_runitor_rwhisker _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_lassociator_lassociator _ _ _ _ @ _). apply maponpaths_2. apply cellset_property. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Section FromLift. End FromLift.