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