The Axiom of Multiple Choice and Models for Constructive Set Theory

Benno van den Berg, Ieke Moerdijk

We propose an extension of Aczel's constructive set theory CZF by an axiom for inductive types and a choice principle, and show that this extension has the following properties: it…