Units and second order in linear logic

Hello Frogs,

There are again some thoughts on the problem of the identity of proofs. 
This time they concern second order linear logic.

It is well-known that the units 1, 0, one, bot of linear logic, can be 
expressed by using second order quantifiers (and multiplicative 
connectives).

We have:

0   = \forall a.a
top = \exists a.a

1   = \forall a.-a # a
bot = \exists a.-a * a

(where the # is the par, and the * is the tensor of linear logic, and -a 
is the negation of a.)

The question that arises now is the following:

  (*)   Should these logical equivalences also be isomorphisms
        in a category theoretical axiomatization of the logic?

I take votes:

For 1/bot:  YES  NO

For 0/top:  YES  NO


Seriously, I could not find any axiomatisation for second order MLL, which 
I could check.

But we know that in the category of coherent spaces they are isos. 
However, there we also have 1=bot and 0=top, which is certainly not the 
case in the agreed on axiomatization for MLL/MALL (*-autonomous for MLL, 
initial/terminal object for 0/top)

On the other hand, if we look at the sequent calculus (or CoS, or proof 
nets), it becomes highly questionable whether we should have these isos. 
Just by doing the exercise of eliminating the cut from the composition of 
the canonical proofs for the implications, we see that we have to identify 
the proof

                            id ----------
                                 -a , a
                             # ----------
                                 -a # a
  1 ---                 bot --------------
     1                        bot, -a # a
*  --------------------------------------
            1 * bot,       -a # a
E  --------------------------------------
    \exists a.a * -a,       -a # a
A  --------------------------------------
    \exists a.a * -a, \forall a. -a # a


with the proof


id --------                    id ------
     a, -a                         -a,a 
* --------------------------------------
             a * -a,        -a, a
# --------------------------------------
             a * -a,       -a # a
E --------------------------------------
   \exists a.a * -a,       -a # a
A --------------------------------------
   \exists a.a * -a, \forall a. -a # a


which seems rather weird to me.

What do you think? What should the answer to (*) be ?

Ciao,
Lutz