proposition: Lemma op1_prebicat_laws (C : prebicat) : prebicat_laws (op1_prebicat_data C).
proof: Proof. red. cbn. unfold op1_2cell_struct. cbn. repeat use tpair; cbn; intros *. - apply id2_left. - apply id2_right. - apply vassocr. - apply id2_rwhisker. - apply lwhisker_id2. - apply rwhisker_vcomp. - apply lwhisker_vcomp. - apply vcomp_runitor. - apply vcomp_lunitor. - apply rwhisker_rwhisker_alt. - apply pathsinv0, rwhisker_lwhisker_rassociator. - apply lwhisker_lwhisker_rassociator. - apply pathsinv0, vcomp_whisker. - apply runitor_rinvunitor. - apply rinvunitor_runitor. - apply lunitor_linvunitor. - apply linvunitor_lunitor. - apply rassociator_lassociator. - apply lassociator_rassociator. - apply lunitor_lwhisker. - apply rassociator_rassociator. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.PrecategoryBinProduct UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Morphisms.Adjunctions