Lemma BinProductArrowUnique (a b : C) (P : BinProductCone a b) (c : C) (f : C⟦c,a⟧) (g : C⟦c,b⟧) (k : C⟦c,BinProductObject P⟧) : k · BinProductPr1 P = f -> k · BinProductPr2 P = g -> k = BinProductArrow P f g. Proof. intros H1 H2. use limArrowUnique; simpl. now 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.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.