Lemma BinCoproductArrowUnique (a b : C) (CC : BinCoproductCocone a b) (x : C) (f : a --> x) (g : b --> x) (k : BinCoproductObject CC --> x) : BinCoproductIn1 CC · k = f → BinCoproductIn2 CC · k = g → k = BinCoproductArrow CC f g. Proof. intros H1 H2. use colimArrowUnique. simpl. intro u; induction u; simpl. - apply H1. - apply H2. Qed.
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.