proposition: Theorem bcat_laws : prebicat_laws bcat_data.
proof: Proof. repeat split; unfold id2, vcomp2, runitor, lunitor, rinvunitor, linvunitor, rassociator, lassociator, lwhisker, rwhisker; simpl; unfold bcat_precategory_ob_mor, bcat_cell_struct, bcat_ob_mor_cells, bcat_1_id_comp_cells, bcat_2_id_comp_struct, bcat_data; simpl; first [ intros until 1 | intros ]. - apply id_left. - apply id_right. - apply assoc. - apply whisker_left_id_2mor. - apply whisker_right_id_2mor. - apply pathsinv0, whisker_left_on_comp. - apply pathsinv0, whisker_right_on_comp. - apply left_unitor_naturality. - apply right_unitor_naturality. - apply whisker_left_left. - apply whisker_left_right. - apply whisker_right_right. - apply twomor_naturality. - apply (z_iso_inv_after_z_iso (left_unitor f)). - apply (z_iso_after_z_iso_inv (left_unitor f)). - apply (z_iso_inv_after_z_iso (right_unitor f)). - apply (z_iso_after_z_iso_inv (right_unitor f)). - apply (z_iso_inv_after_z_iso (associator f g h)). - apply (z_iso_after_z_iso_inv (associator f g h)). - apply pathsinv0, (triangle_axiom f g). - apply pathsinv0, (pentagon_axiom f g h). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.HorizontalComposition UniMath.Bicategories.WkCatEnrichment.prebicategory UniMath.Bicategories.WkCatEnrichment.whiskering UniMath.Bicategories.Core.Bicat UniMath.Bicategories.WkCatEnrichment.Notations