For my mathematical bird-brain, the most straightforward way to capture the situation you describe would be in terms of equivalence relations: Each person in your example defines an equivalence relation and each is "valid" and useful in their own way.
My question would be:
1. What makes this informal? Is it because a relation is in some way mathematically informal, because given general objects we either have to enumerate permutations or we have to describe the relation in some informal way? Or is it something else?
2. Starting with the above understanding of equivalence relations, where does category theory come in, and what does it solve (and add)?
My guess would be that it is operating on a higher order concept than equivalence relations. For instance, seeing that a situation might be described/given by several equivalence relations, we'd probably want to have equivalences between equivalence relations, and then work based on "quotient sets of equivalence relations" and derive theorems based that?
Doing everything in terms of explicit equivalence relations is perfectly rigorous, but it results in a combinatorial explosion of bookkeeping tasks for anything other than set theory, and so no one actually does it. We want foundations that allow us to engage in idiomatic mathematical reasoning and be perfectly rigorous at the same time.
> For instance, seeing that a situation might be described/given by several equivalence relations, we'd probably want to have equivalences between equivalence relations, and then work based on "quotient sets of equivalence relations"
My question would be:
1. What makes this informal? Is it because a relation is in some way mathematically informal, because given general objects we either have to enumerate permutations or we have to describe the relation in some informal way? Or is it something else?
2. Starting with the above understanding of equivalence relations, where does category theory come in, and what does it solve (and add)?
My guess would be that it is operating on a higher order concept than equivalence relations. For instance, seeing that a situation might be described/given by several equivalence relations, we'd probably want to have equivalences between equivalence relations, and then work based on "quotient sets of equivalence relations" and derive theorems based that?
Fascinating stuff, though.