Lemma LRB_runitor_rwhisker {x y z : B} (f : R (hom x y)) (g : R (hom y z)) : inv_from_z_iso (LRB_associator f (η (hom y y) (identity y)) g) · (LRB_rwhisker (LRB_runitor f) g) = LRB_lwhisker f (LRB_lunitor g). Proof. use z_iso_inv_on_right. 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). clear pf pg. etrans. { unfold LRB_rwhisker. apply maponpaths. apply prewhisker_LRB_runitor. } etrans. 2: { unfold LRB_lwhisker. do 2 apply maponpaths. apply pathsinv0, prewhisker_LRB_lunitor. } etrans. 2: apply maponpaths_2, pathsinv0, prewhisker_LRB_associator'. cbn. unfold functor_fix_snd_arg_mor. unfold LRB_associator_pre_simpl_mor. cbn. etrans. 2: { do 3 apply maponpaths. do 2 apply maponpaths_2. etrans. 2: { apply maponpaths, binprod_id. } apply pathsinv0, (functor_id (LRB_composition y y z)). } rewrite id_left. etrans. 2: { rewrite assoc'. apply maponpaths. rewrite assoc'. apply maponpaths. etrans. 2: apply (functor_comp (LRB_composition x y z)). apply maponpaths. cbn. apply maponpaths. rewrite assoc. apply maponpaths_2. apply pathsinv0, (pr2 (pr2 (LRB_composition_comm y y z) (id₁ y : hom _ _, g0))). } do 2 rewrite id_left. etrans. 2: { apply maponpaths. rewrite assoc'. apply maponpaths. rewrite assoc'. apply maponpaths. rewrite (! functor_id (η_{x,y}) _). apply (pr21 (nat_z_iso_inv (LRB_composition_comm x y z)) _ _ (_ #, lunitor g0 : (hom _ _)⟦_,_⟧)). } simpl. etrans. 2: { do 2 apply maponpaths. rewrite assoc. apply maponpaths_2. etrans. 2: apply functor_comp. apply maponpaths. refine (! lunitor_lwhisker _ _ @ _). apply maponpaths. apply pathsinv0, hcomp_identity_left. } etrans. { apply maponpaths. do 3 apply maponpaths_2. apply (functor_id (LRB_composition x y y)). } rewrite id_left. etrans. { do 2 apply maponpaths. apply (! id_right _). } etrans. { etrans. { apply maponpaths, binprod_comp. } apply (functor_comp (LRB_composition x y z)). } apply maponpaths. etrans. 2: { apply maponpaths. rewrite <- hcomp_identity_right. exact (! pr21 (nat_z_iso_inv (LRB_composition_comm x y z)) _ _ (runitor f0 : (hom _ _)⟦_,_⟧ #, id2 g0)). } cbn. etrans. 2: { rewrite assoc. apply maponpaths_2. apply pathsinv0, (pr2 (pr2 (LRB_composition_comm x y z) (f0 · id₁ y : hom _ _, g0))). } rewrite id_left. do 2 apply maponpaths. apply pathsinv0, (functor_id (η_{y,z})). 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.