In $\lambda C$ we have abstraction over types, type constructors, etc. Are there any works out there that explore quantification over variables that inhabit these entities? For example, in simple type theory, we get to quantify over variables of any types, e.g., individuals, represented by $\fora...