1: \begin{definition}

2: Let $X \in \permnom$ and $Y \in \sbnom$.

3: We define a $\perm$-equivariant map $\phi$ as follows:

4: \[ \phi \colon (X \wandto U(Y)) \to U(F(X) \sbto Y) \]

5: is defined by using the composition

6: \[ F(X \wandto U(Y)) \times F(X) \xrightarrow{p^{-1}} F((X \wandto U(Y)) \sepprod X) \xrightarrow{F(\ev)} FU(Y) \xrightarrow{\epsilon} Y, \]

7: where $p^{-1}$ is from Theorem~\ref{thm:monoidal} and $\ev$ is the evaluation map of the exponent $\wandto$.

8: By Currying and the adjunction, we obtain $\phi$:

9: 

10: \begin{prooftree}

11: \AxiomC{$F(X \wandto U(Y)) \times F(X) \to Y$}

12: \RightLabel{\, by Currying}

13: \UnaryInfC{$F(X \wandto U(Y)) \to (F(X) \sbto Y)$}

14: \RightLabel{\, by Theorem~\ref{thm:adjunction}}

15: \UnaryInfC{$\phi \colon (X \wandto U(Y)) \to U(F(X) \sbto Y)$}

16: \end{prooftree}

17: \end{definition}