proposition: Lemma sigma_prebicat_laws : disp_prebicat_laws sigma_bicat_data.
proof: Proof. repeat split; red; cbn; intros *; use (@total2_reassoc_paths' (_ ==> _) (fun x' => _ ==>[ x'] _) (fun x'xx => _ ==>[ make_total_cell (pr1 x'xx) (pr2 x'xx)] _)); cbn. - apply disp_id2_left. - apply (disp_id2_left (pr2 ηη)). - apply disp_id2_right. - apply (disp_id2_right (pr2 ηη)). - apply disp_vassocr. - apply (disp_vassocr (pr2 ηη) (pr2 φφ) (pr2 ψψ)). - apply disp_lwhisker_id2. - apply (disp_lwhisker_id2 (pr2 ff) (pr2 gg)). - apply disp_id2_rwhisker. - apply (disp_id2_rwhisker (pr2 ff) (pr2 gg)). - apply disp_lwhisker_vcomp. - apply (disp_lwhisker_vcomp (ff := (pr2 ff)) (pr2 ηη) (pr2 φφ)). - apply disp_rwhisker_vcomp. - apply (disp_rwhisker_vcomp (ii := pr2 ii) (pr2 ηη) (pr2 φφ)). - apply disp_vcomp_lunitor. - apply (disp_vcomp_lunitor (pr2 ηη)). - apply disp_vcomp_runitor. - apply (disp_vcomp_runitor (pr2 ηη)). - apply disp_lwhisker_lwhisker. - apply (disp_lwhisker_lwhisker (pr2 ff) (pr2 gg) (pr2 ηη)). - apply disp_rwhisker_lwhisker. - apply (disp_rwhisker_lwhisker (pr2 ff) (pr2 ii) (pr2 ηη)). - apply disp_rwhisker_rwhisker. - apply (disp_rwhisker_rwhisker _ _ (pr2 hh) (pr2 ii) (pr2 ηη)). - apply disp_vcomp_whisker. - apply (disp_vcomp_whisker _ _ _ _ _ (pr2 ff) (pr2 gg) (pr2 hh) (pr2 ii) (pr2 ηη) (pr2 φφ)). - apply disp_lunitor_linvunitor. - apply (disp_lunitor_linvunitor (pr2 ff)). - apply disp_linvunitor_lunitor. - apply (disp_linvunitor_lunitor (pr2 ff)). - apply disp_runitor_rinvunitor. - apply (disp_runitor_rinvunitor (pr2 ff)). - apply disp_rinvunitor_runitor. - apply (disp_rinvunitor_runitor (pr2 ff)). - apply disp_lassociator_rassociator. - apply (disp_lassociator_rassociator (pr2 ff) (pr2 gg) (pr2 hh)). - apply disp_rassociator_lassociator. - apply (disp_rassociator_lassociator _ (pr2 ff) (pr2 gg) (pr2 hh)). - apply disp_runitor_rwhisker. - apply (disp_runitor_rwhisker (pr2 ff) (pr2 gg)). - apply disp_lassociator_lassociator. - apply (disp_lassociator_lassociator (pr2 ff) (pr2 gg) (pr2 hh) (pr2 ii)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.Bicategories.Core.Bicat UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Core.AdjointUnique UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.DisplayedBicats.DispAdjunctions UniMath.Bicategories.DisplayedBicats.DispUnivalence