proposition: Lemma total_prebicat_laws : prebicat_laws total_prebicat_data.
proof: Proof. repeat split; intros. - use total2_paths_b. + apply id2_left. + apply disp_id2_left. - use total2_paths_b. + apply id2_right. + apply disp_id2_right. - use total2_paths_b. + apply vassocr. + apply disp_vassocr. - use total2_paths_b. + apply lwhisker_id2. + apply disp_lwhisker_id2. - use total2_paths_b. + apply id2_rwhisker. + apply disp_id2_rwhisker. - use total2_paths_b. + apply lwhisker_vcomp. + apply disp_lwhisker_vcomp. - use total2_paths_b. + apply rwhisker_vcomp. + apply disp_rwhisker_vcomp. - use total2_paths_b. + apply vcomp_lunitor. + apply disp_vcomp_lunitor. - use total2_paths_b. + apply vcomp_runitor. + apply disp_vcomp_runitor. - use total2_paths_b. + apply lwhisker_lwhisker. + apply disp_lwhisker_lwhisker. - use total2_paths_b. + apply rwhisker_lwhisker. + apply disp_rwhisker_lwhisker. - use total2_paths_b. + apply rwhisker_rwhisker. + apply disp_rwhisker_rwhisker. - use total2_paths_b. + apply vcomp_whisker. + apply disp_vcomp_whisker. - use total2_paths_b. + apply lunitor_linvunitor. + apply disp_lunitor_linvunitor. - use total2_paths_b. + apply linvunitor_lunitor. + apply disp_linvunitor_lunitor. - use total2_paths_b. + apply runitor_rinvunitor. + apply disp_runitor_rinvunitor. - use total2_paths_b. + apply rinvunitor_runitor. + apply disp_rinvunitor_runitor. - use total2_paths_b. + apply lassociator_rassociator. + apply disp_lassociator_rassociator. - use total2_paths_b. + apply rassociator_lassociator. + apply disp_rassociator_lassociator. - use total2_paths_b. + apply runitor_rwhisker. + apply disp_runitor_rwhisker. - use total2_paths_b. + apply lassociator_lassociator. + apply disp_lassociator_lassociator. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Univalence