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