> You can just partition your urelements if you want distinct "types". Union across those would be disjoint, but within would be standard set union.

In which sense would partitioning urelements lead to something like types? This sounds somewhat like many sorted logic, which is only as expressive as first-order logic, not higher-order logic / simple type theory: https://plato.stanford.edu/entries/logic-many-sorted/

> Even in type theory you have Church VS Curry style as to whether you consider terms as inheritly belonging to a type.

Not sure what the difference is here.