Lemma CoproductOfArrowsIn2 {a b : C} (CCab : CoproductCocone a b) {c d : C} (CCcd : CoproductCocone c d) (f : a --> c) (g : b --> d) : CoproductIn2 CCab · CoproductOfArrows CCab CCcd f g = g · CoproductIn2 CCcd. Proof. unfold CoproductOfArrows. apply CoproductIn2Commutes. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.RepresentableFunctors.Representation.