Unfixing and recursion schemes for data types with binders.

Use fixed-point of endofunctors of endofunctors (that is initial algebras in the category of endofunctors) to define recursion schemes for data types with binders

Unfix binders

when your substitutions are in a fix

This library defines fixed points of endofunctors of the category of endofunctors with the purpose of generalising recursion schemes for data types with binders.

It is still in a very experimental state: for demonstration purpose only (though contributions welcome!)