Theorem bcat_laws : prebicat_laws bcat_data. 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.
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.