Types

atomic: T; complex: given types A, B we have

A ⊸ B	linear implication
♢d A	diamond with dependency label d
□d A	box with dependency label d

Terms

atomic: c constants (i.e. words), x variables; complex: given terms M, N we have

M N	⊸ elimination, function application
λx.M	⊸ introduction, abstraction
▽d M	diamond elimination
△d M	diamond introduction
▼d M	box elimination
▲d M	box introduction