Lemma BinCoproductOfArrowsIn1 {a b : C} (CCab : BinCoproductCocone a b) {c d : C} (CCcd : BinCoproductCocone c d) (f : a --> c) (g : b --> d) : BinCoproductIn1 CCab · BinCoproductOfArrows CCab CCcd f g = f · BinCoproductIn1 CCcd. Proof. unfold BinCoproductOfArrows. apply BinCoproductIn1Commutes. Qed.
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.