proposition: Lemma transport_unit : r₁_to_r₂ ▻ l o η₁ = η₂.
proof: 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.
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