Generalising levels in our category library.

In most forms (all except Concrete0), there are in fact three
different levels, and we had been forcing them to be equal. Removing
this requirement clogs things up with more implicit level arguments,
but simplifies a few things.
Categories of truncated maps