Definition make_BinCoproductCocone (a b : C) : ∏ (c : C) (f : a --> c) (g : b --> c), isBinCoproductCocone _ _ _ f g → BinCoproductCocone a b. Proof. intros. use tpair. - exists c. apply (CopCocone f g). - apply X. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag. Require Import UniMath.CategoryTheory.Limits.BinCoproducts.