Definition BinProductArrowUnique' (c d : C) (P : BinProduct C c d) (x : C) (f : x --> c) (g : x --> d) (k : x --> BinProductObject C P) : k · BinProductPr1 C P = f -> k · BinProductPr2 C P = g -> k = BinProductArrow C P f g. Proof. intros; apply path_to_ctr; split; assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.