Lemma sigma_prebicat_laws : disp_prebicat_laws sigma_bicat_data. 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.
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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.