Lemma ObjectToCoproduct: ∏ (a : stn 1 -> C), Coproduct (stn 1) C a. Proof. intros a. set (stn1ob := invweq(weqstn1tounit) tt). use (make_Coproduct _ _ _ (a stn1ob)). intros i. exact (idtoiso (! (maponpaths a (isconnectedstn1 stn1ob i)))). use (make_isCoproduct _ _ C). intros c g. use (unique_exists (g stn1ob)). intros i. rewrite <- (isconnectedstn1 stn1ob i). apply id_left. intros y. apply impred_isaprop. intros t. apply C. intros y X. rewrite <- (X stn1ob). apply pathsinv0. apply id_left. 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.