proposition: Theorem FinOrdCoproducts_from_Initial_and_BinCoproducts : Initial C -> BinCoproducts C -> FinOrdCoproducts C.
proof: Proof. intros I BinCoprods n. induction n as [|n IHn]. - exact(InitialToCoproduct I). - apply coproducts_stn_Sn. exact(coproducts_stn_unit IHn BinCoprods). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Initial