Very large set axioms over constructive set theories

We investigate large set axioms defined in terms of elementary embeddings over constructive set theories, focusing on $\mathsf{I}\mathsf{K}\mathsf{P}$ and $\mathsf{C}\mathsf{Z}\mathsf{F}$. Most previously studied large set axioms, notably the constructive analogues of large cardinals below $0^{\mathrm{♯}}$, have proof-theoretic strength weaker than full Second-order Arithmetic. On the other hand, the situation is dramatically different for those defined via elementary embeddings. We show that by adding to $\mathsf{I}\mathsf{K}\mathsf{P}$ the basic properties of an elementary embedding $j\colon V\to M$for$\Delta_0$-formulas,whichwewilldenoteby$${\mathsf{\Delta }}_{\mathsf{0}}\text{-}\mathsf{B}\mathsf{T}\mathsf{E}\mathsf{E}$_M$,weobtaintheconsistencyof$$\mathsf{Z}\mathsf{F}\mathsf{C}$$ and more. We will also see that the consistency strength of a Reinhardt set exceeds that of $\mathsf{Z}\mathsf{F}+\mathsf{W}\mathsf{A}$. Furthermore, we will define super Reinhardt sets and $\mathsf{T}\mathsf{R}$, which is a constructive analogue of $V$ being totally Reinhardt, and prove that their proof-theoretic strength exceeds that of $\mathsf{Z}\mathsf{F}$ with choiceless large cardinals.