proposition: Lemma LRB_lassociator_rwhisker_on {a b c d e : B} (f0 : hom a b) (g0 : hom b c) (h0 : hom c d) (i0 : hom d e) : LRB_rwhisker (LRB_associator (η (hom a b) f0) (η (hom b c) g0) (η (hom c d) h0)) (η (hom d e) i0) = LRB_lassociator_rwhisker f0 g0 h0 i0 · #(η (hom a e)) (rassociator f0 g0 h0 ▹ i0) · LRB_lassociator_rwhisker' f0 g0 h0 i0.
proof: Proof. etrans. { unfold LRB_rwhisker. apply maponpaths. exact (prewhisker_LRB_associator' f0 g0 h0). } unfold LRB_associator_pre_simpl_mor. simpl. unfold functor_fix_snd_arg_mor. unfold LRB_lassociator_rwhisker, LRB_lassociator_rwhisker'. simpl. etrans. { do 2 apply maponpaths. exact (! id_left (id₁ (η (hom d e) i0))). } etrans. { etrans. { apply maponpaths, binprod_comp. } apply (functor_comp (LRB_composition a d e)). } rewrite ! assoc'. apply maponpaths. etrans. { do 2 apply maponpaths. exact (! id_left (id₁ (η (hom d e) i0))). } etrans. { etrans. { apply maponpaths, binprod_comp. } apply (functor_comp (LRB_composition a d e)). } apply maponpaths. etrans. { do 2 apply maponpaths. exact (! id_left (id₁ (η (hom d e) i0))). } etrans. { etrans. { apply maponpaths, binprod_comp. } apply (functor_comp (LRB_composition a d e)). } rewrite ! assoc. etrans. { do 3 apply maponpaths. exact (! id_left (id₁ (η (hom d e) i0))). } etrans. { apply maponpaths. etrans. { apply maponpaths, binprod_comp. } apply (functor_comp (LRB_composition a d e)). } rewrite ! assoc. apply maponpaths_2. etrans. 2: { do 2 apply maponpaths_2. refine (pr21 (LRB_composition_comm a d e) _ _ ((rassociator f0 g0 h0 : (hom _ _)⟦_,_⟧) #, id₁ i0) @ _). apply maponpaths. cbn. apply maponpaths. apply hcomp_identity_right. } apply maponpaths_2. etrans. 2: { rewrite assoc'. apply maponpaths. apply pathsinv0. apply (pr2 (pr2 (LRB_composition_comm a d e) (f0 · (g0 · h0) : hom _ _, i0))). } rewrite id_right. cbn. do 2 apply maponpaths. apply pathsinv0, (functor_id (η (hom d e))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.CompositesAndInverses UniMath.CategoryTheory.PrecompEquivalence UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.RezkCompletion UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.YonedaLemma UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Properties UniMath.Bicategories.PseudoFunctors.Examples.Composition