Lemma LRB_rwhisker_lwhisker {x y z w : B} (f : R (hom x y)) {g h : R (hom y z)} (α : R (hom y z)⟦g,h⟧) (i : R (hom z w)) : LRB_lwhisker f (LRB_rwhisker α i) · inv_from_z_iso (LRB_associator f h i) = inv_from_z_iso (LRB_associator f g i) · (LRB_rwhisker (LRB_lwhisker f α) i). Proof. apply pathsinv0, z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left. use (factor_through_squash _ _ (eso (hom x y) 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 _ _)⟦g0,h0⟧, #(η (hom _ _)) α0 = α). { apply (ff (hom _ _) g0 h0). } 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 g0 i0). } etrans. 2: { apply maponpaths, (! LRB_associator_pre_simpl f0 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. apply maponpaths. apply maponpaths_2. apply (functor_id (η_{x,y})). } etrans. 2: { apply maponpaths. apply (functor_id (η (hom z w))). } apply maponpaths_2. exact (! pr21 (LRB_composition_comm x y z) _ _ ((id₁ f0) #, α0)). } 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, g0)). set (t2 := # (η (hom z w)) (id₂ i0)). set (s1 := # (η (hom x z)) (α0 ⋆⋆ id₂ f0)). 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) _ _ ( (α0 ⋆⋆ id₂ f0) : (hom _ _)⟦_,_⟧ #, id2 i0)). } rewrite assoc'. apply maponpaths. cbn. etrans. 2: { rewrite assoc. apply maponpaths_2. etrans. 2: { apply functor_comp. } apply maponpaths. refine (rwhisker_lwhisker_rassociator _ _ _ _ _ _ _ _ _ @ _). apply maponpaths_2. rewrite hcomp_identity_right. now rewrite hcomp_identity_left. } 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. rewrite id_right. do 2 apply maponpaths. refine (_ @ ! pr21 (nat_z_iso_inv (LRB_composition_comm y z w)) _ _ (α0 #, id2 i0)). cbn. do 3 apply maponpaths. apply pathsinv0, (functor_id (η (hom z w))). } cbn. etrans. { do 2 apply maponpaths. apply maponpaths_2, pathsinv0, id_right. } etrans. { apply maponpaths. refine (_ @ functor_comp (LRB_composition x y w) (id₁ (η_{x,y} f0) #, # (η (hom y w)) (id₂ i0 ⋆⋆ α0)) (_ #, is_z_isomorphism_mor (pr2 (LRB_composition_comm y z w) (h0, i0)))). apply maponpaths. rewrite id_right. cbn. apply maponpaths_2. apply pathsinv0, id_right. } rewrite ! assoc. apply maponpaths_2. etrans. { refine (_ @ ! pr21 (nat_z_iso_inv (LRB_composition_comm x y w)) _ _ (id2 f0 #, (id₂ i0 ⋆⋆ α0) : (hom _ _)⟦_,_⟧)). cbn. do 2 apply maponpaths. apply maponpaths_2. apply pathsinv0, (functor_id (η_{x,y})). } apply maponpaths_2. cbn. apply maponpaths. rewrite hcomp_identity_right. now rewrite hcomp_identity_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.