Higher-order, multi-sorted, non purely equational version of universal algebra ? I have been looking around, unsuccessfully, for generalizations of universal algebra based on higher-order logic (rather than first order) and where the relations are not purely equational.  Motivation:  I need a "theory of syntax" for presentations of higher-order, non-equational theories.  Furthermore, I want to be able to specify 'combinators' over these presentations, rigorously.
I am aware of Lawvere theories, but these are still equational (and neither particularly higher-order, though the multi-sorted generalization seems straightforward enough).  There is a beginning of model theory done in a logical independent way, i.e. model theory over an institution; but that seems to concentrate on the model-theoretic aspects, rather than the universal algebra aspects. Perhaps what I am looking for are sketches?
[Edit:] From the various answer below, it seems I should be asking the question "how can I view type theory as a theory of syntax"?  Somehow, that seems like an 'implementation' (as it requires a fair bit of 'encoding'); for example, to express the 'theory of categories' [i.e. (Obj, Mor, id, src, trg, $\circ$) and 5-6 axioms, I need a dependent record.  Plus what is a sort (and sort constructor for Mor), what is an operation, and what is in Prop?  Universal algebra cleanly separates these.
A good question was asked: what theorems do I want?  Well, whatever operations I make on theories, well-formedness of the results will require discharging some obligations -- these obligations should all be finitely expressible (and automatically well-formed).  Furthermore, the resulting syntactic objects and their morphisms should form a finitely co-complete category.  Note that I expect that deciding if a given (presentation of a ) theory has a model to be undecidable.
 A: Lawvere theories generalize to higher-order logic in a straightforward way. A first-order hyperdoctrine is a functor $\mathcal{P} : C^{\mathrm{op}} \to \mathrm{Poset}$ where $C$ has products and is used to interpret terms in context, plus a small herd of conditions to make substitution and quantifiers work out right. 
If you want a hyperdoctrine that can interpret higher-order predicate logic, what you additionally want is to (a) require $C$ to be cartesian closed, and (b) $C$ should have an internal heyting algebra $H$ with the property that for each $X$ in $C$, $\mathit{Obj}(\mathcal{P}(X)) \simeq C(X, H)$. Basically, $H$ models the sort of propositions, and the cartesian closure lets you freely interpret lambda-terms denoting predicates and relations. The bijection $\mathit{Obj}(\mathcal{P}(X)) \simeq C(X, H)$ tells you that the morphisms into $H$ actually do correspond to truth values in context $X$, so you can interpret a higher-order term by interpreting a proposition in $\mathrm{Poset}$ via the functor $\mathcal{P}$, and then transporting it back into $C$. 
(I would have made this a comment, but it was too long.) 
