Lemma CoproductsHSET (I : UU) (HI : isaset I) : Coproducts I HSET. Proof. intros A. use make_Coproduct. - exists (∑ i, pr1 (A i)). apply (isaset_total2 _ HI); intro i; apply setproperty. - simpl; apply tpair. - apply (make_isCoproduct _ _ HSET). intros C f; simpl in *. use tpair. * exists (λ X, f (pr1 X) (pr2 X)); abstract (intro i; apply idpath). * abstract (intros h; apply subtypePath; simpl; [ intro; apply impred; intro; apply has_homsets_HSET | destruct h as [t ht]; simpl; apply funextfun; intro x; rewrite <- ht; destruct x; apply idpath]). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Coproducts. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Pushouts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.MoreFoundations.Subtypes.