proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.AdjointUnique UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.TransportLaws UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Morphisms.Properties.ClosedUnderInvertibles UniMath.Bicategories.Limits.Pullbacks