As Peter pointed out, there is a notion of container of morphisms (linear arrow). I had actually never realized that the “dependent container” linear arrow could be backported to “plain” containers.

From the South of France point of view, morphisms for dependent containers are “proof irrelevant”: a morphism is a relation with a proof that it is a simulation. (It is an obvious generalization of the container morphisms or of usual simulation relations.)
However, equality of morphisms is defined as extensional equality of the relations…

This was necessary for the work I was doing with “dependent containers”:
simulations become some kind of continuous function (extensionality is thus important); and it latter became a necessary condition to obtain a model for _full_ linear logic.
(Without it, I wouldn’t be able to get _classical_ linear logic…)

Plain containers are dependent containers with a singleton set of states; it is thus stupid to identify simulations extensionally.

So:
* plain containers form a symmetric monoidal closed category (modeling intuitionistic multiplicative linear logic)

* there is no dualizing object (in the dependent case, it is given by the trivial dependent container SKIP; but the proof that it is dualizing requires classical logic.)

* I don’t think there is a BANG operator: the set of states wouldn’t be a singleton. (For dependent containers, the BANG is given by the free tensor comonoid…)

* Are plain containers closed under product and coproduct? I don’t expect them to be. (In my case, the product of two plain containers is not a plain container: its set of states would contain two elements. Moreover, product and coproduct coincide.)

Hmm… That’s about it for now…