Lemma LRB_rwhisker_rwhisker {x y z w : B} {f g : R (hom x y)} (α : R (hom x y)⟦f,g⟧) (h : R (hom y z)) (i : R (hom z w)) : inv_from_z_iso (LRB_associator f h i) · LRB_rwhisker (LRB_rwhisker α h) i = LRB_rwhisker α (LRB_composition _ _ _ (h, i)) · inv_from_z_iso (LRB_associator g h i). Proof. apply z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left. use (factor_through_squash _ _ (eso (hom _ _) f)). { apply homset_property. } intros [f0 pf]. induction (isotoid _ (pr2 (R (hom x y))) pf). use (factor_through_squash _ _ (eso (hom _ _) g)). { apply homset_property. } intros [g0 pg]. induction (isotoid _ (pr2 (R (hom _ _))) pg). use (factor_through_squash _ _ (eso (hom _ _) h)). { apply homset_property. } intros [h0 ph]. induction (isotoid _ (pr2 (R (hom _ _))) ph). use (factor_through_squash _ _ (eso (hom _ _) i)). { apply homset_property. } intros [i0 pi]. induction (isotoid _ (pr2 (R (hom _ _))) pi). clear pf pg ph pi. assert (α' : ∑ α0 : (hom _ _)⟦f0,g0⟧, #(η (hom _ _)) α0 = α). { apply (ff (hom _ _) f0 g0). } induction α' as [α0 αp]. induction αp. set (t := λ x y z w f g h, toforallpaths _ _ _ (base_paths _ _ (LRB_associator_comm x y z w)) (f , (g, h))). etrans. { apply maponpaths_2, t. } etrans. 2: { apply maponpaths, pathsinv0, t. } etrans. { apply maponpaths_2, (LRB_associator_pre_simpl f0 h0 i0). } etrans. 2: { apply maponpaths, (! LRB_associator_pre_simpl g0 h0 i0). } unfold LRB_associator_pre_simpl_mor ; cbn. unfold functor_fix_snd_arg_mor. etrans. 2: { rewrite assoc. apply maponpaths_2. etrans. 2: { apply functor_comp. } cbn. apply maponpaths. rewrite id_right. etrans. 2: { do 2 apply maponpaths_2. do 2 apply maponpaths. apply (functor_id (η_{y,z})). } etrans. 2: { apply maponpaths. apply (functor_id (η (hom z w))). } apply maponpaths_2. exact (! pr21 (LRB_composition_comm x y z) _ _ (α0 #, (id₁ h0))). } etrans. 2: { apply maponpaths_2. etrans. 2: { do 2 apply maponpaths. apply id_left. } etrans. 2: { apply maponpaths, pathsinv0, binprod_comp. } cbn. apply pathsinv0. set (t1 := pr11 (LRB_composition_comm x y z) (f0, h0)). set (t2 := # (η (hom z w)) (id₂ i0)). set (s1 := # (η (hom x z)) (id₂ h0 ⋆⋆ α0)). set (s2 := id₁ (η (hom z w) i0)). set (t3 := (t1 #, s2)). set (s3 := (s1 #, t2)). exact (functor_comp (LRB_composition x z w) t3 s3). } rewrite ! assoc'. apply maponpaths. etrans. 2: { rewrite assoc. apply maponpaths_2. exact (! pr21 (LRB_composition_comm x z w) _ _ ( (id₂ h0 ⋆⋆ α0) : (hom _ _)⟦_,_⟧ #, id2 i0)). } rewrite assoc'. apply maponpaths. cbn. etrans. 2: { rewrite assoc. apply maponpaths_2. etrans. 2: { apply functor_comp. } apply maponpaths. refine (! rwhisker_rwhisker_alt _ _ _ @ _). apply maponpaths_2. now do 2 rewrite hcomp_identity_right. } etrans. 2: { apply maponpaths_2. apply pathsinv0, (functor_comp (η (hom x w))). } rewrite ! assoc'. apply maponpaths. etrans. { apply maponpaths. etrans. { apply pathsinv0, functor_comp. } cbn. now rewrite id_right. } rewrite id_left. etrans. 2: { rewrite assoc. apply maponpaths_2. refine (! pr21 (nat_z_iso_inv (LRB_composition_comm x y w)) _ _ (α0 #, id2 (h0 · i0) : (hom _ _)⟦_,_⟧) @ _). cbn. apply maponpaths_2, maponpaths. now rewrite hcomp_identity_right. } cbn. rewrite ! assoc'. apply maponpaths. etrans. 2: { apply functor_comp. } apply maponpaths. cbn. rewrite id_right. rewrite (functor_id (η (hom y w))). 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.