I forgot to write a post about this a year ago, but I gave a talk at AustMS2020 detailing some work that Martti Karvonen and I did, originating in a discussion on the category theory Zulip chat server. The main gist of the project is removing the need for Global Choice from a pair of theorems in pure category theory dealing with concrete and non-concrete categories. The most famous example (shown by Freyd) of a non-concrete locally small category is the homotopy category of , which is the category whose objects are topological spaces, but whose morphisms are homotopy classes of continuous maps. It is a quotient of the concrete category of topological spaces, by a congruence on its hom-sets. The first theorem that we improved, due to Kučera, is that this is as bad as it gets: every locally small category is the quotient of a concrete category by a congruence like this. The proof constructs a concrete category, but it’s not very nice or workable, so it’s really just an existence result.

Unfortunately the original proof starts by well-ordering the universe of sets, which really makes me itch: category theory is generally rather constructive in nature, or at least can be reformulated to have some kind of constructive content. A purely category-theoretic statement that needs the axiom of Global Choice seems non-optimal to me. And, thankfully, this is the case. Martti came up with a way to remove Choice (even normal AC) from the construction, and then I figured out how to do the whole thing in Algebraic Set Theory with the assumption of Excluded Middle (i.e. the category with class structure is *Boolean*).

Then we turned out attention to a theorem of Freyd that gives a precise characterisation of which categories are concretizable, albeit we started from Vinárek’s cleaner and shorter proof. It shows that a necessary condition for concreteness, due to Isbell, is also sufficient. Isbell gave examples of non-concretizable categories, but they were artificial, specifically constructed to violate his condition. Like Kučera’s theorem, even Vinárek’s improved proof used Global Choice to pick a well-ordering of the universe. We were able to re-do the theorem in ZF, and more generally in (Boolean) algebraic set theory, with the additional assumption that the universal object has a well-ordered stratification by small objects (roughly, it has a small map to the object of ordinals). This last assumption is validated in any membership-based set theory where some cumulative hierarchy exhausts the class of all sets, say the von Neumann hierarchy for ZF, or some weaker set theories where a hierarchy, or a rank function, is posited axiomatically (see eg this paper).

The paper is in preparation, and would have been done by now, had I not been distracted by other projects. Martti is being very patient with me! For now, let me point to the slides for my talk, which you can see here.