Lemma CoproductOfArrowsIn1 {a b : C} (CCab : CoproductCocone a b) {c d : C} (CCcd : CoproductCocone c d) (f : a --> c) (g : b --> d) : CoproductIn1 CCab · CoproductOfArrows CCab CCcd f g = f · CoproductIn1 CCcd. Proof. unfold CoproductOfArrows. apply CoproductIn1Commutes. 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.