Definition binprod_ump_1_univ_cat : binprod_ump_1 (univ_cat_binprod_cone C₁ C₂). Proof. intro q. use make_binprod_1cell. - exact (bindelta_pair_functor (binprod_cone_pr1 q) (binprod_cone_pr2 q)). - apply nat_z_iso_to_invertible_2cell. apply bindelta_pair_pr1_z_iso. - apply nat_z_iso_to_invertible_2cell. apply bindelta_pair_pr2_z_iso. 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.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Categories.Dialgebras. Require Import UniMath.CategoryTheory.Categories.CatIsoInserter. Require Import UniMath.CategoryTheory.Categories.EilenbergMoore. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.IsoCommaCategory. Require Import UniMath.CategoryTheory.CommaCategories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing. Require Import UniMath.CategoryTheory.Monads.Monads. 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.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.CommaObjects. Require Import UniMath.Bicategories.Limits.Inserters. Require Import UniMath.Bicategories.Limits.Equifiers. Require Import UniMath.Bicategories.Limits.IsoInserters. Require Import UniMath.Bicategories.Limits.EilenbergMooreObjects. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.Monads.Examples.MonadsInBicatOfUnivCats.