Definition internal_hom_equiv (x y z : V) : (x --> y ⊸ z) ≃ (x ⊗ y --> z). Proof. use weq_iso. - exact (λ f, f #⊗ identity y · internal_eval y z). - exact (λ f, internal_lam f). - abstract (intro f ; cbn ; use internal_funext ; intros w h ; rewrite tensor_split ; rewrite !assoc' ; rewrite internal_beta ; rewrite !assoc ; rewrite <- tensor_split ; apply idpath). - abstract (intro f ; cbn ; apply internal_beta). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import MonoidalNotations.