Definition preserves_exponentials_map {C₁ C₂ : category} {BC₁ : BinProducts C₁} {BC₂ : BinProducts C₂} (E₁ : Exponentials BC₁) (E₂ : Exponentials BC₂) {F : C₁ ⟶ C₂} (HF : preserves_binproduct F) (x y : C₁) : F(exp (E₁ x) y) --> exp (E₂ (F x)) (F y). Proof. use exp_lam. pose (preserves_binproduct_to_z_iso F HF (BC₁ x (exp (E₁ x) y)) (BC₂ (F x) (F (exp (E₁ x) y)))) as f. refine (inv_from_z_iso f · #F _). apply exp_eval. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.Core.Univalence.