Lemma BinCoproductArrowEta (a b : C) (CC : BinCoproductCocone a b) (x : C) (f : BinCoproductObject CC --> x) : f = BinCoproductArrow CC (BinCoproductIn1 CC · f) (BinCoproductIn2 CC · f). Proof. apply BinCoproductArrowUnique; 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.