  Myhill’s exponentiation axiom is now part of all major systems of constructive set theory. In the case of CZF, in fact, one has a strengthening of exponentiation, known as subset collection, which is also a weakening of power set. A generalisation of exponentiation can also be found in constructive type theory.