Abstract

IZF is an intuitionistic version of Zermelo-Fraenkel set theory (ZFC). We present a practical approach to doing extraction in IZF, based on formulas-as-types principle.