Lemma help₂ (f : C⟦X,Y⟧) (g g' : C⟦Y,X⟧) (η : id₁ X ==> g ∘ f) (η' : id₁ X ==> g' ∘ f) : g ◅ ((f ◅ η') ▻ g) o (g ◅ (linvunitor f ▻ g) o (lassociator _ _ _ o η ▻ g)) = g ◅ (rassociator _ _ _) o lassociator _ _ _ o η ▻ (g' ∘ f ∘ g) o rinvunitor _ o η' ▻ g. Proof. rewrite !vassocr. rewrite !(maponpaths (λ z, _ o (_ o z)) (!(vassocr _ _ _))). rewrite <- help₁. rewrite <- !vassocr. apply maponpaths. rewrite <- !rwhisker_vcomp. rewrite !lwhisker_hcomp, !rwhisker_hcomp. rewrite !vassocr. rewrite !(maponpaths (fun z => _ o z) (!(vassocr _ _ _))). rewrite <- hcomp_identity. rewrite hcomp_lassoc. rewrite !vassocr. rewrite hcomp_lassoc. rewrite <- !vassocr. apply maponpaths. rewrite <- !interchange. rewrite !id2_left. rewrite hcomp_rassoc. rewrite !vassocr. rewrite <- (id2_right (id₂ g)). rewrite !interchange. rewrite triangle_r_inv. rewrite id2_right. reflexivity. 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.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.TransportLaws. Require Import UniMath.Bicategories.Core.EquivToAdjequiv.