Dependent types are super confusing, but at the same time they feel easier than normal ones.

I guess that makes sense for every advanced concept - as a concept wouldn’t exist if it isn’t making things easier when you finally get it.

I think that they are hard to learn because we consider them as something fancy, but they actually are the simpler thing, and it’s normal, first-order types that are weird.

With first-order types, you have two things — types and values, dependent types there is only one thing, type e.g. “Number” is a type of “Set” in the same way that 1 is a type of “Number”.