internal language
The internal language of some mathematical structure is the left adjoint to an obvious forgetful functor into some generators.
- monoids use lists.
- Cartesian multicategories have the theory of cartesian multicategories.
- monoidal categories use string diagrams.
- premonoidal categories use string diagrams with runtime.
- effectful categories use string diagrams with runtime.
- symmetric monoidal categories use linear-interchanging do-notation.
- symmetric effectful categories use linear do-notation.
- Freyd categories use non-linear do-notation.
- Compact closed category use graphs.
- double categories use marked bicategorical string diagrams.
- Message theories are an internal language for physical monoidal multicategories generated by states.
- cartesian closed categories use simply-typed lambda calculus.
- Posetal linear bicategory use Pierce diagrams.