Lemma Exponentials_functor_HSET : Exponentials CP. Proof. intro P. use left_adjoint_from_partial. - apply (exponential_functor_cat P). - intro Q; simpl; apply eval. - intros Q R φ; simpl in *. use tpair. + use tpair. * { use make_nat_trans. - intros c u; simpl. use make_nat_trans. + simpl; intros d fx. apply (φ d (make_dirprod (pr2 fx) (# R (pr1 fx) u))). + intros a b f; simpl; cbn; unfold prodtofuntoprod. apply funextsec; intro x. etrans; [|apply (toforallpaths _ _ _ (nat_trans_ax φ _ _ f) (make_dirprod (pr2 x) (# R (pr1 x) u)))]; cbn. repeat (apply maponpaths). assert (H : # R (pr1 x · f) = # R (pr1 x) · #R f). { apply functor_comp. } unfold prodtofuntoprod. simpl (pr1 _); simpl (pr2 _). apply maponpaths. apply (eqtohomot H u). - intros a b f; cbn. apply funextsec; intros x; cbn. apply subtypePath; [intros xx; apply (isaprop_is_nat_trans _ _ has_homsets_HSET)|]. apply funextsec; intro y; apply funextsec; intro z; cbn. repeat apply maponpaths; unfold covyoneda_morphisms_data. assert (H : # R (f · pr1 z) = # R f · # R (pr1 z)). { apply functor_comp. } apply pathsinv0. now etrans; [apply (toforallpaths _ _ _ H x)|]. } * abstract ( apply (nat_trans_eq has_homsets_HSET); cbn; intro x; apply funextsec; intro p; apply maponpaths; assert (H : # R (identity x) = identity (R x)); [apply functor_id|]; induction p as [t p]; apply maponpaths; simpl; now apply pathsinv0; eapply pathscomp0; [apply (toforallpaths _ _ _ H p)|]). + abstract ( intros [t p]; apply subtypePath; simpl; [intros x; apply (isaset_nat_trans has_homsets_HSET)|]; apply (nat_trans_eq has_homsets_HSET); intros c; apply funextsec; intro rc; apply subtypePath; [intro x; apply (isaprop_is_nat_trans _ _ has_homsets_HSET)|]; simpl; rewrite p; cbn; clear p; apply funextsec; intro d; cbn; apply funextsec; intros [t0 pd]; simpl; assert (HH := toforallpaths _ _ _ (nat_trans_ax t c d t0) rc); cbn in HH; rewrite HH; cbn; unfold covyoneda_morphisms_data; unfold prodtofuntoprod; cbn; now rewrite id_right). 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.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Arithmetic.NNO. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.Categories.Type.Core. Require Import UniMath.CategoryTheory.Categories.Type.MonoEpiIso. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.EpiFacts. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.SplitMonicsAndEpis. Require Import UniMath.CategoryTheory.ElementaryTopos. Require Import UniMath.CategoryTheory.PowerObject. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. assert (p : (BinProductsFromPullbacks PullbacksHSET TerminalHSET) = BinProductsHSET).