proposition: Lemma LRB_runitor_pre_simpl {x y : B} (f : B⟦x,y⟧) : pr1 (LRB_runitor_nat_z_iso_pre x y) f = (pr1 (LRB_composition_comm x y y) (_,_)) · #(η_{x,y}) (runitor f).
proof: Proof. cbn. rewrite ! id_left. etrans. { apply maponpaths_2, maponpaths, binprod_id. } etrans. { apply maponpaths_2, functor_id. } refine (id_left _ @ _). now rewrite id_right. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.CompositesAndInverses UniMath.CategoryTheory.PrecompEquivalence UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.RezkCompletion UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.YonedaLemma UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Properties UniMath.Bicategories.PseudoFunctors.Examples.Composition