Definition yoneda_preserves_exponentials : preserves_exponentials Exp (Exponentials_PreShv) (yoneda_preserves_binproduct _ BP). Proof. intros X Y. apply nat_trafo_z_iso_if_pointwise_z_iso. intro Z. use is_z_isomorphism_path. - exact (z_iso_mor (yoneda_exponentials_iso X Y Z)). - exact (yoneda_exponentials_iso_is_preserves_exponentials X Y Z). - apply z_iso_is_z_isomorphism. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Adjunctions.Core. 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.Core.Prelude. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.YonedaBinproducts.