Lemma Exponentials_HSET_slice (X : HSET) : Exponentials (BinProducts_HSET_slice X). 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.
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.