fact: Definition disp_prebicat_laws : UU := disp_id2_left_law × disp_id2_right_law × disp_vassocr_law × disp_lwhisker_id2_law × disp_id2_rwhisker_law × disp_lwhisker_vcomp_law × disp_rwhisker_vcomp_law × disp_vcomp_lunitor_law × disp_vcomp_runitor_law × disp_lwhisker_lwhisker_law × disp_rwhisker_lwhisker_law × disp_rwhisker_rwhisker_law × disp_vcomp_whisker_law × disp_lunitor_linvunitor_law × disp_linvunitor_lunitor_law × disp_runitor_rinvunitor_law × disp_rinvunitor_runitor_law × disp_lassociator_rassociator_law × disp_rassociator_lassociator_law × disp_runitor_rwhisker_law × disp_lassociator_lassociator_law.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Univalence