Hyperdoctrines and Monadic Second Order Logic
I don't know! 
No, your assumption is not right. You can quantify over higher-order functions and predicates in IHOL (in fact, predicates are just functions into a type of propositions). The setup looks a bit like this:

$$
\begin{array}{llcl}
\mbox{Sort} &amp; \omega &amp; ::= &amp;  \omega \to \omega \;\; | \;\; \omega \times \omega \;\; | \;\; 1  \;\;|\;\; \mathrm{prop}  \;\;|\;\; \iota\\
\mbox{Term} &amp; t &amp; ::= &amp; x \;\;|\;\; \lambda x.t \;\;|\;\; t\;t' \;\;|\;\; (t,t) \;\; | \;\; \pi_1(t) \;\;|\;\; \pi_2(t) \;\;|\;\; () \\
&amp;            &amp;  |  &amp; 
     p \Rightarrow q \;\;|\;\; \top \;\;|\;\; p \wedge q \;\;|\;\; \bot \;\;|\;\; p \vee q  \\
&amp; &amp; | &amp; \forall x:\omega.p \;\;|\;\; \exists x:\omega.p  \;\;|\;\; t =_\omega t' \\
&amp; &amp; | &amp; f(\vec{t}) 
\end{array}
$$


You give the usual typing rules to judge the well-formedness of a term. The first line of terms are the usual simply-typed lambda calculus, the second two lines are the propositions of higher-order logic (typed as elements of $\mathrm{prop}$), and the third line are whatever constants you use to form individuals (elements of $\iota$). 

Then the idea is that you want to extend the Kripke semantics for first-order intuitionistic logic to higher-order logic, by extending the hyperdoctrine semantics with additional structure. A first-order hyperdoctrine is a functor $P : C^\mathrm{op} \to \mathrm{Poset}$ between a category $C$ with products (used to interpret the terms in context), and a category of posets (the truth value lattices), satisfying some conditions to make substitution work right. 

To get to IHOL, you additionally assert that 


$C$ is cartesian closed (to model the ability to quantify over function types), and 
$C$ has an internal Heyting algebra $H$ satisfying the property that for every $\Gamma \in C$, $\mathit{Obj}(P(\Gamma)) \simeq C(\Gamma, H)$. You use $H$ to model $\mathrm{prop}$, and the isomorphism tells you that terms of type $\mathrm{prop}$ really do correspond to truth values.  


This structure is almost an "elementary topos". If you additionally require that $P(\Gamma)$ is a poset of subojects of $\Gamma$, then you're there. (This essentially says that you can add a comprehension principle to your logic.)