Lemma precompWithBinCoproductArrow {a b : C} (CCab : BinCoproductCocone a b) {c d : C} (CCcd : BinCoproductCocone c d) (f : a --> c) (g : b --> d) {x : C} (k : c --> x) (h : d --> x) : BinCoproductOfArrows CCab CCcd f g · BinCoproductArrow CCcd k h = BinCoproductArrow CCab (f · k) (g · h). Proof. apply BinCoproductArrowUnique. - rewrite assoc. rewrite BinCoproductOfArrowsIn1. rewrite <- assoc, BinCoproductIn1Commutes. apply idpath. - rewrite assoc, BinCoproductOfArrowsIn2. rewrite <- assoc, BinCoproductIn2Commutes. apply idpath. 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.