Lemma LRB_associator_comp_m_on {a b c d e : B} (f : hom a b) (g : hom b c) (h : hom c d) (i : hom d e) : pr1 (LRB_associator (η (hom a b) f) (LRB_composition b c d (η (hom b c) g, η (hom c d) h)) (η (hom d e) i)) = LRB_associator_comp_m f g h i · #(η (hom a e)) (pr1 (rassociator_transf _ _ _ _) (f , ((g · h : hom _ _),i))) · LRB_associator_comp_m' f g h i. Proof. unfold LRB_associator_comp_m, LRB_associator_comp_m'. set (n2 := LRB_composition_comm a d e ). set (n1 := LRB_associator_comm a b d e). set (q := toforallpaths _ _ _ (base_paths _ _ n1) (f, (g·h : hom _ _, i))). etrans. 2: { apply maponpaths_2. unfold n2. rewrite assoc'. apply maponpaths. exact (! prewhisker_LRB_associator_co _ _ _). } rewrite assoc. etrans. 2: { apply maponpaths_2. rewrite assoc'. apply maponpaths. rewrite assoc'. apply maponpaths. simpl. rewrite assoc. apply maponpaths_2. apply pathsinv0, (pr2 (pr2 (LRB_composition_comm a b e) (f, g · h · i : hom _ _))). } rewrite id_left. etrans. 2: { apply maponpaths_2. apply maponpaths. rewrite assoc'. apply maponpaths. etrans. 2: apply (functor_comp (LRB_composition a b e)). apply maponpaths. etrans. 2: apply binprod_comp. rewrite id_left. apply maponpaths. apply pathsinv0, (pr2 (pr2 (LRB_composition_comm b d e) (g · h : hom _ _, i))). } etrans. 2: { apply maponpaths_2. do 2 apply maponpaths. apply pathsinv0, (functor_id (LRB_composition a b e)). } rewrite id_right. set (t := pr21 (LRB_associator_nat_z_iso a b d e)). unfold is_nat_trans in t. etrans. 2: { apply maponpaths_2. exact (! (t _ _ (id₁ (η_{ a, b} f) #, (pr1 (LRB_composition_comm b c d) (g, h) #, id₁ (η_{ d, e} i))))). } Opaque LRB_composition. Opaque LRB_composition_comm. Opaque LRB_associator_nat_z_iso. cbn. etrans. 2: { rewrite assoc'. apply maponpaths. etrans. 2: apply (functor_comp (LRB_composition a b e)). etrans. 2: apply maponpaths, binprod_comp. rewrite id_left. etrans. 2: { do 2 apply maponpaths. etrans. 2: apply (functor_comp (LRB_composition b d e)). apply maponpaths. etrans. 2: apply binprod_comp. rewrite id_left. apply maponpaths_2. apply pathsinv0, (pr2 (pr2 (LRB_composition_comm b c d) (g, h))). } rewrite binprod_id. rewrite (functor_id (LRB_composition b d e)). now rewrite (functor_id (LRB_composition a b e)). } apply pathsinv0, id_right. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.CategoryTheory.PrecompEquivalence. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.RezkCompletions.RezkCompletions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.YonedaLemma. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Properties. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition.