むむ？

C内に確実に存在する射とか自然変換達をうまく組み合わせて、[A□X, B] → [A, [X, B] ] という同型射（可逆射）を具体的に構成できればいいのですが、これはなかなか難しいようです。Cがデカルト閉なら、型付きラムダ計算の結果を翻訳して具体的構成ができるかもしれません（僕はやったことありません）。

単純に、これじゃダメでしょうか？（Haskellで書いてますが、文意は推測できると思います。）

f :: ((a,x) -> b) -> (a -> (x -> b))
f h = \a -> \x -> h (a, x)

g :: (a -> (x -> b)) -> ((a,x) -> b)
g h' = \ (a, x) -> h' a x