Constructive Sets in Computable Sets

The original interpretation of the constructive set theory CZF in Martin-Lof's type theory uses the 'extensional identity types'. It is generally believed that these 'types' do not belong to type theory. In this paper it will be shown that the interpretation goes through without identity types. This paper will also show that the interpretation can be given in an intensional type theory. This reflects the computational nature of the interpretation. This computational aspect is reinforced by an w-Set model of…