Lemma yoneda_exponentials_iso_is_preserves_exponentials (X Y Z : C) : z_iso_mor (yoneda_exponentials_iso X Y Z) = pr1 (preserves_exponentials_map _ _ (yoneda_preserves_binproduct _ BP) _ _) Z. Proof. apply funextsec. intro f. apply nat_trans_eq_alt. intro d. apply funextfun. intro x. cbn. do 2 ( refine (!maponpaths (λ x, _ · BinProductArrow _ _ x _ · _) (id_right (BinProductPr1 _ _)) @ _); refine (!maponpaths (λ x, _ · BinProductArrow _ _ _ x · _) (id_right (BinProductPr2 _ _)) @ _); refine (maponpaths (λ x, x · _) (postcompWithBinProductArrow _ _ _ _ _ _ _) @ !_) ). refine (assoc _ _ _ @ _). refine (maponpaths (λ x, x · _) (postcompWithBinProductArrow _ _ _ _ _ _ _) @ _). apply (maponpaths (λ x, x · _)). refine ( maponpaths (λ x, BinProductArrow _ (BP X (pr1 (Exp X) Y)) x _) _ @ maponpaths (λ x, BinProductArrow _ (BP X (pr1 (Exp X) Y)) _ x) _ ). - apply id_right. - refine (maponpaths (λ x, x · _) (id_right _) @ _). refine (maponpaths (λ x, x · _) (id_right _) @ _). refine (maponpaths (λ x, _ · x) (id_left _) @ _). exact (!id_right _). Qed.
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.