Generally what we're talking about is the ability to say something like "for all types X which satisfy a predicate P, we have this code". The ability to quantify over "all" types is a key property of dependently typed languages. Likewise, a lot of Haskell's ability to simulate DT languages comes from its ability to reason about HKTs.

In a DT language you have something called a Pi type which is a bit like a function type. An example would be to compare the types of two functions which, essentially, determine whether two integers are coprime

    coprime1 :      Int  ->      Int  -> Bool
    coprime2 : (a : Int) -> (b : Int) -> Maybe (IsCoPrime a b)

The important part is to look past the syntax and note that IsCoPrime is a type which depends upon the values of the first two arguments. Another way of reading this is as follows

    coprime3 : forall (a b : Int), Maybe (IsCoPrime a b)

this emphasizes that the type of `coprime3` is quantifying over all values in Int.

Then we can take this idea to the higher-kinded level by looking at the type of, say, monoids

     monoid : forall (A : Type), 
              { zero : A
              , plus : A -> A -> A
              , leftId  : forall (a : A), plus zero a = a
              , rightId : forall (a : A), plus a zero = a
              , assoc   : forall (a b c : A) , plus a (plus b c) =
                                               plus (plus a b) c
              }

Here we can see that the `forall` notation lets us freely abstract over "all types" just like we previously abstracted over "all values". This continues to work at every level. For instance, we can note that `monoid` above is "a type of types" or maybe a "specification" and we can abstract over all "all specifications" as well

    specProperty : forall (S : Type -> Type), P S

Surely your monoid example should be a Sigma type (`exists`), not a Pi type (`forall`), since a monoid is a specification of data for a single type A, not for all types A. Indeed, the empty type has no monoid structure, so the Pi type you wrote down is necessarily empty.

Oh, yup. Surely indeed! I need my checker clearly