(* ******************************************************************************* *) (** * Bicategories Benedikt Ahrens, Marco Maggesi February 2018 ********************************************************************************* *) 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. Local Open Scope cat. Local Open Scope mor_disp_scope. Section Strict_Fiber_Bicat. Context {C : bicat} (D : disp_prebicat C) (h : local_iso_cleaving D) (c : C). Definition strict_fiber_bicat_1_id_comp_cells : prebicat_1_id_comp_cells. Proof. exists (discrete_fiber_precategory_data D h c). red. cbn. intros d d' f f'. exact (f ==>[id2 (identity c)] f'). Defined. 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. Local Arguments transportf {_} {_} {_} {_} {_} _. Local Arguments transportb {_} {_} {_} {_} {_} _. Definition strict_fiber_bicat_data_laws_vcomp_left : ∏ (a b : strict_fiber_bicat_data) (f g : strict_fiber_bicat_data ⟦ a, b ⟧) (x : f ==> g), id₂ f • x = x. Proof. intros a b f g x ; cbn. rewrite disp_id2_left. rewrite transportfbinv. reflexivity. Qed. Definition strict_fiber_bicat_data_laws_vcomp_right : ∏ (a b : strict_fiber_bicat_data) (f g : strict_fiber_bicat_data ⟦ a, b ⟧) (x : f ==> g), x • id₂ g = x. Proof. intros a b f g x ; cbn. rewrite disp_id2_right. unfold transportb. rewrite transport_f_f. rewrite transportf_set. - reflexivity. - apply C. Qed. Definition strict_fiber_bicat_data_laws_vcomp_assoc : ∏ (a b : strict_fiber_bicat_data) (f₁ f₂ f₃ f₄ : strict_fiber_bicat_data ⟦ a, b ⟧) (x : f₁ ==> f₂) (y : f₂ ==> f₃) (z : f₃ ==> f₄), x • (y • z) = (x • y) • z. Proof. intros a b f₁ f₂ f₃ f₄ x y z ; cbn. rewrite disp_mor_transportf_prewhisker. rewrite disp_vassocr. rewrite disp_mor_transportf_postwhisker. unfold transportb. rewrite !transport_f_f. apply (@transportf_paths _ (λ α : id₁ c ==> id₁ c, f₁ ==>[ α] f₄)). apply C. Qed. Definition strict_fiber_bicat_data_laws_rwhisker_id2 : ∏ (a₁ a₂ a₃ : strict_fiber_bicat_data) (f : strict_fiber_bicat_data ⟦ a₁ , a₂ ⟧) (g : strict_fiber_bicat_data ⟦ a₂, a₃ ⟧), f ◃ id₂ g = id₂ (f · g). Proof. intros a₁ a₂ a₃ f g ; cbn. rewrite disp_lwhisker_id2. unfold transportb. rewrite disp_mor_transportf_prewhisker. rewrite disp_mor_transportf_postwhisker. rewrite transport_f_f. rewrite disp_id2_right. unfold transportb. rewrite disp_mor_transportf_postwhisker. rewrite transport_f_f. apply (@transportf_transpose_left _ (λ α : id₁ c ==> id₁ c, _ ==>[ α] _)). refine (disp_vcomp_rinv (disp_local_iso_cleaving_invertible_2cell h (f;; g) (idempunitor c)) @ _). unfold transportb. apply (@transportf_paths _ (λ α : id₁ c ==> id₁ c, _ ==>[ α] _)). apply C. Qed. Definition strict_fiber_bicat_data_laws_id2_lwhisker : ∏ (a₁ a₂ a₃ : strict_fiber_bicat_data) (f : strict_fiber_bicat_data ⟦ a₁ , a₂ ⟧) (g : strict_fiber_bicat_data ⟦ a₂ , a₃ ⟧), id₂ f ▹ g = id₂ (f · g). Proof. intros a₁ a₂ a₃ f g ; cbn. rewrite disp_id2_rwhisker. unfold transportb. rewrite disp_mor_transportf_prewhisker. rewrite disp_mor_transportf_postwhisker. rewrite transport_f_f. rewrite disp_id2_right. unfold transportb. rewrite disp_mor_transportf_postwhisker. rewrite transport_f_f. apply (@transportf_transpose_left _ (λ α : id₁ c ==> id₁ c, _ ==>[ α] _)). refine (disp_vcomp_rinv (disp_local_iso_cleaving_invertible_2cell h (f;; g) (idempunitor c)) @ _). unfold transportb. apply (@transportf_paths _ (λ α : id₁ c ==> id₁ c, _ ==>[ α] _)). apply C. Qed. Definition strict_fiber_bicat_data_laws_vcomp_lwhisker : ∏ (a₁ a₂ a₃ : strict_fiber_bicat_data) (f : strict_fiber_bicat_data ⟦ a₁ , a₂ ⟧) (g₁ g₂ g₃ : strict_fiber_bicat_data ⟦ a₂ , a₃ ⟧) (x : g₁ ==> g₂) (y : g₂ ==> g₃), (f ◃ x) • (f ◃ y) = f ◃ (x • y). Proof. intros a₁ a₂ a₃ f g₁ g₂ g₃ x y ; cbn. etrans. { apply maponpaths. etrans. { apply disp_mor_transportf_prewhisker. } apply maponpaths. apply disp_mor_transportf_postwhisker. } do 2 refine (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _) _ _ _ _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). apply maponpaths. etrans. { apply maponpaths_2. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f;; g₂) (idempunitor c))). } etrans. { apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths_2. apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply disp_lwhisker_vcomp. } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } refine (!_). etrans. { apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths. apply disp_rwhisker_transport_right. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_postwhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. apply disp_vassocl. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transportf_paths _ (λ α : id₁ c ==> id₁ c, _ ==>[ α] _)). apply C. Qed. Definition strict_fiber_bicat_data_laws_vcomp_rwhisker : ∏ (a₁ a₂ a₃ : strict_fiber_bicat_data) (f₁ f₂ f₃ : strict_fiber_bicat_data ⟦ a₁ , a₂ ⟧) (g : strict_fiber_bicat_data ⟦ a₂ , a₃ ⟧) (x : f₁ ==> f₂) (y : f₂ ==> f₃), (x ▹ g) • (y ▹ g) = (x • y) ▹ g. Proof. intros a₁ a₂ a₃ f₁ f₂ f₃ f₄ x y ; cbn. etrans. { apply maponpaths. etrans. { apply disp_mor_transportf_postwhisker. } apply maponpaths. apply disp_mor_transportf_prewhisker. } do 2 refine (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _) _ _ _ _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). apply maponpaths. etrans. { apply maponpaths_2. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f₂;; f₄) (idempunitor c))). } etrans. { apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths_2. apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocl _ _ _ @ _). apply maponpaths. etrans. { apply maponpaths. apply disp_rwhisker_vcomp. } apply disp_mor_transportf_prewhisker. } etrans. { apply maponpaths_2. apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } refine (!_). etrans. { apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths. apply disp_rwhisker_transport_left_new. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_postwhisker. } refine (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _) _ _ _ _ _ _ @ _). apply (@transportf_paths _ (λ α : id₁ c ==> id₁ c, _ ==>[ α] _)). apply C. Qed. Definition strict_fiber_bicat_data_laws_vcomp_lunitor : ∏ (a b : strict_fiber_bicat_data) (f g : strict_fiber_bicat_data ⟦ a, b ⟧) (x : f ==> g), (id₁ a ◃ x) • lunitor g = lunitor f • x. Proof. intros a b f g x ; cbn. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. rewrite !disp_mor_transportf_postwhisker. rewrite !transport_f_f. etrans. { apply maponpaths. rewrite disp_vassocl. do 2 apply maponpaths. rewrite disp_vassocr. apply maponpaths. apply maponpaths_2. apply (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (id_disp a;; g) (idempunitor c))). } unfold transportb. rewrite transport_f_f. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. rewrite disp_mor_transportf_postwhisker. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. etrans. { do 2 apply maponpaths. apply disp_id2_left. } unfold transportb. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. etrans. { apply maponpaths. rewrite disp_vassocl. do 2 apply maponpaths. apply disp_vcomp_lunitor. } unfold transportb. rewrite transport_f_f. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. refine (_ @ _). { apply maponpaths. apply disp_vassocr. } unfold transportb. rewrite transport_f_f. apply (@transportf_paths _ (λ α : id₁ c ==> id₁ c, _ ==>[ α] _)). apply C. Qed. Definition strict_fiber_bicat_data_laws_vcomp_runitor : ∏ (a b : strict_fiber_bicat_data) (f g : strict_fiber_bicat_data ⟦ a, b ⟧) (x : f ==> g), (x ▹ id₁ b) • runitor g = runitor f • x. Proof. intros a b f g x ; cbn. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. rewrite !disp_mor_transportf_postwhisker. rewrite !transport_f_f. etrans. { apply maponpaths. rewrite disp_vassocl. do 2 apply maponpaths. rewrite disp_vassocr. apply maponpaths. apply maponpaths_2. apply (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (g;;id_disp b) (idempunitor c))). } unfold transportb. rewrite transport_f_f. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. rewrite disp_mor_transportf_postwhisker. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. etrans. { do 2 apply maponpaths. apply disp_id2_left. } unfold transportb. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. etrans. { apply maponpaths. rewrite disp_vassocl. do 2 apply maponpaths. apply disp_vcomp_runitor. } unfold transportb. rewrite transport_f_f. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. refine (_ @ _). { apply maponpaths. apply disp_vassocr. } unfold transportb. rewrite transport_f_f. apply (@transportf_paths _ (λ α : id₁ c ==> id₁ c, _ ==>[ α] _)). apply C. Qed. Definition strict_fiber_bicat_data_laws_lwhisker_lwhisker : ∏ (a₁ a₂ a₃ a₄ : strict_fiber_bicat_data) (f₁ : strict_fiber_bicat_data ⟦ a₁ , a₂ ⟧) (f₂ : strict_fiber_bicat_data ⟦ a₂ , a₃ ⟧) (f₃ f₄ : strict_fiber_bicat_data ⟦ a₃ , a₄ ⟧) (x : f₃ ==> f₄), (f₁ ◃ (f₂ ◃ x)) • lassociator f₁ f₂ f₄ = lassociator f₁ f₂ f₃ • (f₁ · f₂ ◃ x). Proof. intros a₁ a₂ a₃ a₄ f₁ f₂ g₁ g₂ x ; cbn. etrans. { apply maponpaths. etrans. { apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. apply disp_mor_transportf_prewhisker. } do 2 apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths_2. etrans. { apply maponpaths. apply disp_rwhisker_transport_right. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_postwhisker. } refine (!_). etrans. { apply maponpaths. etrans. { apply disp_mor_transportf_postwhisker. } apply maponpaths. apply disp_mor_transportf_prewhisker. } refine (!_). do 3 (refine (@transport_f_f _ (λ z : id₁ c ==> id₁ c, _ ==>[ z ] _) _ _ _ _ _ _ @ _)). do 2 refine (_ @ !(@transport_f_f _ (λ z : id₁ c ==> id₁ c, _ ==>[ z ] _) _ _ _ _ _ _)). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f₁;; local_iso_cleaving_1cell h (f₂;; g₂) (idempunitor c)) (idempunitor c))). } etrans. { apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply disp_lwhisker_vcomp. } apply maponpaths. etrans. { apply maponpaths. apply disp_vassocl. } etrans. { apply disp_rwhisker_transport_right. } etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f₂;; g₂) (idempunitor c))). } etrans. { apply disp_mor_transportf_prewhisker. } etrans. { apply maponpaths. apply disp_id2_right. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_rwhisker_transport_right. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths_2. apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths_2. etrans. { apply maponpaths_2. apply disp_lwhisker_vcomp_alt. } etrans. { apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. apply disp_lwhisker_lwhisker. } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_prewhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. apply disp_vcomp_whisker_alt. } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_prewhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } refine (!_). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (local_iso_cleaving_1cell h (f₁;; f₂) (idempunitor c);; g₁) (idempunitor c))). } etrans. { apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. etrans. { etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths. apply disp_vassocr. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_prewhisker. } etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths. apply disp_vassocr. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_prewhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply maponpaths. etrans. { apply maponpaths. apply disp_vassocr. } apply disp_mor_transportf_prewhisker. } do 2 refine (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _) _ _ _ _ _ _ @ _). apply (@transportf_paths _ (λ α : id₁ c ==> id₁ c, _ ==>[ α] _)). apply cellset_property. Qed. Definition strict_fiber_bicat_data_laws_rwhisker_lwhisker : ∏ (a₁ a₂ a₃ a₄ : strict_fiber_bicat_data) (f₁ : strict_fiber_bicat_data ⟦ a₁ , a₂ ⟧) (f₂ f₃ : strict_fiber_bicat_data ⟦ a₂ , a₃ ⟧) (f₄ : strict_fiber_bicat_data ⟦ a₃ , a₄ ⟧) (x : f₂ ==> f₃), (f₁ ◃ (x ▹ f₄)) • lassociator f₁ f₃ f₄ = lassociator f₁ f₂ f₄ • ((f₁ ◃ x) ▹ f₄). Proof. intros a₁ a₂ a₃ a₄ f₁ f₂ f₃ f₄ x ; cbn. etrans. { apply maponpaths. etrans. { apply disp_mor_transportf_postwhisker. } apply maponpaths. etrans. { apply disp_mor_transportf_prewhisker. } apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths_2. etrans. { apply maponpaths. apply disp_rwhisker_transport_right. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_postwhisker. } refine (!_). etrans. { apply maponpaths. etrans. { apply disp_mor_transportf_postwhisker. } apply maponpaths. apply disp_mor_transportf_prewhisker. } refine (!_). do 3 (refine (@transport_f_f _ (λ z : id₁ c ==> id₁ c, _ ==>[ z ] _) _ _ _ _ _ _ @ _)). do 2 refine (_ @ !(@transport_f_f _ (λ z : id₁ c ==> id₁ c, _ ==>[ z ] _) _ _ _ _ _ _)). etrans. { apply maponpaths. etrans. { refine (disp_vassocl _ _ _ @ _). apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f₁;; local_iso_cleaving_1cell h (f₃;; f₄) (idempunitor c)) (idempunitor c))). } etrans. { apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_lwhisker_vcomp _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f₃;; f₄) (idempunitor c))). } apply disp_mor_transportf_prewhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. apply disp_id2_right. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_rwhisker_transport_right. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_postwhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths_2. etrans. { apply maponpaths_2. apply disp_lwhisker_vcomp_alt. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_prewhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths_2. refine (disp_vassocl _ _ _ @ _). do 2 apply maponpaths. apply disp_rwhisker_lwhisker. } unfold transportb. apply disp_mor_transportf_postwhisker. } etrans. { apply disp_mor_transportf_postwhisker. } apply maponpaths. do 2 apply maponpaths_2. apply disp_mor_transportf_prewhisker. } etrans. { apply disp_mor_transportf_prewhisker. } apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_prewhisker. } do 2 refine (@transport_f_f _ (λ z : id₁ c ==> id₁ c, _ ==>[ z ] _) _ _ _ _ _ _ @ _). refine (!_). etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths. apply disp_rwhisker_transport_left_new. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_prewhisker. } refine (@transport_f_f _ (λ z : id₁ c ==> id₁ c, _ ==>[ z ] _) _ _ _ _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (local_iso_cleaving_1cell h (f₁;; f₂) (idempunitor c);; f₄) (idempunitor c))). } etrans. { apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply disp_rwhisker_vcomp. } etrans. { apply disp_mor_transportf_postwhisker. } apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f₁;; f₂) (idempunitor c))). } etrans. { apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply disp_rwhisker_transport_left_new. } etrans. { apply maponpaths. apply disp_rwhisker_vcomp_alt. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } refine (!_). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. apply disp_vassocr. } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transportf_paths _ (λ α : id₁ c ==> id₁ c, _ ==>[ α] _)). apply cellset_property. Qed. Definition strict_fiber_bicat_data_laws_rwhisker_rwhisker : ∏ (a₁ a₂ a₃ a₄ : strict_fiber_bicat_data) (f₁ f₂ : strict_fiber_bicat_data ⟦ a₁ , a₂ ⟧) (f₃ : strict_fiber_bicat_data ⟦ a₂ , a₃ ⟧) (f₄ : strict_fiber_bicat_data ⟦ a₃ , a₄ ⟧) (x : f₁ ==> f₂), lassociator f₁ f₃ f₄ • ((x ▹ f₃) ▹ f₄) = (x ▹ f₃ · f₄) • lassociator f₂ f₃ f₄. Proof. intros a₁ a₂ a₃ a₄ f₁ f₂ f₃ f₄ x ; cbn. etrans. { apply maponpaths. etrans. { apply disp_mor_transportf_postwhisker. } apply maponpaths. etrans. { apply disp_mor_transportf_prewhisker. } apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths. apply disp_rwhisker_transport_left_new. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_prewhisker. } do 3 refine (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _) _ _ _ _ _ _ @ _). refine (!_). etrans. { apply maponpaths. etrans. { apply disp_mor_transportf_postwhisker. } apply maponpaths. apply disp_mor_transportf_prewhisker. } do 2 refine (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _) _ _ _ _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f₂;; local_iso_cleaving_1cell h (f₃;; f₄) (idempunitor c)) (idempunitor c))). } apply disp_mor_transportf_postwhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply maponpaths. apply disp_id2_left. } etrans. { apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } do 2 refine (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _) _ _ _ _ _ _ @ _). refine (!_). etrans. { apply maponpaths. etrans. { refine (disp_vassocl _ _ _ @ _). apply maponpaths. etrans. { apply maponpaths. etrans. { refine (disp_vassocr _ _ _ @ _). apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (local_iso_cleaving_1cell h (f₁;; f₃) (idempunitor c);; f₄) (idempunitor c))). } apply disp_mor_transportf_postwhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply disp_rwhisker_vcomp. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f₁;; f₃) (idempunitor c))). } etrans. { apply disp_mor_transportf_postwhisker. } apply maponpaths. apply disp_id2_left. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_rwhisker_transport_left_new. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_prewhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply disp_rwhisker_vcomp_alt. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_prewhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply disp_rwhisker_rwhisker. } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply disp_vcomp_whisker_alt. } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } refine (!_). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths_2. apply disp_vassocr. } apply disp_mor_transportf_postwhisker. } apply disp_mor_transportf_postwhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transportf_paths _ (λ α : id₁ c ==> id₁ c, _ ==>[ α] _)). apply cellset_property. Qed. Definition strict_fiber_bicat_data_vcomp_whisker : ∏ (a₁ a₂ a₃ : strict_fiber_bicat_data) (f₁ f₂ : strict_fiber_bicat_data ⟦ a₁ , a₂ ⟧) (g₁ g₂ : strict_fiber_bicat_data ⟦ a₂ , a₃ ⟧) (x : f₁ ==> f₂) (y : g₁ ==> g₂), (x ▹ g₁) • (f₂ ◃ y) = (f₁ ◃ y) • (x ▹ g₂). Proof. intros a₁ a₂ a₃ f₁ f₂ g₁ g₂ x y ; cbn. etrans. { apply maponpaths. etrans. { apply disp_mor_transportf_prewhisker. } etrans. { apply maponpaths. apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } refine (!_). etrans. { apply maponpaths. etrans. { apply disp_mor_transportf_prewhisker. } etrans. { apply maponpaths. apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. etrans. { refine (disp_vassocl _ _ _ @ _). apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f₁;; g₂) (idempunitor c))). } apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } refine (!_). etrans. { apply maponpaths. etrans. { refine (disp_vassocl _ _ _ @ _). apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f₂;; g₁) (idempunitor c))). } apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply disp_vcomp_whisker. } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } refine (!_). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. apply disp_vassocr. } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transportf_paths _ (λ α : id₁ c ==> id₁ c, _ ==>[ α] _)). apply cellset_property. Qed. Definition strict_fiber_bicat_data_laws_lunitor_linvunitor : ∏ (a b : strict_fiber_bicat_data) (f : strict_fiber_bicat_data ⟦ a, b ⟧), lunitor f • linvunitor f = id₂ (id₁ a · f). Proof. intros a b f ; cbn. rewrite disp_mor_transportf_prewhisker. rewrite !transport_f_f. rewrite disp_mor_transportf_postwhisker. rewrite !transport_f_f. etrans. { apply maponpaths. rewrite disp_vassocl. do 2 apply maponpaths. rewrite disp_vassocr. apply maponpaths, maponpaths_2. apply disp_lunitor_linvunitor. } unfold transportb. rewrite transport_f_f. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. rewrite disp_mor_transportf_postwhisker. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. etrans. { do 2 apply maponpaths. apply disp_id2_left. } unfold transportb. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. etrans. { apply maponpaths. apply (disp_vcomp_rinv (disp_local_iso_cleaving_invertible_2cell h (id_disp a;; f) (idempunitor c))). } unfold transportb. rewrite transport_f_f. apply (transportf_set (λ α : id₁ c ==> id₁ c, _ ==>[ α] _) _). apply C. Qed. Definition strict_fiber_bicat_data_laws_linvunitor_lunitor : ∏ (a b : strict_fiber_bicat_data) (f : strict_fiber_bicat_data ⟦ a, b ⟧), linvunitor f • lunitor f = id₂ f. Proof. intros a b f ; cbn. rewrite disp_mor_transportf_prewhisker. rewrite !transport_f_f. rewrite disp_mor_transportf_postwhisker. rewrite !transport_f_f. etrans. { apply maponpaths. rewrite disp_vassocl. do 2 apply maponpaths. rewrite disp_vassocr. apply maponpaths, maponpaths_2. apply (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (id_disp a;; f) (idempunitor c))). } unfold transportb. rewrite transport_f_f. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. rewrite disp_mor_transportf_postwhisker. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. etrans. { do 2 apply maponpaths. apply disp_id2_left. } unfold transportb. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. etrans. { apply maponpaths. apply disp_linvunitor_lunitor. } unfold transportb. rewrite transport_f_f. apply (transportf_set (λ α : id₁ c ==> id₁ c, _ ==>[ α] _) _). apply C. Qed. Definition strict_fiber_bicat_data_laws_runitor_rinvunitor : ∏ (a b : strict_fiber_bicat_data) (f : strict_fiber_bicat_data ⟦ a, b ⟧), runitor f • rinvunitor f = id₂ (f · id₁ b). Proof. intros a b f ; cbn. rewrite disp_mor_transportf_prewhisker. rewrite !transport_f_f. rewrite disp_mor_transportf_postwhisker. rewrite !transport_f_f. etrans. { apply maponpaths. rewrite disp_vassocl. do 2 apply maponpaths. rewrite disp_vassocr. apply maponpaths, maponpaths_2. apply disp_runitor_rinvunitor. } unfold transportb. rewrite transport_f_f. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. rewrite disp_mor_transportf_postwhisker. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. etrans. { do 2 apply maponpaths. apply disp_id2_left. } unfold transportb. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. etrans. { apply maponpaths. apply (disp_vcomp_rinv (disp_local_iso_cleaving_invertible_2cell h (f ;; id_disp b) (idempunitor c))). } unfold transportb. rewrite transport_f_f. apply (transportf_set (λ α : id₁ c ==> id₁ c, _ ==>[ α] _) _). apply C. Qed. Definition strict_fiber_bicat_data_laws_rinvunitor_runitor : ∏ (a b : strict_fiber_bicat_data) (f : strict_fiber_bicat_data ⟦ a, b ⟧), rinvunitor f • runitor f = id₂ f. Proof. intros a b f ; cbn. rewrite disp_mor_transportf_prewhisker. rewrite !transport_f_f. rewrite disp_mor_transportf_postwhisker. rewrite !transport_f_f. etrans. { apply maponpaths. rewrite disp_vassocl. do 2 apply maponpaths. rewrite disp_vassocr. apply maponpaths, maponpaths_2. apply (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f ;; id_disp b) (idempunitor c))). } unfold transportb. rewrite transport_f_f. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. rewrite disp_mor_transportf_postwhisker. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. etrans. { do 2 apply maponpaths. apply disp_id2_left. } unfold transportb. rewrite disp_mor_transportf_prewhisker. rewrite transport_f_f. etrans. { apply maponpaths. apply disp_rinvunitor_runitor. } unfold transportb. rewrite transport_f_f. apply (transportf_set (λ α : id₁ c ==> id₁ c, _ ==>[ α] _) _). apply C. Qed. Definition strict_fiber_bicat_data_laws_lassociator_rassociator : ∏ (a₁ a₂ a₃ a₄ : strict_fiber_bicat_data) (f₁ : strict_fiber_bicat_data ⟦ a₁ , a₂ ⟧) (f₂ : strict_fiber_bicat_data ⟦ a₂ , a₃ ⟧) (f₃ : strict_fiber_bicat_data ⟦ a₃ , a₄ ⟧), lassociator f₁ f₂ f₃ • rassociator f₁ f₂ f₃ = id₂ (f₁ · (f₂ · f₃)). Proof. intros a₁ a₂ a₃ a₄ f₁ f₂ f₃ ; cbn. etrans. { apply maponpaths. etrans. { apply disp_mor_transportf_prewhisker. } apply maponpaths. apply disp_mor_transportf_postwhisker. } do 2 refine (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _) _ _ _ _ _ _ @ _). etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (local_iso_cleaving_1cell h (f₁;; f₂) (idempunitor c);; f₃) (idempunitor c))). } apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. refine (disp_vassocl _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. refine (disp_rwhisker_vcomp _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths. exact (disp_vcomp_linv (disp_local_iso_cleaving_invertible_2cell h (f₁;; f₂) (idempunitor c))). } apply disp_rwhisker_transport_left_new. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. apply disp_id2_rwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply disp_lassociator_rassociator. } apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. etrans. { refine (disp_vassocl _ _ _ @ _). apply maponpaths. etrans. { apply maponpaths. refine (disp_vassocr _ _ _ @ _). etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply disp_lwhisker_vcomp. } apply disp_mor_transportf_postwhisker. } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. etrans. { apply maponpaths_2. etrans. { apply maponpaths. exact (disp_vcomp_rinv (disp_local_iso_cleaving_invertible_2cell h (f₂;; f₃) (idempunitor c))). } etrans. { apply disp_rwhisker_transport_right. } etrans. { apply maponpaths. apply disp_lwhisker_id2. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_postwhisker. } etrans. { apply maponpaths. etrans. { apply maponpaths. apply disp_id2_left. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply disp_mor_transportf_prewhisker. } apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } etrans. { apply maponpaths. exact (disp_vcomp_rinv (disp_local_iso_cleaving_invertible_2cell h (f₁;; local_iso_cleaving_1cell h (f₂;; f₃) (idempunitor c)) (idempunitor c))). } etrans. { apply (@transport_f_f _ (λ z : _ ==> _, _ ==>[ z ] _)). } apply (transportf_set (λ α : id₁ c ==> id₁ c, _ ==>[ α] _) _). apply C. Qed. End Strict_Fiber_Bicat.