Combinatorial insertions

Tags: Type theory, do-notation - theory of symmetric monoidal categories.