type ** : Type -> Type -> Type
var a < c
var {a}: c -> d
class Monad: Type -> Type
type a : Monad := \ t . t -> t
free type Term ::=  Var Variable | Lam Variable Term | App Term Term 
type WNet={(sys,i,o): T * T * T . i = o } 
var a+ : Type
var - 
var []+
op a:? b
op a: ? b