Dear Hugh,

In ZF if there is an extendible cardinal (or just proper class of supercompact cardinals formulated properly in ZF) then there is a class forcing extension in which AC holds and one preserves all supercompact cardinals (and much more).

Thanks for pointing this out. It suggests that for the choiceless-HP, AC might be compatible with maximality if the existence of supercompacts is (still unclear), and also that any “good set theory” compatible with supercompacts has a chance of being at least “simulated” in models of useful axioms compatible with AC.

Of course I’d prefer just to always assume choice but do want to stay open-minded about that as we don’t know what the set theory of the 22nd century might look like.

Best,

Sy