@zwarich@hachyderm.io As for separation and power sets, some of the other contributors are interested in CZF and we even have proved some results using it, but I have not dug into those proofs too much.