Definition psfunctor_B_to_LRB_invertible_cells : invertible_cells psfunctor_B_to_LRB_data. Proof. split. - exact (λ x, is_invertible_2cell_id₂ (C := LRB) (η (hom x x) (id₁ x))). - exact (λ x y z f g, pr2 (lift_functor_along_comm (R (hom x z)) (pair_functor (η_{x,y}) (η_{y,z})) (pair_functor_eso (η_{x,y}) (η_{y,z}) (eso (hom x y)) (eso_{y,z})) (pair_functor_ff (η_{x,y}) (η_{y,z}) (ff_{x,y}) (ff_{y,z})) (hcomp_functor ∙ η_{x,z})) (make_catbinprod (C := hom x y) (D := hom y z) f g)). Defined.
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.