I'm probably at the level of "moderately skilled amateur" when it comes to type theory (I took courses in college about compilers and the math behind type theor

I'm probably at the level of "moderately skilled amateur" when it comes to type theory (I took courses in college about compilers and the math behind type theory like Hoare logic), but I got confused by the second sentence: > A function has a dependent type when the type of its result depends upon the value of its argument Pretty straightforward, and something I'm familiar with. > The type of all types is the type of every type, including itself. I...don't know what this means. It's unclear to me how to understand the meaning of "the type of every type", since I don't have an intuition of how to "combine" all of those types into something that I can reason about. My first instinct would be that it's saying it's a set, but if it contains itself, doesn't that run into Russel's paradox (unless they're assuming some specific set of axioms around set construction to solve this, which seems strange to leave implicit)? Am I missing something obvious, or is it kind of unclear what they're talking about here? Maybe my confusion is that I feel like the difference between "all" and "every" is ambiguous, so I don't know how to read this as circular other than logically grouping "all types" into one thing and "every type" into a group of separate things, only I don't know what that group even is.