Lemma postcompWithBinCoproductArrow {a b : C} (CCab : BinCoproductCocone a b) {c : C} (f : a --> c) (g : b --> c) {x : C} (k : c --> x) : BinCoproductArrow CCab f g · k = BinCoproductArrow CCab (f · k) (g · k). Proof. apply BinCoproductArrowUnique. - rewrite assoc, BinCoproductIn1Commutes; apply idpath. - 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.