Lemma BinCoproducts_from_Colims : Colims_of_shape two_graph C -> BinCoproducts C. Proof. intros H a b. set (CC := H (bincoproduct_diagram a b)). use make_BinCoproduct. + apply (colim CC). + apply (colimIn CC true). + apply (colimIn CC false). + apply (make_isBinCoproduct _ C); intros c f g. use unique_exists. - apply colimArrow, (BinCoprod f g). - abstract (split; [ apply (colimArrowCommutes CC c (BinCoprod f g) true) | apply (colimArrowCommutes CC c (BinCoprod f g) false) ]). - abstract (intros h; apply isapropdirprod; apply C). - abstract (now intros h [H1 H2]; apply colimArrowUnique; intro x; induction x). Defined.
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.