In the theory of programming languages and structural proof theory, one of the handiest techniques we have available is a method called "logical relations", in which you can prove properties of languages by taking the type structure of the language, and defining families of predicates or relations by induction on the type structure.

For example, if you want to prove that all definable functions in a language halt, you start by giving a predicate $P_X$ picking out the terms of base type $X$ which halt. Then, at higher type (say $A \to B$) you define $P_{A \to B}$ to pick out those terms which halt, and which additionally take elements of $P_A$ to elements of $P_B$. (You need this extra strength because otherwise a term $t$ of type $A \to B$ may evaluate to a function value, which diverges when given an input.) Then you prove a theorem showing that every definable term is in the predicate, and there you go.

This is a very natural technique, and I've often wondered where it shows up in the rest of mathematics. Recently, I learned that category theorists know it too, and call it by various names -- I listed the ones I was able to find in the question. Since (a) categories seem to serve as an interlingua for mathematics, and (b) lots of mathematicians hang out here, I figured I could ask: what other branches of mathematics has this technique been used in, and for what?

familyof predicates/set by recursion over the structure of types -- ie, you give a recursive function $\mathrm{SyntacticType} \to \mathrm{Set}$ (here, sets of terms). Such a definition becomes "logical" when you define this function to ensure that the terms you pick out appropriately respect the desired categorical structure of each type constructor. Categorically, we're "gluing along the hom-functor" of the syntactic category of types and terms. The explicit recursion goes away here, which gives me hope for a broader set of analogies. $\endgroup$ – Neel Krishnaswami May 15 '10 at 19:50