Reference request: proof-theoretic strength of $\mathsf{KP}$ with recursively large ordinals and $\mathsf{CZF}$ with large set axioms

Question

Large set axioms are notions corresponding to large cardinals on constructive set theories like $\mathsf{IZF}$ or $\mathsf{CZF}$. The notion of inaccessible sets, Mahlo sets, and 2-strong sets correspond to inaccessible, Mahlo, and weakly compact cardinals on $\mathsf{ZFC}$. (See Rathjen's The Higher Infinite in Proof Theory and Ziegler's thesis for the definition of notions I mentioned, and check the description added in the )

It is known that the proof-theoretic strength (or consistency strength if you are not familiar with the proof-theoretic one) of $\mathsf{CZF}$ is the same as that of $\mathsf{KP}$, so we may expect the strength of $\mathsf{CZF}$ with large sets are quite weaker than that of $\mathsf{ZF}$. In fact, Rathjen described the proof-theoretic strength of large sets over $\mathsf{CZF}$ in his paper The Higher Infinite in Proof Theory. Here is the result he stated:

Theorem 6.9. $\mathsf{CZF}+\forall x\exists I (x\in I \land \text{$I$ is inaccessible})$ can be interpretable in $\mathsf{KP}+\forall \alpha\exists \kappa>\alpha(\text{$\kappa$ is recursively inaccessible})$. Moreover, the interpretation preserves the validity of $\Pi^0_2$-sentences.

Theorem 6.14. $\mathsf{CZF}+\forall x\exists M (x\in M \land \text{$M$ is Mahlo})$ can be interpretable in $\mathsf{KP}+\forall \alpha\exists \kappa>\alpha(\text{$\kappa$ is recursively Mahlo})$. Moreover, the interpretation preserves the validity of $\Pi^0_2$-sentences.

Theorem 6.20. $\mathsf{CZF}+\forall x\exists K (x\in M \land \text{$K$ is 2-strong})$ can be interpretable in $\mathsf{KP}+\forall \alpha\exists \kappa>\alpha(\text{$\kappa$ is $\Pi_3$-reflecting})$. Moreover, the interpretation preserves the validity of $\Pi^0_2$-sentences.

However, Rathjen does not state the proof of his results in this paper. Combining some known results may result in a proof of the statement given above, but I have no clear idea which one would be relevant.

Question. Where can I find a proof (or a rough sketch of a proof) of the statements described above?

---

Added on 1 April 2021: I realized that just referring to Ziegler's thesis for the definition of large set axioms is not correct, since the different definitions result in different proof-theoretic strength.

Ziegler defined inaccessible sets as transitive sets which satisfy the second-order Strong Collection and $\mathsf{CZF}$. Some other references (e.g., Rathjen's paper I cited) add an additional requirement that an inaccessible set must satisfy the regular extension axiom $\mathsf{REA}$, which claims that every set is contained in a regular set. Let me call the former weakly inaccessible sets, and the latter strongly inaccessible sets.

It turns out that the existence of weakly inaccessible sets does not strictly increase the proof-theoretic strength:

Theorem. The theory $\mathsf{CZF}$ + "every set is contained in a weakly inaccessible set" has the same proof-theoretic strength with $\mathsf{CZF+REA}$.

(See Theorem 4.7 of Rathjen's The Anti-Foundation Axiom in Constructive Set Theories for its proof.)

However, the proof-theoretic strength of $\mathsf{CZF}$ with a strongly inaccessible set exceeds that of $\mathsf{CZF+REA}$. In fact, it has the same proof-theoretic strength with $\mathsf{KP}$ with a recursively inaccessible ordinal. (Theorem 6.5 of Rathjen's Proof Theory of Constructive Systems: Inductive Types and Univalence.)

Note that both weakly and strongly inaccessible sets are just $V_\kappa$ for an inaccessible cardinal $\kappa$ over $\mathsf{ZFC}$. There may be a difference between them over $\mathsf{ZF}$ since strongly inaccessible sets would think there is a proper class of regular cardinals. I do not think there is any direct relation between these two kinds of sets and weakly inaccessible cardinals.

Rathjen defined his inaccessible sets as strongly inaccessible sets in his papers, so we have to understand inaccessible sets in that sense.

Answer 1

Rathjen stated rough sketch of proof that intuitionistic theory (e.g. $\mathsf{CZF}+(\forall x)(\exists I)[x\in I\land I \text{ is inaccessible}]$) has at least the strength of the classical one (e.g. $\mathsf{KP}\omega+(\forall\alpha)(\exists\kappa)[\alpha<\kappa\land\kappa\text{ is recursively inaccessible}]$) in The Realm of Ordinal Analysis.

The proof that the intuitionistic theory has at least the strength of the classical one requires an ordinal analysis of the classical theories as given in [73, 74, 82] and a proof of the well-foundedness of the pertinent ordinal representation system in the intuitionistic theory.

From this description, Rathjen's proof is probably following.

Let $T_i$ be intuitionistic theory, $T$ be classical theory corresponding to intuitionistic one, and $\langle A,\prec\rangle$ be primitive recursive well-ordering which has proof-theoretic ordinal of $T$.

1. Prove well-foundedness of $\prec\restriction$ in $T_i$ by using higher infinites where $\prec\restriction$ is proper initial seqment of $\prec$.
2. Embed $T$ into infinitary derivation $\mathrm{RS}$ and prove "$T\vdash\varphi$ implies there exists $\alpha\in A$ such that $\mathrm{RS}$-cutfree proof of $\varphi$ whose height bounded by $\alpha$ for all $\Sigma_1^{L_{\omega_1^\mathrm{CK}}}$-sentence $\varphi$" by using cut elimination and collapsings in $T_i$.
3. Prove "If there is $\mathrm{RS}$-cutfree proof of $\varphi$ whose height bounded by $\alpha\in A$, then $\varphi$ is true for all $\Pi^0_2$-sentence" by using transfinite induction up to $\alpha$ and $\Pi^0_2$-partial truth definition in $T_i$.