Left Residual in a Monoidal Category

A left residual in a Monoidal Category is a sort of Exponential Object in a Monoidal Category ( 𝒱 , ⊗ , I ) 𝒱 tensor-product 𝐼 (\mathcal{V},\otimes,I) whose evaluation map is left-biased. Explicitly, a left residual of B 𝐵 B by A 𝐴 A is an object A \ B \ 𝐴 𝐵 A\backslash B , along with an evaluation map e ⁢ v l : A ⊗ ( A \ B ) → B : 𝑒 subscript 𝑣 𝑙 → tensor-product 𝐴 \ 𝐴 𝐵 𝐵 ev_{l}:A\otimes(A\backslash B)\to B , along with a natural transformation

λ[−]:A⊗−→B→−→A\B\lambda[-]:{{A\otimes-}\to{B}}\to{{-}\to{A\backslash B}}

such that e ⁢ v l ∘ ( A ⊗ λ ⁢ [ f ] ) = f 𝑒 subscript 𝑣 𝑙 tensor-product 𝐴 𝜆 delimited-[] 𝑓 𝑓 ev_{l}\circ(A\otimes\lambda[f])=f and g = λ ⁢ [ e ⁢ v l ∘ ( A ⊗ g ) ] 𝑔 𝜆 delimited-[] 𝑒 subscript 𝑣 𝑙 tensor-product 𝐴 𝑔 g=\lambda[ev_{l}\circ(A\otimes g)] .