Lemma help₁ (f : C⟦X,Y⟧) (g g' : C⟦Y,X⟧) (η : id₁ X ==> g ∘ f) (η' : id₁ X ==> g' ∘ f) : ((g ∘ f) ◅ (η' ▻ g o rinvunitor _)) o η ▻ g = (η ▻ (g' ∘ f ∘ g) o rinvunitor _) o η' ▻ g. Proof. rewrite <- rwhisker_vcomp. rewrite !vassocr. rewrite !lwhisker_hcomp, !rwhisker_hcomp. rewrite rinvunitor_natural. rewrite <- !vassocr. rewrite <- !interchange. rewrite !id2_left, !id2_right. rewrite <- (id2_left η). rewrite interchange. rewrite id2_left. apply (maponpaths (λ z, z • _)). rewrite left_unit_inv_assoc₂. rewrite <- triangle_l_inv. rewrite lunitor_V_id_is_left_unit_V_id. rewrite !lwhisker_hcomp. 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.