Definition has_binprod_ump_one_types : has_binprod_ump (one_types_binprod_cone X Y). Proof. use make_binprod_ump. - exact binprod_ump_1_one_types. - exact binprod_ump_2_cell_one_types. - exact binprod_ump_2_cell_pr1_one_types. - exact binprod_ump_2_cell_pr2_one_types. - exact binprod_ump_2_cell_unique_one_types. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.OneTypes. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.Inserters. Require Import UniMath.Bicategories.Limits.Equifiers.