Indeed, and e:t in type theory is quite a strong ontological commitment, it implies that the mathematical universe is necessarily subdivided into static types. My abstraction logic [1] has no such commitments, it doesn't even presuppose any abstractions. Pretty much the only requirement is that there are at least two distinct mathematical objects.

[1] http://abstractionlogic.com