Lemma id_left_adjoint_equivalence_to_pb_ump_2_cell_eq : (φ ◃ qγ') • lassociator _ _ _ • (((φ ◃ lpr2 ^-1) • β • (ψ ◃ lpr2)) ▹ g) • rassociator _ _ _ = lassociator _ _ _ • (((φ ◃ lpr1 ^-1) • α • (ψ ◃ lpr1)) ▹ f) • rassociator ψ qpr1' f • (ψ ◃ qγ'). Proof. rewrite <- !rwhisker_vcomp. rewrite !vassocl. refine (!_). etrans. { rewrite !vassocr. rewrite <- rwhisker_lwhisker. rewrite !vassocl. apply idpath. } use vcomp_move_R_pM ; [ is_iso | ] ; cbn. refine (!_). rewrite !vassocr. rewrite lwhisker_vcomp. rewrite <- lc. rewrite <- lwhisker_vcomp. rewrite !vassocl. etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite lwhisker_vcomp. rewrite vcomp_rinv. rewrite lwhisker_id2. rewrite id2_rwhisker. rewrite id2_left. rewrite !vassocl. rewrite <- rwhisker_lwhisker_rassociator. apply idpath. } rewrite !vassocr. rewrite p. rewrite !vassocl. do 2 apply maponpaths. rewrite lwhisker_vcomp. rewrite lc. rewrite <- lwhisker_vcomp. rewrite !vassocr. apply maponpaths_2. rewrite rwhisker_lwhisker_rassociator. 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.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.TransportLaws. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Properties.ClosedUnderInvertibles. Require Import UniMath.Bicategories.Limits.Pullbacks.