I believe I once had a proof of this proposition, but it's been lost to the mists of time and old hard drives, so who knows if it was correct, and try as I might I can't seem to reproduce it.

Is it possible, in Melliès' [tensorial logic](https://www.irif.fr/~mellies/tensorial-logic.html), to give a proof of ¬(¬1 ⊗ ¬1) (a.k.a. 1 ⅋ 1)?  Equivalently, is there an arrow in a dialogue category (with monoidal unit 1 and negation functor ¬) from ¬1 to 1?