Isbell gave, in *Two set-theoretic theorems in categories* (1964), a necessary criterion for categories to be concretisable (i.e. to admit some faithful functor into sets). Freyd, in *Concreteness* (1973), showed that Isbell’s criterion is also sufficient.

My question is: **Has anyone ever used Isbell’s criterion to check that a category is concretisable?**

I’m interested not only in seeing the theorem is formally invoked in print, to show some category is concretisable — though of course that would be a perfect answer, if it’s happened. What I’m also interested in, and suspect is more likely to have occurred, is if anyone’s found the criterion useful as a heuristic for checking whether a category is concretisable, in a situation where one wants it to be concrete but finding a suitable functor is not totally trivial. (I’m imagining a situation similar to the adjoint functor theorems: they give very useful quick heuristics for guessing whether adjoints exist, but if they suggest an adjoint does exist, usually there’s an explicit construction as well, so they’re used as heuristics much more often than they’re formally invoked in print.)

What I’m not so interested in is uses of the criterion to confirm that an expected non-concretisable category is indeed non-concretisable — I’m after cases where it’s used in expectation of a *positive* answer.

rarelyformally invoked, but apart from the special cases for LFP’s you mention, I don’t think I’ve ever had cause to do so (and I feel like I don’t see it done terribly often either), whereas I use the associated heuristics all the time (and so I imagine other authors doing similarly behind the scenes). $\endgroup$