proposition: Lemma ProductsHSET (I : UU) : Products I HSET.
proof: Proof. intros A. use make_Product. - exists (∏ i, pr1 (A i)); apply isaset_forall_hSet. - simpl; intros i f; apply (f i). - apply make_isProduct; try apply homset_property. intros C f; simpl in *. use tpair. * exists (λ c i, f i c); 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; apply funextsec; intro i; rewrite <- ht; apply idpath ]). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.WeakEquivalences UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Pullbacks UniMath.CategoryTheory.Limits.Graphs.Equalizers UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Categories.HSET.Core