[enricozb]

Perhaps I overstated how related the two were. I was pulling mostly from the Lean documentation on Universes [0]

> The formal argument for this is known as Girard's Paradox. It is related to a better-known paradox known as Russell's Paradox, which was used to show that early versions of set theory were inconsistent. In these set theories, a set can be defined by a property.

[0]: https://lean-lang.org/functional_programming_in_lean/Functor...