# Examples of Universe inconsistency in normal use of dependent types

In dependent types, Type : Type results in inconsistency (Girard's or Hurken's paradox).

Are there examples of universe inconsistency (where assuming Type : Type would result something that is false) showing up "accidentally" when not deliberately trying to prove it (when proving unrelated things)?

This is a hard question to answer, in part because it's unclear what it means to get something "by accident". Regularly, though, people run into the Universe Inconsistency error of Coq, as some quick googling will show (e.g. here). This certainly sometimes happens by accident, sometimes in the attempt at showing inconsistencies or testing the limits of the prover.