As to the prominent question of whether CZF itself has the existence property, this has been solved in the negative by Swan (2014). There the author made use of three well devised realisability models and embeddings between them, to show that even the weak existence property fails for CZF. In so doing he also showed that CZF’s subset collection schema is the culprit. As clearly highlighted in (Swan 2014) the fact that CZF does not have EP does not indicate some weakness in CZF as a constructive theory. Even if Swan proved essentially that CZF asserts the existence of mathematical objects that it does not know how to construct, still CZF does have natural interpretations in which these objects can be constructed, like, for example, Aczel’s interpretation into type theory (Aczel 1978).