Why are types in type theory unordered collections?

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?

• "All data is stored and operated on in some order". In this part of the question you refer to an unordered collection of "all data". :) Jul 10, 2017 at 7:58
• As an analogy, sorting algorithms "operate on ordered collections". But the algorithms themselves, which is what the theory is about, are not linearly ordered in any interesting way. Jul 10, 2017 at 13:19
• I guess my sticking point is that, in set theory, if I declare some arbitrary set X = {a,b,c} then those elements are not in the order a then b then c. Yet as humans we have no ability to reason about such a set until I put it on paper in some arbitrary order, whether that's {a,b,c} or {b,c,a}. If you ask me "is the element "a" in set X?" I have to scan over the set in some arbitrary order, that is I need some algorithm that respects the arbitrary ordering to find the element "a" (imagine the set being much bigger so as I really would need an algorithm to find if an element is in X). Jul 10, 2017 at 16:40
• Fair point, I'm thinking more along the lines of Per Martin Löf -like intensional type theories. e.g. homotopy type theory. Jul 10, 2017 at 22:24
• If, in fact, "as humans we have no ability to reason about such a set until I put it on paper in some arbitrary order," then I must not be human. Most of my reasoning about sets involves neither an ordering nor any attempt to write down all the members of the sets. Jul 11, 2017 at 1:59