A category PG whose objects are natural numbers and morphisms are port graphs
We can compose a \((m,n)\) port graph with a \((n, p)\) port graph \((V \sqcup V',[in,in'],[out,out'], i'')\)
\(V \sqcup V' \xrightarrow{[in,in']} \mathbb{N}\) maps elements of \(V\) according to \(in\) and elements of \(V'\) according to \(in'\) (likewise for out).
The bijection \(\bar m \sqcup O \sqcup O' \xrightarrow{i''} I \sqcup I' \sqcup \bar p\) is defined as \(i''(x)=\begin{cases}i(x) & i(x) \in I \\ i'(i(x))& i(x) \in \bar n \\ i'(x) & x \in O' \end{cases}\)
The identity port graph on \(n\) is \((\varnothing, !, !, id_{\bar n})\) where \(\varnothing \xrightarrow{!} \mathbb{N}\) is a unique function.
This category is a prop.
The monoidal product of two portgraphs... TODO