Conor has some further ideas that must be somehow related about putting well-orders on positions, that are somewhere in this blog. They both seem

to involve putting some structure on positions.

I am very curious about the relations between containers with quotients and “species of structures” a la Fiore/Joyal/.. . Species seem very oriented towards data-structures with a finite number of distinguishable positions.

]]>the easiest is probably to use setoids and define , where is just the “quotient” of modulo permutations of lists.

(Of course, we must require that the family of shapes is a family of setoids, indexed by a setoid: it must respect equality… This gets very messy…)

Then, an action/shape is just given by a tuple , and a reaction/position is just a tuple of , where each is a position in shape .

Note that this is not the same as the bang defined on interaction systems, since the number of actions/shapes is not determined by the state. In particular, while iterating the container, the number of shapes can change.

That is the free comonoid just means that it is the “smallest” such comonoid:

(1) there is an arrow

(2) there is an arrow

Those arrows satisfy some commutativity and associativity diagrams, and are universal in some sense (”free”).

A more abstract way to look at it is by saying that the functor from the category of containers to the category of -comonoids is adjoint to the obvious forgetful functor from -comonoids to the containers…

All of this seems very important to LL people, but I have to admit I don’t have strong intuitions about them…

About the link between container morphisms and simulations between interaction systems: the relation seems very subtle. When I wrote that container morphisms are all “equal” I had the “classical” notion of simulation: usual relations. In the case of containers, the set of states are trivial: . There is only one non-empty relation between two such sets: .

In a constructive setting, this is far more complex than that!

]]>kinds of morphisms seems very subtle. It seems to me that a dependent

container morphism (one with a *function* mapping high-level sorts to

low-level sorts) is the same as an interaction system morphism which happens to be (the graph of) a total function.

I can see, I think, that several different container morphisms can “satisfy” extensionally the same simulation relation, but not that all container morphisms are extensionally equal.

]]>seems to be as a quotient of

(here the second “n” is being used for the set “Fin(b)” or

.

About Pierre’s suggestion for a bang on plain containers, I take

it the idea is that

(1)

an angel’s move (shape) in the bang of a contrainer is a multiset of angel’s moves (shapes) in the unbagged container . We now have to arrange that the set of positions for a shape does not depend on the particular order in which a shape is given.

(2)

a demon’s response (position) to an angel’s move is (represented by) a permutation p of dom(a), and a function . Equality of representations is modulo permutations.

It is as iff the angel has an inexhaustible supply of slave devices

to which she can issue as many commands in parallel as she likes

(possibly none). But she has to wait for all the responses.

What does one have to show about this? That C! is the free comonoid generated by C? What is this in layman’s

terms?