Definition one_types_binprod_cone (X Y : one_types) : binprod_cone X Y. Proof. use make_binprod_cone. - use make_one_type. + exact (pr1 X × pr1 Y). + apply isofhleveldirprod. * exact (pr2 X). * exact (pr2 Y). - exact pr1. - exact pr2. 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.