Lemma BinCoproductArrowsEq (c d : C) (CC : BinCoproduct c d) (x : C) (k1 k2 : BinCoproductObject CC --> x) : BinCoproductIn1 CC · k1 = BinCoproductIn1 CC · k2 -> BinCoproductIn2 CC · k1 = BinCoproductIn2 CC · k2 -> k1 = k2. Proof. intros H1 H2. set (p1 := BinCoproductIn1 CC · k1). set (p2 := BinCoproductIn2 CC · k1). rewrite (BinCoproductArrowUnique _ _ CC _ p1 p2 k1). apply pathsinv0. apply BinCoproductArrowUnique. unfold p1. apply pathsinv0. apply H1. unfold p2. apply pathsinv0. apply H2. apply idpath. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.ProductCategory.