Hi, correct me if I'm wrong but I think what's going on here is two theories are Morita equivalent (see TST, pg. 59), at least when restricted to models in Grothendieck topoi.

If and are, respectively, the finite-limit theory and its higher-order counterpart and indeed the models in every topos are equivalent, then we have a chain of equivalences , where and are the classifying topoi.  Taking corresponding to , and similarly , we get two functors witnessing an equivalence .

I know almost nothing about categorical model theory but isn't trading a function for a a form of 'de-Skolemization'? Skolemization is the inverse process, if I recall correctly, where an existential axiom is traded for an explicit witness.

I don't know where to go from here but since Skolemization is a pretty famous construction, it could be a good keyword for your searches.

It also points out a potential breaking point of the naive reasoning whereby every can be turned into a function, since this smells a lot like AC and some topoi do not have it.

@jwrigley I'm not assuming that the categories of models are equivalent, but am asking if that is the case. Or if anything similar can be shown/is known.

@matteocapucci good point. But I'm not just de-Skolemizing, but asking for unique existence. I guess there might be a setting where even a functional, total relation might not come from an actual arrow, but this smells like predicative mathematics, and probably not an issue in a topos.

Consider for instance the definition of a group: one could write it in terms of quantifiers and so on, rather than as an equational theory. The multiplication operation should not just be a vanilla . The identity and inverse are of course not specified uniquely, but they can be proved to be unique, so that's not a problem.

The classifying topos for a given theory in a "sub-geometric" fragment of logic is a category of sheaves on the corresponding syntactic category for the theory in that fragment. For a regular theory, for example, we construct the syntactic (regular) category as a category of regular formulas-in-context. But we get an equivalent classifying topos for the theory whether we take the regular, coherent, or geometric (pretopos) syntactic categories. This is a consequence of the fact that geometric morphisms necessarily preserve all of the constructions which interpret geometric logic.

However, this is not the case for higher order logic: there are geometric morphisms whose inverse image functors do not preserve power objects or exponentials, or which do not commute with universal quantification. It may sometimes be possible to construct a topos which classifies a higher order theory in the sense that models of in a topos correspond to those geometric morphisms which do preserve the relevant structure, but at that point it is clear that this will typically be different from the classifying topos for the simpler theory.

As for whether the categories of models will be equivalent, that depends exclusively on whether the simpler theory is constructively/intuitionistically equivalent to the higher-order one.