Definition bcat_2_id_comp_struct : prebicat_2_id_comp_struct bcat_1_id_comp_cells. Proof. repeat split; simpl; unfold bcat_cell_struct. - intros. exact (identity _). - intros. exact (left_unitor f). - intros. exact (right_unitor f). - intros. exact (inv_from_z_iso (left_unitor f)). - intros. exact (inv_from_z_iso (right_unitor f)). - intros. exact (inv_from_z_iso (associator f g h)). - intros. exact (associator_2mor f g h). - intros a b f g h x y. exact (x · y). - intros a b c f g1 g2 x. exact (whisker_left f x). - intros a b c f1 f2 g x. exact (whisker_right x g). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.Bicategories.WkCatEnrichment.prebicategory. Require Import UniMath.Bicategories.WkCatEnrichment.whiskering. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.WkCatEnrichment.Notations.