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 is exactly the point being made. That you can spot right away that something "doesn't make sense".

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.

That happens all the time with ordinals.