Definition binprod_ump_1_one_types : binprod_ump_1 (one_types_binprod_cone X Y). Proof. intro q. use make_binprod_1cell. - exact (λ x, binprod_cone_pr1 q x ,, binprod_cone_pr2 q x). - use make_invertible_2cell. + intro x ; cbn. apply idpath. + apply one_type_2cell_iso. - use make_invertible_2cell. + intro x ; cbn. apply idpath. + apply one_type_2cell_iso. 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.