I see. So, to confirm my understanding, in FOL, we can quantify over variables of type, e.g., $A \to B \to ...$ as long as the individuals of the domain are of type $A \to B \to ...$? If so, is this the reason why ZF is a first-order theory even some axioms quantify over sets, e.g., Axiom of union, i.e. the individuals are sets?

Thanks. So do you know why is the common answer to what is a higher-order logic, like you pointed out, is that any logic in which we intend to have quantifiers over "functions" or "sets"? Is it a special case?

Thanks. Just to clarify my understanding: the quantification of variables of type $A \to B$ is valid in FOL because the elements of the domain in question are of type $A \to B$. If so, how come the quantification over $(A \to B) \to (A \to B)$ is still valid in FOL?