Just a guess....

[Zuhair]

Language: FOL

Primitives. membership, identical, ordered pair

Axioms: Identity theory + characteristic property of ordered pairs +

Sets with the same members are identical

An element of a set is singleton

A singleton is its element

If phi is stratified then a set of all singletons satisfying phi
exists.

An ordered pair is singleton

/

stratification follows Quine for = and e symbols, in addition an
ordered pair and its projection will be assigned the same type.

This theory is purely extensional as regards sets in it, but it can
interpret NFU+Infinity in the following manner:

x is an NFU set iff Exist p. x=(p,p)

x is an NFU element of y <> Exist p. y=(p,p) & x e p

It is trivial to prove that all axioms of NFU + Infinity follows.

So this is a purely extensional NFU + Infinity.

I have the vague sense of what qualifies a predicate to be type
leveling (like identity and projection) or type elevating (like
membership).

If a predicate P(x,x1,..,xn) is axiomatized such that

P(x,x1..,xn) & P(x,y1,..,yn) > x1=y1 &...& xn=yn & Exist y. x R y

where there can exist more than one object having the relation R to
the same y.

Then P is a type leveling predicate.

If P(x,x1,...,xn) doesn't satisfy the above property but satisfy Exist
y. x R y then it is type elevating predicate, i.e. x is higher in type
than every xi (i=1,..,n).

just a guess.

Zuhair