The slides of my talk given at AIM in Nottingham is available from http://www.cs.swan.ac.uk/~csetzer/slides/index.html (first item). It contains my idea how to define coalgebras via nested destructor patterns and some suggestions for how to deal with it syntactically. Anton