Lemma op1_prebicat_laws (C : prebicat) : prebicat_laws (op1_prebicat_data C). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.Adjunctions.