For an alphabet $\mathrm{\Sigma }$, let ${\mathrm{\Sigma }}^{\ast }$ be the free monoid of strings over $\mathrm{\Sigma }$. A formal grammar $𝐴$ is a family of types indexed by strings:

This definition views formal grammars directly as indexed families of types over strings (which equivalently form presheaves on the discrete category of strings). This view forms the central notion of the Dependent Lambek Calculus. For a given string $𝑤$, the type $𝐴(𝑤)$ represents the type of all valid parse trees for $𝑤$ according to the grammar $𝐴$. If the grammar cannot parse $𝑤$, then $𝐴(𝑤)$ is the empty type.