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.

The Realm of Ordinal Analysisbriefly mentions how to prove it, and (unfortunately, at least for me that is not familiar with ordinal analysis) the proof uses ordinal analysis. (Add: the reporter said he will post an answer tomorrow (according to GMT+9), so I am waiting for it.*) $\endgroup$ – Hanul Jeon Dec 27 '20 at 17:29