Lemma CoproductsBool {C : category} (HC : BinCoproducts C) : Coproducts bool C. Proof. intros H. use make_Coproduct. - apply (HC (H true) (H false)). - induction i; apply (pr1 (HC (H true) (H false))). - use (make_isCoproduct _ _ C); intros c f. set (uniqex := pr2 (HC (H true) (H false)) c (f true) (f false)). use unique_exists. + exact (pr1 (pr1 uniqex)). + abstract (cbn; induction i; [exact (pr1 (pr2 (pr1 uniqex))) | exact (pr2 (pr2 (pr1 uniqex)))]). + abstract (intros x; apply impred; intros; apply C). + abstract (intros h1 h2; apply (maponpaths pr1 (pr2 uniqex (h1,,(h2 true,,h2 false))))). 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.