Proposition make_double_bicat_laws (B : ver_bicat_sq_id_comp_whisker) (H₁ : whisker_square_bicat_law B) (H₂ : double_bicat_id_comp_square_laws B) (H₃ : double_bicat_cylinder_laws B) (H₄ : isaset_square_double_bicat_law B) : double_bicat_laws B. Proof. exact (H₁ ,, H₂ ,, H₃ ,, H₄). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.