Extensional set equality in the calculus of constructions
The original representation of set theory in the calculus of constructions, has met an objection on the grounds that the axiom of exstensionality is incompatible with the assumptions for arithmetic. In this paper, it is shown that there is really no problem with the axiom of extensionality. Furthermore, Huet's representation has the advantage that results of Seldin's results imply the consistency of the representation. Having such a consistency proof may be important if one needs a trusted theorem prover, since consistency is clearly a necessary condition (although not a sufficient condition) for being trusted, and the paper closes with some remarks on what makes a system trusted.
extensionality calculus of constructions set theory typed lambda-calculus trusted systems