$\mathbb P^*$ is non-separative. What about for separative $\mathbb P$?

What did Chatty say in response? Has his training made him believe in Woodin cardinals?

There’s a rumor that some top set theorists have actually found inconsistencies, but the arguments are so intricate that they can be mined for proofs of other results enough to make a long successful academic career.

@NoahSchweber There’s still time 😂

If it can be done succinctly, could you explain why the countable approximation property holds for the product of length 2?

This is basically a restricted version of Mitchell forcing, right? It's only $\omega$-many terms and the $Add(\omega_1)$ posets are in the forcing language of the adjacent $Add(\omega)$ poset, instead of the product of all of them up to that point, as in Mitchell.

Note that MM implies SCH, which implies that $\square_{\kappa^+,\kappa^+}$ holds whenever $\kappa$ is a singular strong limit.

Can you construct (a version of) the natural numbers in this theory?

@AlecRhea Yes, I think so.

@AlecRhea I read this as a stand-alone axiom scheme.

You are probably aware of this, not sure if it’s relevant: cambridge.org/core/journals/review-of-symbolic-logic/article‌​/…

Putting the "picture of the universe" aside, my main point is that set theory has developed a slew of sophisticated transfinite induction arguments for various applications. They are not always about "$\in$-rank" directly but often build some other kind of hierarchy for the purpose at hand. Maybe these ideas could be useful when category theory gets itself into such pickles as described in the OP, or elsewhere. Anyway, as you know, in the context of Choice, the Foundation axiom is merely a simplifying assumption and doesn't add or subtract any structural information.

Pardon my ignorance. But the deeper reason behind my comment is that keeping track of cardinality is less fine than keeping track of "when things are born", which can be useful in more complicated recursive constructions where a seemingly circular definition is made to make sense because of some hierarchical birthday structure, and cardinality doesn't provide enough structure to work with.

Perhaps it is useful to go a step further like we do in set theory, and make a hierarchy of distinctions of sizes. Rather than merely distinguishing small vs. large categories, one might speak of “categories of rank $<\alpha$” for ordinals $\alpha$.

What is the key mathematical innovation in your work?

Oops, I read poorly.

@FarmerS Hmm. If $\varphi$ is such that $\varphi[\neg X] = X$, then $\varphi[\neg X] \notin \mathcal P(\omega)\setminus \{X\}$.