Lemma binaryProductMapUniqueness {C:category} {a b:C} (prod : BinaryProduct a b) {c:C} (f g : Hom C c (universalObject prod)) : pr_1 prod ∘ f = pr_1 prod ∘ g -> pr_2 prod ∘ f = pr_2 prod ∘ g -> f = g. Proof. intros r s. apply mapUniqueness. apply dirprodeq. exact r. exact s. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.