write out the bigger structure as discussed between fab/jelle

[wires]

so this discussion

@FabrizioRomanoGenovese can you put in the stuff you discussed in the earlier meeting

[FabrizioRomanoGenovese]

Sure. Just one comment about the picture: $X$ has type $Mor(FSMC_b)$.
Here $FSMC$ stands for "free symmetric monoidal category". A term of this type should be generated by a bunch of objects $GenObj$ and a bunch of generating morphisms $GenMorph$. In detail we should have:

• a $o:GenObj$ which generates $Obj(t)$ (this is just the free commutative monoid on $t$)
• a $m:GenMor$, together with mappings $source, target:GenMorph -> Obj(t)$ that say who are domains and codomains of each morphism.

From this one should be able to obtain $FSMC(o,m,source,target)$, where a term of this type is a legitimate composition of morphisms in the category.