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.
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.CategoryTheory.DisplayedCats.Total. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence.