Chapter X of Mac Lane and Moerdijk's Sheaves in Geometry and Logic focuses on Classifying topoi. The basic concept in the early pages is the one of geometric formula, which is by definition a first-order formula.
Now, it is possible that it comes clear later in the book, but just for curiosity: is there a version of "Classifying topos" in higher order logic? I.e., can one introduce similar notions when the language is not first-order, and so "classify" kinds of objects which are intrinsically higher-order?
Sorry if the question is vague (hope it has at least sense), but before going through I would just like to satisfy this curiosity.
Thank you in advance.