I think the main references for this are Jacobs's book <i>Categorical Logic and Type Theory</i> (Chapter 8), and also Crole's <i>Categories for Types</i>.

The rough idea is to do categorical logic over the \`algebraic theory of types'. 
That is, you consider a category whose objects are finite products of a certain object $\mathit{Type}$, and whose morphisms $A \to \mathit{Type}$ are thought of as types with free type variables in $A$. Then, models are fibrations over such categories, of which you ask for more structure to be able to quantify over predicates. By carefully tuning what you demand, you may obtain quantification over all kinds of higher-order predicates, but there are ways of sticking to second-order logic.