proposition: Lemma CoproductsHSET (I : UU) (HI : isaset I) : Coproducts I HSET.
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Coproducts UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Pushouts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Categories.HSET.Core UniMath.Combinatorics.FiniteSets UniMath.MoreFoundations.Subtypes