proposition: 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: Proof. intros H1 H2. use limArrowUnique; simpl. now intro u; induction u; simpl; [ apply H1 | apply H2 ]. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits