Lemma LRB_laws : prebicat_laws LRB_data. 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.
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.