proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric