Please excuse my naïveté, I have no higher math education, just a curious observer. In type theories, types are treated as set-like because they're unordered collections. Yet, the putative motive in modern (constructivist) type theories is to get mathematics closer to computation, but in a computer, there can never exist an unordered collection. All data is stored and operated on in some order, sequentially. We may have a function that does not care about the order of the data it operates on, but the data then still has some arbitrary ordering. So why are all foundational math theories based on unordered collections rather than ordered?
"the putative motive in type theories is to get mathematics closer to computation": there is certainly not a single motive for type theories: first type theories were developped long before computers.
Foundational math theories also usually try to avoid as much as possible unnecessary assumptions. So if a theory does not need order on its objects, it is usually better not to add such a useless order.