Lemma limits_isBinCoproduct_from_isBinCoproductCocone (C : category) {a b c} (u : C ⟦ a, c⟧)(v : C ⟦ b, c⟧) : isBinCoproductCocone _ _ _ _ u v -> Limits.BinCoproducts.isBinCoproduct C a b c u v. Proof. intro h. set (CC := make_BinCoproductCocone _ _ _ _ _ _ h); simpl. intros x f g. use unique_exists; simpl. - apply (BinCoproducts.BinCoproductArrow CC f g). - abstract (split; [ apply (BinCoproducts.BinCoproductIn1Commutes _ _ _ CC) | apply (BinCoproducts.BinCoproductIn2Commutes _ _ _ CC)]). - abstract (intros h'; apply isapropdirprod; apply C). - intros h' [H1 H2]. eapply (BinCoproducts.BinCoproductArrowUnique _ _ _ CC). + exact H1. + exact H2. 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.