We propose a model of constructive set theory in Homotopy Type Theory (HoTT), and investigate to which extent it is a model of Constructive Zermelo Fraenkel set theory (CZF).

In contrast with the cumulative hierarchy in the book, “Homotopy Type Theory”, the underlying type and membership relation of our model are definable in plain Martin-Löf type theory. The Univalence Axiom, as well as higher inductive types, in the form of mere set quotients, occur in proving the axioms of constructive set theory.

The idea behind the model can shortly be summarised as follows. The underlying type of Aczel’s setoid model of CZF in Martinl-Löf type theory can be seen from a HoTT perspective as a type of iterative multisets. Multisets differ from sets in that each element has a multiplicity. The HoTT book takes the approach of identifying multiset which only differ by their positive multiplicities when constructing the culmutative hierarchy. We take the alternative approach of using the subtype of multisets with merely propositional multiplicites.