proposition: Lemma Exponentials_HSET_slice (X : HSET) : Exponentials (BinProducts_HSET_slice X).
proof: Proof. intros f. exists (hfiber_functor _ f). use make_are_adjoints. - apply eta. - apply eps. - split. + intros x; apply eq_mor_slicecat, funextsec; intro x1. now apply subtypePath; [intro y; apply setproperty|]; reflexivity. + intros x; apply eq_mor_slicecat, funextsec; intro x1; simpl. use total2_paths_f; [apply idpath|]; cbn. apply funextsec; intro y. use subtypePath. * intro z; apply setproperty. * simpl. apply maponpaths. apply maponpaths. reflexivity. 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