Definition binarySumMap {C:category} {a b:C} (sum : BinarySum a b) {c:C} : a --> c -> b --> c -> rm_opp_ob (universalObject sum) --> c := λ f g, rm_opp_mor (sum \\ (opp_mor f,,opp_mor g)).
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.