Definition sym_mon_closed_left_tensor_left_adjoint_universal (V : sym_mon_closed_cat) (x y : V) : is_universal_arrow_from (monoidal_left_tensor x) y (x ⊸ y) (sym_mon_braiding V x (x ⊸ y) · internal_eval x y). Proof. intros z f. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply homset_property | ] ; refine (internal_eta _ @ _ @ !(internal_eta _)) ; apply maponpaths ; refine (!(id_left _) @ _ @ id_left _) ; rewrite <- !sym_mon_braiding_inv ; rewrite !assoc' ; apply maponpaths ; rewrite !assoc ; rewrite <- !tensor_sym_mon_braiding ; rewrite !assoc' ; exact (!(pr2 φ₁) @ pr2 φ₂)). - refine (internal_lam (sym_mon_braiding V z x · f) ,, _). abstract (cbn -[sym_mon_braiding] ; rewrite !assoc ; rewrite tensor_sym_mon_braiding ; rewrite !assoc' ; rewrite internal_beta ; rewrite !assoc ; rewrite sym_mon_braiding_inv ; rewrite id_left ; apply idpath). 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.