The context of this article is the programme to develop monoidal bicategories with a feedback operation as an algebra of processes, with applications to concurrency theory. The objective here is to study reachability, minimization and minimal realization in these bicategories. In this setting the automata are 1-cells, in contrast with previous studies where they appeared as objects. As a consequence, we are able to study the relation of minimization and minimal realization to serial composition of automata using (co)lax (co)monads. We are led to define suitable behaviour categories and prove minimal realization theorems that extend classical results.

We introduce the notion of strongly concatenable process as a refinement of concatenable processes (Degano et al. 1996), which can be expressed axiomatically via a functor [Qscr ](_) from the category of Petri nets to an appropriate category of symmetric strict monoidal categories, in the precise sense that, for each net N, the strongly concatenable processes of N are isomorphic to the arrows of [Qscr ](N). In addition, we identify a coreflection right adjoint to [Qscr ](_) and characterize its replete image, thus yielding an axiomatization of the category of net computations.

We show how to solve the word problem for simply typed λβη-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is [Pscr ]-category theory, a version of ordinary category theory where each hom-set is equipped with a partial equivalence relation. The part of [Pscr ]-category theory we develop here is constructive and thus permits extraction of programs from proofs. It is important to stress that in our method we make no use of traditional proof-theoretic or rewriting techniques. To show the robustness of our method, we give an extended treatment for more general λ-theories in the Appendix.