proposition: Lemma LRB_laws : prebicat_laws LRB_data.
proof: Proof. repeat split ; intro ; intros. - apply id_left. - apply id_right. - apply assoc. - exact (functor_id (LRB_composition_curry1 a b c f) g). - exact (functor_id (LRB_composition_curry2 a b c g) f). - exact (! functor_comp (LRB_composition_curry1 _ _ _ _) _ _). - exact (! functor_comp (LRB_composition_curry2 _ _ _ _) _ _). - apply LRB_vcomp_lunitor. - apply LRB_vcomp_runitor. - apply LRB_lwhisker_lwhisker. - apply LRB_rwhisker_lwhisker. - apply LRB_rwhisker_rwhisker. - refine (! functor_comp (LRB_composition a b c) (x #, id2 h) (id2 g #, y) @ _). refine (_ @ functor_comp (LRB_composition a b c) (id2 f #, y) (x #, id2 i)). do 2 rewrite <- binprod_comp. now rewrite ! id_left, ! id_right. - apply (pr22 (LRB_lunitor f)). - apply (pr22 (LRB_lunitor f)). - apply (pr22 (LRB_runitor f)). - apply (pr22 (LRB_runitor f)). - apply (pr22 (LRB_associator f g h)). - apply (pr22 (LRB_associator f g h)). - apply LRB_runitor_rwhisker. - apply LRB_lassociator_lassociator. 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