Show how lack of universe levels would create contradiction in homotopy type theory (in Agda)
The problem is not specific to homotopy type theory. In type theory in general, if there is a type of all types, then every type is inhabited. This was shown first by Girard who encoded the Burali-Forti paradox in type theory.

A simplification of the paradox was found by Hurkens. Here is Agda code for it, and here is Coq code.