Lemma BinCoproduct_endo_is_identity (CC : BinCoproductCocone a b) (k : BinCoproductObject CC --> BinCoproductObject CC) (H1 : BinCoproductIn1 CC · k = BinCoproductIn1 CC) (H2 : BinCoproductIn2 CC · k = BinCoproductIn2 CC) : identity _ = k. Proof. use colim_endo_is_identity. intro u; induction u; simpl; assumption. Defined.
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.