Lemma LRB_lassociator_lwhisker_on {a b c d e : B} (f0 : hom a b) (g0 : hom b c) (h0 : hom c d) (i0 : hom d e) : LRB_lwhisker (η (hom a b) f0) (LRB_associator (η (hom b c) g0) (η (hom c d) h0) (η (hom d e) i0)) = LRB_lassociator_lwhisker f0 g0 h0 i0 · #(η (hom _ _)) (f0 ◃ rassociator g0 h0 i0) · LRB_lassociator_lwhisker' f0 g0 h0 i0. Proof. etrans. { unfold LRB_lwhisker. apply maponpaths. exact (prewhisker_LRB_associator' g0 h0 i0). } unfold LRB_associator_pre_simpl_mor. simpl. unfold functor_fix_snd_arg_mor. unfold LRB_lassociator_lwhisker, LRB_lassociator_lwhisker'. simpl. etrans. { apply maponpaths, maponpaths_2. exact (! id_left (id₁ (η (hom a b) f0))). } etrans. { etrans. { apply maponpaths, binprod_comp. } apply (functor_comp (LRB_composition a b e)). } rewrite ! assoc'. apply maponpaths. etrans. { apply maponpaths, maponpaths_2. exact (! id_left (id₁ (η (hom a b) f0))). } etrans. { etrans. { apply maponpaths, binprod_comp. } apply (functor_comp (LRB_composition a b e)). } apply maponpaths. etrans. { apply maponpaths, maponpaths_2. exact (! id_left (id₁ (η (hom a b) f0))). } etrans. { etrans. { apply maponpaths, binprod_comp. } apply (functor_comp (LRB_composition a b e)). } rewrite ! assoc. etrans. { do 2 apply maponpaths. apply maponpaths_2. exact (! id_left (id₁ (η (hom a b) f0))). } etrans. { apply maponpaths. etrans. { apply maponpaths, binprod_comp. } apply (functor_comp (LRB_composition a b e)). } rewrite ! assoc. etrans. 2: { apply maponpaths_2. refine (pr21 (LRB_composition_comm a b e) _ _ (id₁ f0 #, (rassociator g0 h0 i0 : (hom _ _)⟦_,_⟧)) @ _). apply maponpaths. cbn. apply maponpaths. apply hcomp_identity_left. } cbn. etrans. { do 2 apply maponpaths_2. apply maponpaths. apply maponpaths_2. apply pathsinv0, (functor_id (η (hom _ _))). } rewrite ! assoc'. apply maponpaths. unfold LRB_associator_comp_r'. cbn. rewrite ! assoc. apply maponpaths_2. etrans. 2: { apply maponpaths_2. apply pathsinv0. apply (pr2 (pr2 (LRB_composition_comm a b e) (f0, g0 · (h0 · i0) : hom _ _))). } now rewrite id_left. 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.