Lemma total_prebicat_laws : prebicat_laws total_prebicat_data. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence.