Categorical equivalent of higher order logic From Simply typed lambda calculus and higher order logic, I get the impression that HOL is STLC + equality + equality axioms. I was wondering if there is a particular kind of category modelling this.
The structure you want is due to Andy Pitts, and is called a tripos. It extends the notion of hyperdoctrine, which gives a categorical model for first-order logic, with enough structure to model higher-order logic.
However, much more of the work in this part of categorical logic focuses on toposes instead of triposes, which are just a little bit more expressive than HOL (basically you get to form sets by comprehension, too, giving a model of set theory with bounded quantifiers).
References:

Andrew M. Pitts, The Theory of Triposes
Andrew M. Pitts, Tripos theory in retrospect