Let us summarise. We have moved so far in three dimensions. From simple types we moved to second order; from second order we moved to high order constructors. So, we moved in two different dimensions here. But then we moved also towards dependent types, which is a dimension orthogonal to the previous ones.

---