Let CZF denote the constructive Zermel-Fraenkel set theory, a weak set theory which turns into full-blown ZF/ZFC iff Law of Excluded Middle/Axiom of Choice are respectively added. Let CZF(n) denote CZF + REA + Inacc(n), i.e. CZF augmented by Regular Extension Axiom and axioms about existence of `n` universes (`ω` is allowed, meaning Inacc(n) for each positive `n`).
Now let HoTT(n) be the univalent dependent intuitionistic type theory with higher inductive types and `n` universes (`ω` allowed) and HoTT(n++) the same theory augmented by existence of one additional universe U(n + 1) and type V of Un-small Aczel-Gylterud hereditary sets. Note that HoTT(n++) includes HoTT(n + 1) and is included in HoTT(n + 2).
Now, if I understand it correctly, the following holds:
1) For all `n`, CZF(n + 1) models HoTT(n++) which in turn models CZF(n). The whole sequence of theories shares same proof theoretic ordinal as long as `n` is finite. Moreover, CZF(n) proves the same arithmetical statements as HoTT(n + 1) and HoTT(n++).
2) CZF(ω) and HoTT(ω) are bi-interpretable, prove the same arithmetical statements and share the same proof theoretical ordinal (equal or slightly above Bachmann-Howard ordinal, yet way below KPM-ordinal).
3) In HoTT(ω) + LEM/AC the same construction models ZF(C)
Is it true that HoTT(n++) + LEM/AC would model ZF(C) + Inacc(n) and be modelled by ZF(C) + Inacc(n + 1)? If so, can we show conservativity regarding set-theoretic statements?
The results mentioned above can be shown to hold in a roundabout way, but could be straightforwardly if it turns out that Aczel-Gylterud iterated set construction in HoTT satisfies CZF + REA + ΠΣW-AC + RDC + PAx in strong enough sense.
Would adding propositional resizing (i.e. impredicative Prop) and/or inductive-recursive definitions to HoTT ruin something in this idyllic picture?