|
|
|
|
|
|
by enricozb
131 days ago
|
|
|
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... |
|
|