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 Gir

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/Functors___-Applicative-Functors___-and-Monads/Universes/ https://lean-lang.org/functional_programming_in_lean/Functor...