Show how lack of universe levels would create contradiction in homotopy type theory (in Agda) The homotopy type theory book claims in section 1.3 that "As in naive set theory, we might wish for a universe of all types" but from this one could "deduce from it that every type, including the empty type representing the proposition False, is inhabited"

The reference that it gives uses notation that I don't understand, however.

Could someone write invalid Agda code which produces a element of $\bot$, but which would be valid if Agda had a single universe that contains itself?
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.