Lemma ProductsHSET (I : UU) : Products I HSET. 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.
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.WeakEquivalences. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Graphs.Equalizers. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Categories.HSET.Core.