proposition: Lemma Exponentials_functor_HSET : Exponentials CP.
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.AxiomOfChoice UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.NNO UniMath.CategoryTheory.SubobjectClassifier UniMath.CategoryTheory.Categories.Type.Core UniMath.CategoryTheory.Categories.Type.MonoEpiIso UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.covyoneda UniMath.CategoryTheory.EpiFacts UniMath.CategoryTheory.Monics UniMath.CategoryTheory.SplitMonicsAndEpis UniMath.CategoryTheory.ElementaryTopos UniMath.CategoryTheory.PowerObject UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.Categories.HSET.Univalence