That means, when we ask "If ZFC + {n inaccessibles | n natural} and CIC + LEM + (some choice) prove the same statements," we should formulate it as sth like

If F is an interpretation from type-theoretic language to set theory, then whether "type theory proves P" iff "set theory proves F(P)."

Team Cherry demands the hardcore user to really be a hardworking hardcore user. Alas, we are already too busy to be a hardcore user in math.

Doing every achievement sounds really tough...

Just for curiosity, to a month-old post: Did you finally free Phaloom?

OTOH, Dorais' equiconsistency proof between ACA0+ and Provident set theory seems to give a bi-interpretation between these two theories in a way to preserve β-models. (A β-model of ACA0+ should be an ω-model of ACA0+ that is correct about recursible well-orders.)

I believe type theory also has some cumulative nature when we start to talk about large-cardinal-like axioms (like the level of universes). Set theory has better control on the hierarchy, so replacing set theory with type theory as a consistency-strength calibrator may be hard.

I believe it is somehow relevant to understanding the iterated Bachmann-Howard collapsing of a dilator.

You should protect your time from Silksong first (by a person who lost 40+ hours to it).

I think, we should apply the same POV to zero sharp. Adding zero sharp means, we add bunch of ordinals from the least height model of ZFC so that at some height of L-hierarchy, we have an L-ultrafilter, giving an iterable mouse.

We can enhance this theory by adding the axiom "There are two cardinals." The most natural model-theoretic POV for adding the axiom is end-extending from H(ω₁) to H(ω₂).

We do not think something like, "Add the axiom, then the (fixed) largest cardinal now has an additional cardinal below."