Strengthening agent shapes

In the wiring diagram formalism for agent-based programs, it is possible to weaken an agent shape $A$ (i.e. the guarantee of having a distinguished map $A\rightarrow X$ into some state of the world $X$) to some agent shape $B$ by precomposing the distinguished $A$ with a map $A \leftarrow B$.

If we want to *strengthen* the agent shape via a map $A\rightarrow B$, AlgebraicRewriting currently has a `Strengthen` box but this works by pushout: it *adds* to the world in order to guarantee that given one has a distinguished $A$ that one will get a distinguished $B$.

What we need is a way to strengthen a distinguished $A$ to a distinguished $B$ via $f:A\rightarrow B$ without mutating the world state. There are two problems with this: 1.) there may be no way of extending $A\rightarrow X$ along $f$, 2.) there might be *many* ways of doing so. The first case is addressed by having a "failure" output wire also typed $A$. The second case can be addressed by making a uniformly random choice. Call the box which does this `StrengthenChoice`.

This feature is very common and has historically been modeled via abuse of the `Query` box: that box is meant to be used by running some algorithm for every such match of a certain shape, with the subroutine feeding back into a special input port which signals to switch to the next match. We abuse this by never closing the loop: enter the query box, pick an arbitrary match (which could strengthen the agent shape) and then just continue along, never to loop back. While this has the same semantics to `StrengthenChoice`, it has different performance characteristics and is overkill (e.g. it's nice when all the boxes in a rewrite program are stateless).

To motivate this with a particular example inspired by Nate Osgood and Xiaoyan Li, consider modeling contract rate semantics:

We come in with a distinguished infected person. We pick another person at random (not knowing whether they are infected or not). We then check whether they are susceptible or not (if they are, this information gets promoted to the "type level", i.e. the agent shape records that if we are in the top wire of the second box then we are guaranteed to have a distinguished infected and distinguished susceptible person). Then we can flip a biased coin given this choice of arbitrary other person who happens to be susceptible and if heads execute an infection event.