Lemma InitialToCoproduct (I : Initial C): ∏ (a : stn 0 -> C), Coproduct (stn 0) C a. Proof. intros a. use (make_Coproduct _ _ _ I (λ i : stn 0, fromempty (weqstn0toempty i))). intros c g. use unique_exists. - apply (InitialArrow I c). - intros i. apply (fromempty (weqstn0toempty i)). - intro; apply impred_isaprop. intro; apply homset_property. - intros. apply InitialArrowUnique. 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.