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