Lemma Products_HSET_slice I X : Products I (HSET / X). 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.
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.AxiomOfChoice. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits.