A *concretization* of a category is a faithful functor to the category of sets. A category is *concretizable* if there exists such a functor.

An evident necessary condition for concretizability is local smallness. Of course, for many local smallness is part of the definition of category. In the 1960s, Isbell exhibited a further necessary condition and conjectured its sufficiency.

The following theorems were established in the early 1970s:

1) (Freyd) Isbell's necessary condition for concretizability is sufficient.

2) (Kučera) Every category is a quotient of a concretizable category by a congruence.

Precise definitions, statements, and proofs may be found in Chapter 6 of "Theory of Mathematical Structures" by Adámek. These results are formulated in the language of class-set theory and proved in GB+Global Choice. The arguments rely on having an appropriate well-ordering of the class of all sets.

Another result from the same period is:

3) (Freyd) The Homotopy Category is not concretizable.

By definition, this category is a quotient of a concretizable category. Here the evident weakening to a schema (asserting that no formula yields a concretization) is formalizable in the language of set theory, and the argument appears to carry over as well.

Are the evident weakenings of assertions 1) and 2) to schemata (for definable categories, concretizations and congruences) provable in ZFC?