Combinatorial insertionsLast updated Oct 7, 2024Tags: Type theory, do-notation - theory of symmetric monoidal categories.