Lemma ExponentialsType : Exponentials BinProductsType. Proof. intro X. unfold is_exponentiable. unfold is_left_adjoint. refine (exp_functor X,, _). unfold are_adjoints. use tpair. - use make_dirprod. + use make_nat_trans. * intro Y; cbn. unfold exp_functor_ob. exact (flip make_dirprod). * intros ? ? ?; reflexivity. + use make_nat_trans. * intro Y; cbn. unfold exp_functor_ob. exact (λ pair, (pr2 pair) (pr1 pair)). * intros ? ? ?; reflexivity. - use make_form_adjunction; reflexivity. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Categories.Type.Core. Require Import UniMath.CategoryTheory.Categories.Type.Limits.