Definition has_binprod_ump_binprod_cat_ump (HB_2_1 : is_univalent_2_1 B) (p : binprod_cone) (H : has_binprod_ump p) : binprod_cat_ump HB_2_1 p. Proof. intro x. use equiv_cat_to_adj_equiv. use rad_equivalence_of_cats. - apply is_univ_hom. exact HB_2_1. - use full_and_faithful_implies_fully_faithful. split. + intros f g α. use hinhpr. simple refine (_ ,, _). * exact (binprod_ump_2cell H (pr1 α) (pr2 α)). * use pathsdirprod. ** apply binprod_ump_2cell_pr1. ** apply binprod_ump_2cell_pr2. + unfold faithful. intros f g α. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro ; apply homset_property. } use (binprod_ump_2cell_unique H). * exact (pr1 α). * exact (pr2 α). * exact (maponpaths pr1 (pr2 φ₁)). * exact (maponpaths dirprod_pr2 (pr2 φ₁)). * exact (maponpaths pr1 (pr2 φ₂)). * exact (maponpaths dirprod_pr2 (pr2 φ₂)). - intros f g. use hinhpr. simple refine (binprod_ump_1cell H (pr1 f) (pr2 f) ,, _). use make_z_iso'. + exact (pr1 (binprod_ump_1cell_pr1 H _ (pr1 f) (pr2 f)) ,, pr1 (binprod_ump_1cell_pr2 H _ (pr1 f) (pr2 f))). + use is_z_iso_binprod_z_iso. * apply is_inv2cell_to_is_z_iso. apply property_from_invertible_2cell. * apply is_inv2cell_to_is_z_iso. apply property_from_invertible_2cell. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Univalence.