## Type Labels II

12/19/09

### Extending the notation

At first site, having an equivalence between types (lower case letters a..v) and monadic predicates (upper case A..V) might seem limiting. But it can be extending to a degree by introducing definitions for more complex single variable predicates. For example, say you have

(Mx∧Dx)⊃Nx (*notice the free variable x*)

as a fancier category (those things which if they are M and D are also N), then you could introduce a monadic predicate definition for this, via an equivalence eg