# 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?

• Asking for Agda code is likely to be outside the range of topics here on CS.SE. A more general question about why we can't accept Type:Type, and Girard's paradox might be appropriate. You could try Barendregt's book chapter "lambda calculi with types" Th.5.5.3. It is not a simple result. – chi Jun 15 '18 at 16:33