Lemma psfunctor_B_to_LRB_laws : psfunctor_laws psfunctor_B_to_LRB_data. Proof. repeat split. - exact (λ x y f, functor_id (η_{x,y}) f). - intros x y f g h α β. apply (functor_comp (η_{x,y})). - exact (λ x y f, prewhisker_LRB_lunitor f). - exact (λ x y f, prewhisker_LRB_runitor f). - exact (λ x y z w f g h, prewhisker_LRB_associator f g h). - intro ; intros. set (t := λ fg, ! pr21 (LRB_composition_comm a b c) (make_catbinprod (C:=hom _ _) (D:=hom _ _) f g₁) (make_catbinprod (C:=hom _ _) (D:=hom _ _) f g₂) fg). cbn in t. refine (_ @ t (catbinprodmor (C:=hom _ _) (D:=hom _ _) (id2 f) η0) @ _). + do 2 apply maponpaths. apply lwhisker_hcomp. + now rewrite (functor_id (η (hom a b))). - intro ; intros. unfold psfunctor_B_to_LRB_data. set (t := λ fg, ! pr21 (LRB_composition_comm a b c) (make_catbinprod (C:=hom _ _) (D:=hom _ _) f₁ g) (make_catbinprod (C:=hom _ _) (D:=hom _ _) f₂ g) fg). cbn in t. refine (_ @ t (catbinprodmor (C:=hom _ _) (D:=hom _ _) η0 (id2 g)) @ _). + do 2 apply maponpaths. apply rwhisker_hcomp. + now rewrite (functor_id (η (hom b c))). 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.