Is the existence of double complement of a set provable in Intuitionistic ZF? In Powell's article [1] he introduces the axiom of double complement, which says a double complement $\{x : \lnot\lnot(x\in A)\}$ is a set for any set $A$. 
I can't find similar axiom from other references, even in the Friedman's article [2] on double negation interpretation over set theories. Hence it is natural to ask the relation between his axiom and other axioms of IZF.
(Note: Powell consider the axiom of collection rather than the replacement in his article, but I will consider full IZF.)
I have made some attempts on this problem: if $f(\beta):=\sup\{\alpha\in\mathrm{On} : \lnot\lnot(\alpha<\beta)\}$ exists for each ordinal $\beta$, then the axiom of double complement holds: then $\{x\in V_{f(\operatorname{rank}(A))} : \lnot\lnot(x\in A)\}$ would be the double complement of $A$. (Here $V_\alpha := \bigcup_{\beta\in\alpha} \mathcal{P}(V_\beta)$ is a von Neumann hierarchy. Axiom of power set is necessary in my argument.) However checking $f(\beta)$ is a set is at least as hard as checking the axiom of double complement.
Forcing or realizability seems not helpful to me. This is because we need to generate a set whose double complement is proper class to prove the independence of the axiom of double complement, and it seems to need a proper-class sized name. However both methods just deal with set-sized names.
My question is: Is the axiom of double complement provable from full IZF? If not, is it indenpendent from IZF? Is the axiom of double complement related to the law of excluded middle? I would appreciate any help.
(Added in Jan 04, 2019: Realizability can be used to prove some non-classical principles are compatible with the axiom of double complement. In fact, if $V$ is a model of ZFC and $\mathcal{A}$ is a pca then the realizability model $V(\mathcal{A})$ validates the axiom of double complement.) 
(Added in Jan 06, 2019) I recheck details of the proof of the above statement and I found my proof does not work. Beeson states we can prove the consistency of IZF + Double complement + Church's thesis via realizability in his book Foundations of Constructive Mathematics without proof. I do not know it really holds.

References
[1] Powell, William C. "Extending Gödel's negative interpretation to ZF." The Journal of Symbolic Logic 40.2 (1975): 221-229.
[2] Friedman, Harvey. "The consistency of classical set theory relative to a set theory with intuitionistic logic 1." The Journal of Symbolic Logic 38.2 (1973): 315-319.
 A: A good question.  Bear in mind that there can be no set x whose double complement is the universe. (Think about $\{y\in x: y \not\in y\}$).   If you are thinking in terms of a cumulative hierarchy picture of constructive sets then what this is trying to tell you is that, for any x, there comes a stage by which all things notnotin x have appeared.  And of course, once you have reached such a stage you obtain doublecomp x by separation.  But [the rank of] this stage might increase so steeply with the rank of x that no effective proof can be given that there is such a stage.   If you pursue this line of thought you will probably be able to come up with a kripke model in which lots of sets lack double complements.  I'll have a think about it and get back.
A: This is not a full answer, but I think it is worth to mention: we can prove the theory CZF + Full separation + ￢Double complement is consistent!
The proof goes as follows: consider the Lubarsky's first model in 1. Let $\check{0}(\kappa)=\varnothing$ and $\check{1}(\kappa) = \{\check{0}\upharpoonright (\mathrm{On}\setminus\kappa)\}$. They will behave as 0 and 1 of the model. Furthermore, for each ordinal $\kappa$ define
$$\check{1}_\kappa (\lambda ) = \begin{cases}\varnothing & \text{if }\kappa<\lambda\text{ and} \\ \{\check{0}\upharpoonright (\mathrm{On}\setminus\lambda)\} & \text{otherwise.}\end{cases}$$
I will claim that the element $x\in M_0$, defined by $x(\nu)=\{\check{1}\upharpoonright (\mathrm{On}\setminus\nu)\}$ for every ordinal $\nu$, has no double complement. First, it is tedious to check
$$\kappa \vDash \lnot\lnot (\check{1}_\nu \in x) \iff \forall \lambda \ge \kappa \exists \mu\ge\lambda : \mu\models \check{1}_\nu \in x$$
and the later statement holds: take any $\mu>\max(\lambda, \nu)$. Hence if $y\in M_0$ is a double complement of $x$, then it must contain every $\check{1}_\nu$, which is impossible. (In fact, we need to prove any $y\in M_\xi$ for any $\xi$ cannot be a double complement of $x$. However, its proof is not too different from my proof.)
However, my proof (if correct) has some unsatisfactory points. First, it requires the consistency of ZFC. Lubarsky proved that CZF + Full separation is equiconsistent with the second-order arithmetic [2]. I wonder CZF + Full separation + ￢Double complement is equiconsistent with Second order arithmetic. Kripke models seems not adequate to derive such kind of equiconsistency result (unless we form a Kripke model of CZF over CZF.)
Second, it does not settle my original question: what happenes if we assume the axiom of power set?

(Added in Jan 24, 2019) I found that V. H. Hahanyan makes a bunch of result on the axiom of double complement over IZF (example). But most of his article is written in Russian so it is not easily accessible to me.

References
(1) Lubarsky, Robert S. "Independence results around constructive ZF." Annals of Pure and Applied Logic 132.2-3 (2005): 209-225.
(2) Lubarsky, Robert S. "CZF and Second Order Arithmetic
." Annals of Pure and Applied Logic 141.1-2 (2006): 29-34.
