Lemma has_inserter_ump_2_left_adjoint_equivalence_cell_path : rassociator _ _ _ • (_ ◃ inserter_cone_cell cone₁) • lassociator _ _ _ • (cell ▹ _) = (cell ▹ _) • rassociator _ _ _ • (_ ◃ inserter_cone_cell cone₁) • lassociator _ _ _. Proof. rewrite !vassocl. use (adj_equiv_faithful Hly). rewrite <- !rwhisker_vcomp. use (vcomp_rcancel (rassociator _ _ _)) ; [ is_iso | ]. rewrite !vassocl. rewrite rwhisker_rwhisker_alt. use (vcomp_rcancel (_ ◃ γ₃^-1)) ; [ is_iso | ]. rewrite !vassocl. rewrite vcomp_whisker. use (vcomp_rcancel (lassociator _ _ _)) ; [ is_iso | ]. rewrite !vassocl. rewrite <- rwhisker_rwhisker. use (vcomp_lcancel (lassociator _ _ _)) ; [ is_iso | ]. rewrite !vassocr. rewrite rwhisker_rwhisker. use (vcomp_lcancel (_ ◃ γ₂)). { is_iso. apply property_from_invertible_2cell. } rewrite !vassocr. rewrite <- vcomp_whisker. use (vcomp_lcancel (rassociator _ _ _)) ; [ is_iso | ]. rewrite !vassocr. rewrite <- rwhisker_rwhisker_alt. rewrite !vassocl. cbn -[cell]. cbn in p. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite inverse_pentagon_7. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_lwhisker. rewrite !vassocl. apply idpath. } etrans. { etrans. { apply maponpaths. rewrite !vassocr. rewrite <- lwhisker_lwhisker_rassociator. apply idpath. } rewrite !vassocr. rewrite <- rassociator_rassociator. rewrite !vassocl. apply idpath. } etrans. { do 5 apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite pentagon_6. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite lassociator_rassociator. rewrite id2_left. rewrite !vassocl. apply idpath. } do 2 apply maponpaths. rewrite !vassocr. rewrite <- lwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- lassociator_lassociator. rewrite !vassocl. rewrite !rwhisker_vcomp. apply idpath. } etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite !lwhisker_vcomp. rewrite !vassocl. apply idpath. } etrans. { do 2 apply maponpaths. apply maponpaths_2. apply maponpaths. assert (rassociator _ _ _ • (_ ◃ γ₂) • lassociator _ _ _ • (α₁ ▹ _) • rassociator _ _ _ • (_ ◃ γ₃^-1) • lassociator _ _ _ = (γ₁^-1 ▹ _) • rassociator _ _ _ • (_ ◃ α₂) • lassociator _ _ _ • (γ₁ ▹ g₂)) as H'. { do 3 (use vcomp_move_R_Mp ; [ is_iso | ]). rewrite !vassocl. do 2 (use vcomp_move_L_pM ; [ is_iso | ]). cbn. rewrite !vassocr. exact (!pα). } rewrite !vassocr. rewrite H'. rewrite !vassocl. apply idpath. } etrans. { rewrite <- !lwhisker_vcomp. rewrite !vassocl. do 5 apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_lwhisker. rewrite !vassocl. rewrite !rwhisker_vcomp. apply idpath. } rewrite !vassocr. etrans. { apply maponpaths_2. rewrite lwhisker_hcomp. rewrite pentagon_2. rewrite <- rwhisker_hcomp. apply idpath. } rewrite !vassocl. rewrite rwhisker_vcomp. apply idpath. } etrans. { do 4 apply maponpaths. rewrite !vassocr. rewrite lwhisker_lwhisker. rewrite !vassocl. apply idpath. } etrans. { do 3 apply maponpaths. rewrite !vassocr. do 3 apply maponpaths_2. rewrite lwhisker_hcomp. rewrite inverse_pentagon_5. rewrite <- rwhisker_hcomp. apply idpath. } rewrite !vassocl. etrans. { apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_lwhisker. apply idpath. } rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite !vassocl. apply idpath. } etrans. { rewrite !vassocr. rewrite !rwhisker_vcomp. rewrite !vassocl. apply idpath. } refine (!_). etrans. { do 3 apply maponpaths. rewrite !vassocr. rewrite inverse_pentagon_7. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_lwhisker. rewrite !vassocl. apply idpath. } etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite <- lwhisker_lwhisker_rassociator. rewrite !vassocl. apply idpath. } etrans. { apply maponpaths. rewrite !vassocr. rewrite <- rassociator_rassociator. rewrite !vassocl. do 2 apply maponpaths. etrans. { do 4 apply maponpaths. rewrite !vassocr. do 2 apply maponpaths_2. rewrite rwhisker_hcomp. rewrite !vassocl. rewrite <- inverse_pentagon_5. rewrite <- lwhisker_hcomp. apply idpath. } rewrite !vassocl. etrans. { do 5 apply maponpaths. rewrite !vassocr. rewrite <- lwhisker_lwhisker. rewrite !vassocl. rewrite <- lassociator_lassociator. rewrite !vassocl. apply idpath. } rewrite !vassocr. rewrite !lwhisker_vcomp. do 2 apply maponpaths_2. apply maponpaths. assert (rassociator _ _ _ • (_ ◃ γ₂) • lassociator _ _ _ • (α₁ ▹ _) • rassociator _ _ _ • (_ ◃ γ₃^-1) • lassociator _ _ _ = (γ₁^-1 ▹ _) • rassociator _ _ _ • (_ ◃ α₂) • lassociator _ _ _ • (γ₁ ▹ _)) as H'. { do 3 (use vcomp_move_R_Mp ; [ is_iso | ]). rewrite !vassocl. do 2 (use vcomp_move_L_pM ; [ is_iso | ]). cbn. rewrite !vassocr. exact (!pα). } exact H'. } etrans. { rewrite !vassocr. rewrite rwhisker_vcomp. rewrite !vassocl. rewrite <- !lwhisker_vcomp. etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_lwhisker_rassociator. apply idpath. } rewrite !vassocr. rewrite rwhisker_vcomp. rewrite !vassocl. etrans. { do 5 apply maponpaths. rewrite !vassocr. rewrite rwhisker_lwhisker. rewrite !vassocl. rewrite rwhisker_vcomp. apply idpath. } etrans. { do 4 apply maponpaths. rewrite !vassocr. etrans. { apply maponpaths_2. rewrite lwhisker_hcomp. rewrite pentagon_2. rewrite <- rwhisker_hcomp. apply idpath. } rewrite !vassocl. rewrite rwhisker_vcomp. apply idpath. } etrans. { apply maponpaths. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite lwhisker_lwhisker. rewrite !vassocl. apply idpath. } rewrite !vassocr. do 3 apply maponpaths_2. rewrite !vassocl. rewrite <- inverse_pentagon_2. rewrite <- rwhisker_hcomp. apply idpath. } rewrite !vassocr. rewrite rwhisker_vcomp. apply idpath. } rewrite !vassocl. etrans. { apply maponpaths_2. apply maponpaths. etrans. { apply maponpaths_2. apply fully_faithful_1cell_inv_map_eq. } rewrite !vassocl. etrans. { do 12 apply maponpaths. rewrite !vassocr. rewrite lassociator_rassociator. rewrite id2_left. apply idpath. } etrans. { do 11 apply maponpaths. rewrite !vassocr. rewrite lwhisker_vcomp. rewrite vcomp_rinv. rewrite lwhisker_id2. apply id2_left. } rewrite rassociator_lassociator. rewrite id2_right. apply idpath. } rewrite <- !rwhisker_vcomp. rewrite !vassocl. do 3 apply maponpaths. refine (!_). etrans. { do 3 apply maponpaths. rewrite !vassocr. rewrite !rwhisker_vcomp. apply maponpaths. etrans. { apply maponpaths. apply fully_faithful_1cell_inv_map_eq. } rewrite !vassocl. etrans. { do 2 apply maponpaths. refine (vassocr _ _ _ @ _). rewrite lassociator_rassociator. rewrite id2_left. apply idpath. } etrans. { apply maponpaths. refine (vassocr _ _ _ @ _). rewrite lwhisker_vcomp. rewrite vcomp_rinv. rewrite lwhisker_id2. rewrite id2_left. apply idpath. } refine (vassocr _ _ _ @ _). rewrite rassociator_lassociator. rewrite id2_left. apply idpath. } rewrite <- !rwhisker_vcomp. rewrite !vassocr. do 3 apply maponpaths_2. rewrite !vassocl. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker. rewrite !vassocl. apply idpath. } etrans. { apply maponpaths. rewrite !vassocr. rewrite <- vcomp_whisker. rewrite !vassocl. apply idpath. } etrans. { do 3 apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker. rewrite !vassocl. apply idpath. } etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite <- vcomp_whisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- vcomp_whisker. rewrite !vassocl. apply idpath. } use vcomp_move_R_pM ; [ is_iso | ] ; cbn -[εp]. refine (!_). etrans. { rewrite !vassocr. rewrite rwhisker_rwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker. rewrite !vassocl. apply idpath. } do 3 apply maponpaths. use vcomp_move_R_pM ; [ is_iso | ] ; cbn -[εp]. refine (!_). etrans. { rewrite !vassocr. rewrite p. rewrite !vassocl. apply idpath. } apply maponpaths. refine (!_). etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker_alt. apply idpath. } etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker_alt. apply idpath. } etrans. { rewrite !vassocr. rewrite rwhisker_rwhisker_alt. apply idpath. } rewrite !vassocl. apply maponpaths. etrans. { rewrite !vassocr. rewrite !rwhisker_vcomp. rewrite vcomp_whisker. rewrite !vassocl. rewrite <- !rwhisker_vcomp. rewrite !vassocl. apply idpath. } apply maponpaths. refine (!_). etrans. { rewrite !vassocr. rewrite rwhisker_rwhisker. rewrite !vassocl. apply idpath. } apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker. rewrite !vassocl. apply maponpaths. rewrite rwhisker_rwhisker. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. 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.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.Properties.ContainsAdjEquiv. Require Import UniMath.Bicategories.Limits.Inserters.