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, 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 ⊤?