Lemma transport_unit : r₁_to_r₂ ▻ l o η₁ = η₂. Proof. rewrite <- remove_η₂. unfold r₁_to_r₂. rewrite <- !lwhisker_vcomp. rewrite !vassocr. rewrite help_triangle_η. rewrite linvunitor_assoc. rewrite !vassocr. rewrite !(maponpaths (λ z, ((((((z • _) • _) • _) • _) • _) • _)) (!(vassocr _ _ _))). rewrite rassociator_lassociator, id2_right. rewrite !(maponpaths (λ z, (((((z • _) • _) • _) • _) • _)) (!(vassocr _ _ _))). rewrite rwhisker_vcomp. rewrite <- !vassocr. rewrite <- !rwhisker_vcomp. repeat (apply maponpaths). rewrite <- !vassocr. apply maponpaths. rewrite !vassocr. rewrite rassociator_lassociator, id2_left. rewrite <- !vassocr. apply maponpaths. rewrite !vassocr. rewrite inverse_pentagon. rewrite <- !vassocr. rewrite !rwhisker_hcomp. apply maponpaths. rewrite !vassocr. rewrite !(maponpaths (λ z, (z • _) • _) (!(vassocr _ _ _))). rewrite <- !lwhisker_hcomp. rewrite !lwhisker_vcomp. rewrite rassociator_lassociator. rewrite lwhisker_id2, id2_right. rewrite !lwhisker_hcomp. rewrite <- hcomp_rassoc. rewrite <- !vassocr. apply maponpaths. apply triangle_l. 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.