Every time I want to quickly understand something about an advanced type system or programming language concept I get lost when I see something like this on Wikipedia: Linear type systems are the internal language of closed symmetric monoidal categories, much in the same way that simply typed lambda calculus is the language of Cartesian closed categories. More precisely, one may construct functors between the category of linear type systems and the category of closed symmetric monoidal catego...
