Definition left_adj_equiv_right_biadj_preserves_binprod_1cell : left_adjoint_equivalence right_biadj_preserves_binprod_1cell. Proof. use comp_left_adjoint_equivalence. - use (@comp_left_adjoint_equivalence bicat_of_univ_cats (univ_hom _ _ _) (univ_hom _ _ _) (univalent_category_binproduct (univ_hom _ _ _) (univ_hom _ _ _))). + apply equiv_cat_to_adj_equiv. exact (biadj_hom_equiv R x p). + apply (has_binprod_ump_binprod_cat_ump _ _ Hp). - use equiv_cat_to_adj_equiv. use pair_adj_equivalence_of_cats. + exact (adj_equivalence_of_cats_inv (biadj_hom_equiv R x y₁)). + exact (adj_equivalence_of_cats_inv (biadj_hom_equiv R x y₂)). 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.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Properties. Require Import UniMath.Bicategories.Morphisms.Properties.ClosedUnderInvertibles. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Biadjunction. Require Import UniMath.Bicategories.PseudoFunctors.Preservation.Preservation. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.Limits.Products.