[efr-000U]

We can consider two strategies for constructing the "full" triple category of controlled processes:

1. Give a construction of the double category of controlled processes and all lens reparametrizations, in a functorial way so that we can extend this to a triple category
2. Prove that freely(?) adding companions, in a suitable sense, of each globular chart reparametrization, gives the right thing (this should amount to checking a composition rule)