I have one more comment on choiceless large cardinal axioms that concerns .
It is worth pointing out that Hugh’s consistency proof of shows a good deal more (as pointed out by Hugh):
Theorem: Assume that every real has a sharp. Then, in the hyperuniverse there exists a real x_0 such that every #-generated M to which belongs, satisfies and in the following very strong sense:
(*) Every sentence which holds in a definable inner model of some #-generated model N, holds in a definable inner model of M.
There is no requirement here that N be an outer model of M. In this sense, is not really about outer models. It is much more general.
It follows that not only is consistent with all (choice) large cardinal axioms (assuming, of course, that they are consistent) but also that is consistent with all choiceless large cardinal axioms (assuming, of course, that they are consistent).
The point is that is powerless to provide us with insight into where inconsistency sets in.
Before you protest let me clarify: I know that you have not claimed otherwise! You take the evidence for consistency of large cardinal axioms to be entirely extrinsic.
My point is simply to observe to everyone that makes no predictions on this matter. And, more generally, I doubt that you think that the hyperuniverse program has the resources to make predictions on this question since you take evidence for consistency of large cardinal axioms to be extrinsic.
In contrast “V = Ultimate L” does make predictions on this question, in the following precise sense:
Theorem (Woodin). Assume the Ultimate L Conjecture. Then if there is an extendible cardinal then there are no Reinhardt cardinals.
Theorem (Woodin). Assume the Ultimate L Conjecture. Then there are no Super Reinhardt cardinals and there are no Berkeley cardinals.
Theorem (Woodin). Assume the Ultimate L Conjecture. Then if there is an extendible cardinal then there are no Reinhardt cardinals (or Super Reinhardt cardinals or Berkeley Cardinals, etc.)
(Here the Ultimate L Conjecture is a conjectured theorem of ZFC.)