Definition strict_fiber_bicat_data : prebicat_data. Proof. exists strict_fiber_bicat_1_id_comp_cells. repeat split; cbn. - intros. exact (disp_id2 _). - intros d d' ff. set (PP := disp_local_iso_cleaving_invertible_2cell h (id_disp d;; ff) (idempunitor c)). set (RR := PP •• disp_lunitor ff). assert (Heq : (idempunitor c) • lunitor (identity c) = id2 (identity c)). { abstract (apply linvunitor_lunitor). } exact (transportf (λ x, _ ==>[x] _) Heq RR). - intros d d' ff. assert (Heq : (idempunitor c) • runitor (identity c) = id2 (identity c)). { abstract (cbn ; rewrite <- lunitor_runitor_identity, linvunitor_lunitor ; reflexivity). } set (PP := disp_local_iso_cleaving_invertible_2cell h (ff;; id_disp d') (idempunitor c)). exact (transportf (λ x, _ ==>[x] _) Heq (PP •• disp_runitor ff)). - intros d d' ff. set (PP := disp_inv_cell (disp_local_iso_cleaving_invertible_2cell h (id_disp d;; ff) (idempunitor c))). assert (Heq : linvunitor (identity c) • (idempunitor c)^-1 = id2 (identity c)). { abstract (apply linvunitor_lunitor). } exact (transportf (λ x, _ ==>[x] _) Heq (disp_linvunitor ff •• PP)). - cbn. intros d d' ff. set (PP := disp_inv_cell (disp_local_iso_cleaving_invertible_2cell h (ff;; id_disp d') (idempunitor c))). assert (Heq : rinvunitor (identity c) • (idempunitor c)^-1 = id2 (identity c)). { unfold idempunitor. cbn. abstract (rewrite lunitor_runitor_identity, rinvunitor_runitor ; reflexivity). } exact (transportf (λ x, _ ==>[x] _) Heq (disp_rinvunitor ff •• PP)). - intros d0 d1 d2 d3 ff gg hh. assert (((idempunitor c) • ((idempunitor c) ▹ identity c)) • rassociator _ _ _ • ((identity c ◃ lunitor _) • lunitor _) = id2 _) as Heq. { abstract (cbn ; rewrite !lwhisker_hcomp, !rwhisker_hcomp ; rewrite lunitor_V_id_is_left_unit_V_id ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)) ; rewrite <- triangle_l_inv ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)) ; rewrite lassociator_rassociator, id2_left ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite <- hcomp_vcomp ; rewrite id2_left, linvunitor_lunitor ; rewrite hcomp_identity, id2_left ; rewrite <- lunitor_V_id_is_left_unit_V_id ; rewrite linvunitor_lunitor ; reflexivity ). } refine (transportf (λ z, _ ==>[ z ] _) Heq _). cbn. refine (_ •• disp_rassociator ff gg hh •• _). + refine (disp_local_iso_cleaving_invertible_2cell h (local_iso_cleaving_1cell h (ff;; gg) (idempunitor c);; hh) (idempunitor c) •• _). refine (disp_rwhisker _ _). exact (disp_local_iso_cleaving_invertible_2cell h (ff ;; gg) (idempunitor c)). + refine (_ •• _). * refine (disp_lwhisker _ _). exact (disp_inv_cell (disp_local_iso_cleaving_invertible_2cell h (gg ;; hh) (idempunitor c))). * exact (disp_inv_cell ((disp_local_iso_cleaving_invertible_2cell h (ff;;local_iso_cleaving_1cell h (gg;; hh) (idempunitor c)) (idempunitor c)))). - intros d0 d1 d2 d3 ff gg hh. assert (((idempunitor c) • (identity c ◃ (idempunitor c))) • lassociator _ _ _ • ((lunitor _ ▹ identity c) • lunitor _) = id2 _) as Heq. { abstract (cbn ; rewrite !lwhisker_hcomp, !rwhisker_hcomp ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)) ; rewrite triangle_r_inv ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)) ; rewrite rassociator_lassociator, id2_left ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite <- hcomp_vcomp ; rewrite <- lunitor_V_id_is_left_unit_V_id ; rewrite id2_left, linvunitor_lunitor ; rewrite hcomp_identity, id2_left ; apply linvunitor_lunitor ). } refine (transportf (λ z, _ ==>[ z ] _) Heq _). cbn. refine (_ •• disp_lassociator ff gg hh •• _). + refine (_ •• _). * exact (disp_local_iso_cleaving_invertible_2cell h (ff;;local_iso_cleaving_1cell h (gg;; hh) (idempunitor c)) (idempunitor c)). * refine (disp_lwhisker _ _). exact (disp_local_iso_cleaving_invertible_2cell h (gg ;; hh) (idempunitor c)). + refine (_ •• _). * refine (disp_rwhisker _ _). exact (disp_inv_cell (disp_local_iso_cleaving_invertible_2cell h (ff ;; gg) (idempunitor c))). * exact (disp_inv_cell (disp_local_iso_cleaving_invertible_2cell h (local_iso_cleaving_1cell h (ff;; gg) (idempunitor c);; hh) (idempunitor c))). - intros a b f1 f2 f3 x y. exact (transportf (λ z, _ ==>[ z ] _) (id2_left _) (x •• y)). - intros a1 a2 a3 f g1 g2 x. assert (linvunitor _ • (identity c ◃ id2 _) • lunitor _ = id2 (identity c)) as Heq. { abstract (rewrite lwhisker_id2 ; rewrite id2_right ; apply linvunitor_lunitor). } refine (transportf (λ z, _ ==>[ z ] _) Heq _). refine (_ •• (f ◃◃ x) •• _). + exact (disp_local_iso_cleaving_invertible_2cell h (f ;; g1) (idempunitor c)). + exact (disp_inv_cell (disp_local_iso_cleaving_invertible_2cell h (f ;; g2) (idempunitor c))). - intros a1 a2 a3 f1 f2 g x. assert (linvunitor _ • (id2 _ ▹ identity _) • lunitor _ = id2 (identity c)) as Heq. { abstract (rewrite id2_rwhisker ; rewrite id2_right ; apply linvunitor_lunitor). } refine (transportf (λ z, _ ==>[ z ] _) Heq _). refine (_ •• (x ▹▹ g) •• _). + exact (disp_local_iso_cleaving_invertible_2cell h (f1 ;; g) (idempunitor c)). + exact (disp_inv_cell (disp_local_iso_cleaving_invertible_2cell h (f2 ;; g) (idempunitor c))). 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.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat. Require Import UniMath.Bicategories.DisplayedBicats.FiberCategory.