`A` is a type, yes. Whether `Type` is a type depends on what type system you're working in. If `Type` is its own type, then it turns out you can use that to do

`A` is a type, yes. Whether `Type` is a type depends on what type system you're working in. If `Type` is its own type, then it turns out you can use that to do infinite recursion (this is called Girard's paradox). Dependent types are often used for proving theorems, where infinite recursion corresponds to circular reasoning—a big no-no. So, in many dependently typed languages, `Type` is not its own type (instead, it's common to have an infinite tower of types: `42` has type `Int`, `Int` has type `Type0`, `Type0` has type `Type1`, `Type1` has type `Type2`, and so on). However, if the programming language is just used for programming and not for proving, then it's perfectly fine (and quite convenient) to have `Type` be its own type.