Internal Languages for Monoidal Categories

My earliest work developed internal languages (syntax) for various monoidal and related categories. The significance of such languages changed completely with the advent of linear logic and its incorporation into type systems and languages bit I did not take part in these developments.

Languages for monoidal categories presented the general framework which was further developed in

Languages for triples, bicategories and braided monoidal categories
A note on natural numbers objects in monoidal categories
Coherence in Category Theory and the Church-Rosser Property

The structure of free closed categories provides a simple decision procedure for determining equality of arrows in a free monoidal closed category.