proposition: Lemma CoproductsBool {C : category} (HC : BinCoproducts C) : Coproducts bool C.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.ProductCategory