proposition: Lemma Products_HSET_slice I X : Products I (HSET / X).
proof: Proof. intros F. use make_Product. + use tpair. - exists (∑ x : pr1 X, ∏ i : I, hfiber_hSet (pr2 (F i)) x). abstract (apply isaset_total2; [apply setproperty|]; now intros x; apply impred_isaset; intro i; apply setproperty). - cbn. apply pr1. + intros i. use tpair. - intros H; apply (pr1 (pr2 H i)). - abstract (now apply funextsec; intros H; apply (!pr2 (pr2 H i))). + intros f H. use unique_exists. - use tpair; simpl. * intros x. exists (pr2 f x). intros i. exists (pr1 (H i) x). abstract (exact (!toforallpaths _ _ _ (pr2 (H i)) x)). * abstract (now apply funextsec). - abstract (now intros i; apply eq_mor_slicecat, funextsec). - abstract (now intros g; apply impred_isaprop; intro i; apply has_homsets_slice_precat). - abstract(simpl; intros [y1 y2] Hy; apply eq_mor_slicecat, funextsec; intro x; use total2_paths_f; [apply (toforallpaths _ _ _ (!y2) x)|]; apply funextsec; intro i; apply subtypePath; [intros w; apply setproperty|]; destruct f as [f Hf]; unfold hfiber; rewrite transportf_sec_constant, transportf_total2; simpl; rewrite transportf_const; now rewrite <- Hy). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.AxiomOfChoice UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.covyoneda UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Colimits