Note that an iterative set is a data-structure in the sense of functional programming: a possibly infinitely branching well-founded tree. Different trees may represent the same set. We therefore need to define a notion of extensional equality between iterative sets which disregards repetition and order of elements. This definition is formally similar to the definition of bisimulation of processes in process algebra. The type \(\V\) up to extensional equality can be viewed as a constructive type-theoretic model of the cumulative hierarchy, see the entry on    set theory: constructive and intuitionistic ZF for further information about CZF.