It's popular for mathematicians to roleplay that they are working in ZFC, a theory of sets whose members are sets. What would modeling mathematics in list theory look like? I'm imagining a theory where the objects are lists whose members are lists. Lists would be like sets, but would allow repeated elements, and the elements would have an order. Infinite lists would of course be allowed. What axioms would be appropriate for list theory? How would doing mathematics in list theory compare to working in set theory?

This is how set theorists like to model the natural numbers:
0 = {}
1 = {0}
2 = {0, 1}
3 = {0, 1, 2}
4 = {0, 1, 2, 3}
...

We could do a similar thing in list theory, or we could do something like
0 = ()
1 = (())
2 = (() ())
3 = (() () ())
4 = (() () () ())
...

An important question is what kind of orders are allowed in lists. For example, could the real numbers in their usual order be a list? If so, it would violate some properties we might expect from lists. Consider the sublist formed by taking all the real numbers greater than 0. This list would have no starting point, so it's questionable whether it's right to call it a list. We say the real numbers in their usual order are not "well-ordered."

Mathematicians often claim that the real numbers can be put in a different order which is well-ordered, although they are not able to exhibit this order (P2314 related).

Inb4 every thread I just larp about acl2 but you should look at what well-founded structure it uses as the premise for recursion and induction.
(The ordinals and hence lexicographically ordered natural n-tuples)