[FOM] Extensionality and Church-Oswald constructions

[Roger Bishop Jones]

I am at present engaged in the construction of  a model for a set 
theory with a universal set (not NF or NFU).

The method I am using is similar in some respects to the method 
described in Chapter 4 of Forster's book on set theory with a 
universal set, and called there "Church-Oswald constructions".
This involves taking a model of a well-founded set theory and 
extending it to achieve closure under additional operations 
which yield non-well-founded sets.

In the examples shown by Forster care is taken to use 
constructions which yield extensional results.
I however, had in mind using a construction which will not give 
an extensional relationship and then obtaining from this an 
extensional relation over equivalence classes of elements from 
the domain of the constructed model using the smallest 
equivalence relation which will give an extensional result.

I am loth to make the construction considerably more complex for 
the sake of extensionality (which I think it would have to be in 
my case) if I can easily fix the problem later.

Does anyone know reasons why getting extensionality in the 
initial construction might be necessary or desirable? 
(presumably problems with the obvious method of subsequently 
trading up to an extensional relationship).

Roger Jones