Proposition internal_lam_natural {x₁ x₂ y z : V} (f : x₁ --> x₂) (g : x₂ ⊗ y --> z) : f · internal_lam g = internal_lam (f #⊗ identity y · g). Proof. use internal_funext. intros w h. etrans. { rewrite tensor_split. rewrite tensor_comp_id_r. rewrite !assoc'. rewrite internal_beta. rewrite !assoc. rewrite <- tensor_split. apply idpath. } refine (!_). etrans. { rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. rewrite !assoc. rewrite <- tensor_split. apply idpath. } apply idpath. Qed.
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.