Lemma LRB_vcomp_runitor {x y : B} {f g : R (hom x y)} (α : R(hom x y)⟦f,g⟧) : LRB_rwhisker α (η (hom y y) (identity y)) · LRB_runitor g = pr1 (LRB_runitor f) · α. Proof. 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 x y) g)). { apply homset_property. } intros [g0 pg]. induction (isotoid _ (pr2 (R (hom x y))) pg). clear pf pg. etrans. { apply maponpaths. exact (toforallpaths _ _ _ (base_paths _ _ (LRB_runitor_comm _ _)) g0). } assert (α' : ∑ α0 : (hom x y)⟦f0,g0⟧, #(η_{x,y}) α0 = α). { apply (ff_{x,y} f0 g0). } induction α' as [α0 αp]. induction αp. etrans. 2: apply maponpaths_2, (! prewhisker_LRB_runitor f0). etrans. 2: { rewrite assoc'. apply maponpaths. apply (functor_comp (η_{x,y})). } etrans. 2: { do 2 apply maponpaths. apply (vcomp_runitor f0 g0 α0). } etrans. { apply maponpaths, (LRB_runitor_pre_simpl g0). } etrans. 2: apply maponpaths, pathsinv0, (functor_comp (η_{x,y})). rewrite ! assoc. apply maponpaths_2. etrans. 2: { do 2 apply maponpaths_2. apply pathsinv0, (functor_id (LRB_composition_curry1 x y y (η_{x,y} f0))). } rewrite id_left. refine (_ @ pr21 (LRB_composition_comm x y y) _ _ (α0 #, id2 (id₁ y) : (hom _ _)⟦_,_⟧ ) @ _) ; cbn. - unfold functor_fix_snd_arg_mor. apply maponpaths_2, maponpaths, maponpaths, pathsinv0, (functor_id (η (hom y y))). - do 2 apply maponpaths. apply pathsinv0, rwhisker_hcomp. 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.