And the idea in the context of the original post is that this is supposed to be a parody of a formal math definition in a paper or textbook (using Jabberwocky vocabulary instead of real math vocabulary).
Not that it makes sense anyway. Somehow πβπ and πβπ.
That is exactly the point being made. That you can spot right away that something "doesn't make sense".
No, the point was that πβπ is a typo and πβπ is what was intended. Type theory will reject the mistake but set theory will accept it. This is then presented as a reason why mathematicians should prefer type-theory-based proof assistants to set-theory-based ones, since the former will catch these kinds of mistakes while the later won't.
Thatβs possible. For instance, X = {{}} and U = {}. Or in general, if X_0 = {} and X_{i+1} = {X_0, ..., X_i}, then X_i is both an element and a subset of X_j whenever i < j.