Lemma prewhisker_LRB_runitor {x y : B} (f : B⟦x,y⟧) : pr1 (LRB_runitor (η_{x,y} f)) = LRB_lwhisker (η_{x,y} f) (id₁ (η (hom y y) (id₁ y))) · pr1 (LRB_composition_comm x y y) (make_catbinprod (C := hom x y) (D := hom y y) f (id₁ y)) · # (η_{x,y}) (runitor f). Proof. refine (toforallpaths _ _ _ (base_paths _ _ (LRB_runitor_comm x y)) f @ _). etrans. 2: { do 2 apply maponpaths_2. apply (! functor_id (LRB_composition_curry1 x y y (η_{x,y} f)) _). } rewrite id_left. unfold LRB_runitor_nat_z_iso_pre. cbn. rewrite ! id_left. etrans. { apply maponpaths_2. etrans. { apply maponpaths, binprod_id. } apply functor_id. } now rewrite id_left, id_right. 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.