2.0

This pull request introduces compatibility with the latest Agda release 2.3.2.2, but necessarily breaks compatibility with previous versions (the Agda developers have decided to preload their own universe levels).

Some other minor uncontroversial additions included.