Proposition is_inj_internal_transpose {x y z : V} {f g : x ⊗ y --> z} (p : internal_transpose f = internal_transpose g) : f = g. Proof. unfold internal_transpose in p. pose (maponpaths (λ z, sym_mon_braiding _ _ _ · z #⊗ identity _ · internal_eval _ _) p) as q. cbn in q. rewrite !assoc' in q. rewrite !internal_beta in q. rewrite !assoc in q. rewrite !sym_mon_braiding_inv in q. rewrite !id_left in q. exact q. 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.