internal language
The internal language of some mathematical structure is the left adjoint to an obvious forgetful functor into some generators.
There exists a correspondence between algebraic structures (the models or semantics, which we want to reason about) and combinatorial structures (their internal languages, which we use to talk about them). The chief example has always been the correspondence between Cartesian Closed Categories — models of intuitionistic logic — and the Simply Typed Lambda Calculus — their internal language (Huet, 1985), but many other internal languages capture similar categorical constructions. Note that the problem is not to find an internal language, it is to find a good one.
Other.
- double categories use marked bicategorical string diagrams.
- Message theories are an internal language for physical monoidal multicategories generated by states.
- Posetal linear bicategory use Pierce diagrams.
References.