Let's say something about higher order recursive types: if we want to capitalise on co-inductive types, we can use them for representing data types, for representing syntax and for representative predicates in proof-theory.
Higher order in predicative quantification is really probably the only ingredient that is necessary for discussing predicates, because this is the way for expressing relation induction. Probably we do not need in predicative data type. We can just as well work with recursive data types.
We need also precise correspondence statements between the objects systems and the encoding systems. And these go by the name of adequacy theorems.