Definition BinCoproductOfArrows {a b : C} (CCab : BinCoproductCocone a b) {c d : C} (CCcd : BinCoproductCocone c d) (f : a --> c) (g : b --> d) : BinCoproductObject CCab --> BinCoproductObject CCcd := BinCoproductArrow CCab (f · BinCoproductIn1 CCcd) (g · BinCoproductIn2 CCcd).
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag. Require Import UniMath.CategoryTheory.Limits.BinCoproducts.