Tags: Category, Promonoidal category of spliced arrows, session do-notation. Context theory for monoidal categories