Lemma transport_counit : ε₂ o l ◅ r₁_to_r₂ = ε₁. Proof. rewrite <- remove_ε₁. unfold r₁_to_r₂. do 3 rewrite <- rwhisker_vcomp. rewrite <- !vassocr. rewrite help_triangle_ε. rewrite !vassocr. rewrite <- !lwhisker_vcomp. repeat (apply (maponpaths (λ z, z • _))). use vcomp_move_L_Mp. { is_iso. } cbn. rewrite (maponpaths (λ z, z • _) (!(vassocr _ _ _))). rewrite inverse_pentagon. rewrite !vassocr. rewrite !lwhisker_vcomp. rewrite !lwhisker_hcomp, !rwhisker_hcomp. rewrite <- !vassocr. rewrite (maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)). rewrite <- interchange. rewrite lassociator_rassociator, !id2_right, hcomp_identity. rewrite id2_left. rewrite <- interchange. rewrite rassociator_lassociator, !id2_right, hcomp_identity. rewrite id2_right. rewrite <- !lwhisker_hcomp, <- !rwhisker_hcomp. rewrite <- lwhisker_vcomp. rewrite !lwhisker_hcomp, !rwhisker_hcomp. rewrite triangle_r_inv. rewrite <- !vassocr. apply maponpaths. apply hcomp_rassoc. 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.