Lemma LRB_lwhisker_lwhisker {x y z w : B} (f : R (hom x y)) (g : R (hom y z)) {h i : R (hom z w)} (α : R (hom z w)⟦h,i⟧) : LRB_lwhisker f (LRB_lwhisker g α) · inv_from_z_iso (LRB_associator f g i) = inv_from_z_iso (LRB_associator f g h) · LRB_lwhisker (LRB_composition _ _ _ (f,g)) α. 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 _ _)⟦h0,i0⟧, #(η (hom _ _)) α0 = α). { apply (ff (hom _ _) h0 i0). } 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 h0). } etrans. 2: { apply maponpaths, (! LRB_associator_pre_simpl f0 g0 i0). } assert (p : (LRB_lwhisker (η_{y,z} g0) (# (η (hom z w)) α0)) = (LRB_composition_comm y z w (g0 , h0)) · #(η (hom _ _)) (lwhisker g0 α0) · (nat_z_iso_inv (LRB_composition_comm y z w)) (g0 , i0)). { cbn. etrans. 2: { apply maponpaths_2. refine (pr21 (LRB_composition_comm y z w) _ _ (id2 g0 : (hom _ _)⟦_,_⟧ #, α0) @ _) ; cbn. do 2 apply maponpaths. apply hcomp_identity_left. } cbn. rewrite assoc'. etrans. 2: { apply maponpaths. apply pathsinv0, (pr2 (LRB_composition_comm y z w) (g0, i0)). } rewrite (functor_id (η_{y,z})). apply (! id_right _). } etrans. { apply maponpaths. unfold LRB_lwhisker. apply maponpaths. apply p. } unfold LRB_associator_pre_simpl_mor. cbn. etrans. { do 3 apply maponpaths. rewrite assoc'. apply maponpaths. refine (_ @ pr21 (nat_z_iso_inv (LRB_composition_comm y z w)) _ _ (identity g0 #, α0)). cbn. apply maponpaths_2, maponpaths, lwhisker_hcomp. } do 2 rewrite assoc. etrans. { do 3 apply maponpaths. rewrite assoc. apply maponpaths_2. apply (pr2 ((pr2 (LRB_composition_comm y z w)) (g0, h0))). } rewrite id_left. cbn. etrans. 2: { rewrite assoc. apply maponpaths_2. etrans. 2: { apply functor_comp. } cbn. now rewrite id_left, id_right. } etrans. { rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, functor_comp. } cbn. rewrite id_right. do 2 apply maponpaths. exact (! pr21 (nat_z_iso_inv (LRB_composition_comm y z w)) _ _ ( (id₂ g0) #, α0)). } simpl. etrans. { apply maponpaths. etrans. { apply maponpaths, maponpaths_2, (! id_left _). } etrans. { apply maponpaths, binprod_comp. } apply (functor_comp (LRB_composition x y w)). } rewrite ! assoc. apply maponpaths_2. etrans. { rewrite assoc'. apply maponpaths. refine (_ @ ! pr21 (nat_z_iso_inv (LRB_composition_comm x y w)) _ _ (id₁ f0 #, (α0 ⋆⋆ id₂ g0) : (hom _ _)⟦_,_⟧)). cbn. do 2 apply maponpaths. apply maponpaths_2. apply pathsinv0, (functor_id (η_{x,y})). } rewrite ! assoc. apply maponpaths_2. cbn. do 2 rewrite hcomp_identity_left. etrans. { rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, functor_comp. } apply maponpaths. apply lwhisker_lwhisker_rassociator. } etrans. { apply maponpaths, (functor_comp (η (hom _ _))). } rewrite ! assoc. apply maponpaths_2. etrans. { rewrite assoc'. apply maponpaths. refine (_ @ ! pr21 (LRB_composition_comm x z w) _ _ (id2 (f0 · g0) : (hom _ _)⟦_,_⟧ #, α0)). cbn. do 2 apply maponpaths. apply pathsinv0, hcomp_identity_left. } cbn. rewrite assoc. apply maponpaths_2. etrans. { apply pathsinv0, functor_comp. } cbn. apply maponpaths. use total2_paths_f. - cbn. rewrite (functor_id (η (hom x z))). apply id_right. - rewrite transportf_const. cbn. apply 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.