# Substructural types, the lambda calculus, and CCCs

It's well known that the simply-typed lambda calculus corresponds to a cartesian closed category. How would substructural type systems be characterized in category theory?

For example, linear type systems correspond to closed symmetric monoidal categories. But what category-theoretic constructions correspond to affine type systems, ordered type systems, and relevant type systems?

• Affine type systems correspond to what some would call semicartesian closed monoidal categories. The categorical structure associated with relevant type systems probably has no standard name. I suppose it is a symmetric monoidal closed category with suitable natural transformations implementing duplication. For what concerns "ordered" type systems, I don't know exactly, are you talking about subtyping? – Damiano Mazza Jun 6 '17 at 16:16
• I don't understand what answer we're suposed to give. An entire research overfiew of various variants of the Curry-Howard correspondence for substructural type theory? That's a bit much. Perhaps this should instead be tagged as a reference-request. – Andrej Bauer Jun 7 '17 at 7:04
• @AndrejBauer Just tagged this as a reference-request. Variants of the Curry-Howard correspondence for substructural type systems are exactly what I'm looking for. Thank you – C. Bednarz Jun 7 '17 at 7:09
• Relevance type systems correspond to relevance monoidal categories. – Mike Shulman Jun 9 '17 at 8:22