Lemma binarySumMapUniqueness {C:category} {a b:C} (sum : BinarySum a b) {c:C} (f g : Hom C (rm_opp_ob (universalObject sum)) c) : f ∘ in_1 sum = g ∘ in_1 sum -> f ∘ in_2 sum = g ∘ in_2 sum -> f = g. Proof. intros r s. apply opp_mor_eq, mapUniqueness, dirprodeq; assumption. 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.