Definition make_isBinCoproductCocone (hsC : has_homsets C)(a b co : C) (ia : a --> co) (ib : b --> co) : (∏ (c : C) (f : a --> c) (g : b --> c), ∃! k : C ⟦co, c⟧, ia · k = f × ib · k = g) → isBinCoproductCocone a b co ia ib. Proof. intros H c cc. set (H':= H c (coconeIn cc true) (coconeIn cc false)). use tpair. - exists (pr1 (pr1 H')). set (T := pr2 (pr1 H')). simpl in T. abstract (intro u; induction u; [ apply (pr1 T) | apply (pr2 T)]). - simpl. intros. abstract (intros; apply subtypePath; [ intro; apply impred; intro; apply hsC | apply path_to_ctr; split; [ apply (pr2 t true) | apply (pr2 t false)] ]). 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.