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 ¬(¬⊤ ⊗ ¬⊤) (a.k.a. ⊤ ⅋ ⊤)?  Equivalently, is there an arrow in a dialogue category (with monoidal unit ⊤ and negation functor ¬) from ¬⊤ to ⊤?