Impredicative polymorphism exercises: fix bug and comment

* The code typechecked but did not implement its specification. Fix this.
* Improve a comment.
Impredicative polymorphism exercises: make levels explicit

* Make universe levels explicit, to clarify what is happening.
* Parameterize id-type by level.
* Use uniformly ℓ instead of l for levels.

This was suggested (in part) by @Toxaris in:
https://github.com/Blaisorblade/Agda/commit/6b0d1815e7dffea8b1504ed18690490679c0c783#commitcomment-3691556
Impredicative polymorphism exercises: try out level-polymorphic types

Try implementing @Toxaris suggestion, and report on the strange error message.

https://github.com/Blaisorblade/Agda/commit/6b0d1815e7dffea8b1504ed18690490679c0c783#commitcomment-3691560