Definition binarySumMap_2 {C:category} {a b a' b':C} (sum : BinarySum a b) (sum' : BinarySum a' b') (f : a --> a') (g : b --> b') : rm_opp_ob (universalObject sum) --> rm_opp_ob (universalObject sum'). Proof. unshelve refine (binarySumMap _ _ _). { exact (in_1 sum' ∘ f). } { exact (in_2 sum' ∘ g). } 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.