Lemma composition_of_maps : r₂_to_r₁ o r₁_to_r₂ = composition_of_triangles. Proof. unfold r₁_to_r₂, r₂_to_r₁, composition_of_triangles. rewrite !vassocr. apply (maponpaths (λ z, z • lunitor r₁)). rewrite <- !vassocr. apply (maponpaths (λ z, rinvunitor r₁ • z)). rewrite <- !lwhisker_vcomp, <- !rwhisker_vcomp. rewrite <- !lwhisker_vcomp. rewrite <- !vassocr. rewrite !lwhisker_hcomp, !rwhisker_hcomp. rewrite !vassocr. rewrite !(maponpaths (fun z => z • _) (!(vassocr _ _ _))). rewrite hcomp_lassoc. rewrite !vassocr. rewrite !(maponpaths (fun z => (z • _) • _) (!(vassocr _ _ _))). rewrite hcomp_lassoc. rewrite !vassocr. rewrite !(maponpaths (fun z => ((z • _) • _) • _) (!(vassocr _ _ _))). rewrite hcomp_lassoc. rewrite !vassocr. rewrite !(maponpaths (fun z => (((z • _) • _) • _) • _) (!(vassocr _ _ _))). rewrite hcomp_lassoc. rewrite !vassocr. rewrite !(maponpaths (fun z => ((((z • _) • _) • _) • _) • _) (!(vassocr _ _ _))). rewrite hcomp_lassoc. rewrite !vassocr. rewrite <- !lwhisker_hcomp, <- !rwhisker_hcomp. rewrite help₂. rewrite <- !vassocr. apply maponpaths. rewrite !lwhisker_hcomp, !rwhisker_hcomp. rewrite <- !interchange. rewrite !vassocr. rewrite <- inverse_pentagon_3. rewrite <- !vassocr. do 3 rewrite interchange. rewrite !id2_left. rewrite !vassocr. rewrite !(maponpaths (λ z, ((z • _) • _) • _) (!(vassocr _ _ _))). rewrite <- hcomp_lassoc. rewrite <- interchange. rewrite !hcomp_identity. rewrite !vassocr, id2_left. rewrite ε₁_natural. rewrite <- rwhisker_vcomp. repeat (rewrite <- (id2_right (id₂ r₁)) ; rewrite interchange). rewrite !id2_right. rewrite !vassocr. apply (maponpaths (λ z, z • _)). rewrite !(maponpaths (λ z, ((z • _) • _) • _) (!(vassocr _ _ _))). rewrite <- !rwhisker_hcomp. rewrite rwhisker_vcomp. rewrite rassociator_lassociator, id2_rwhisker, id2_right. rewrite !vassocr. rewrite !(maponpaths (λ z, (z • _) • _) (!(vassocr _ _ _))). rewrite rwhisker_vcomp. rewrite rassociator_lassociator, id2_rwhisker, id2_right. rewrite !vassocr. rewrite !(maponpaths (λ z, z • _) (!(vassocr _ _ _))). rewrite !rwhisker_hcomp. rewrite <- hcomp_lassoc. rewrite <- !vassocr. rewrite <- hcomp_lassoc. rewrite !vassocr. apply (maponpaths (λ z, z • _)). rewrite !hcomp_identity. rewrite <- !vassocr. rewrite <- !interchange. rewrite !vassocr, !id2_left, !id2_right. rewrite <- (id2_right (lunitor r₂)). rewrite !vassocr. rewrite <- (id2_left η₁). rewrite interchange. rewrite !vassocr. rewrite !id2_right, !id2_left. apply (maponpaths (λ z, z • _)). apply rinvunitor_natural. 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.