proposition: Lemma transport_counit : ε₂ o l ◅ r₁_to_r₂ = ε₁.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.TransportLaws UniMath.Bicategories.Core.EquivToAdjequiv