Definition yoneda_exponentials_iso (X Y Z : C) : z_iso ((yoneda C (exp (Exp X) Y) : _ ⟶ _) Z) ((exp (Exponentials_PreShv (yoneda C X)) (yoneda C Y) : _ ⟶ _) Z). Proof. refine (hset_equiv_weq_z_iso _ _ _). refine (yoneda_weq _ _ (exp (Exponentials_PreShv _) _) ∘ _). refine (adjunction_hom_weq (pr2 (Exponentials_PreShv _)) _ _ ∘ _). refine (invweq (z_iso_comp_right_weq (preserves_binproduct_to_z_iso _ (yoneda_preserves_binproduct _ BP) _ (BinProducts_PreShv _ _)) _) ∘ _). refine (weq_from_fully_faithful (yoneda_fully_faithful _) _ _ ∘ _). refine (invweq (adjunction_hom_weq (pr2 (Exp X)) _ _) ∘ _). refine (invweq (weq_from_fully_faithful (yoneda_fully_faithful _) _ _) ∘ _). exact (invweq (yoneda_weq _ _ (yoneda _ _))). 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.