3 ms·

In standard mathmatics you cannot identify isomorphic objects without the use of an informal argument or abuse of notation: The issue is that the two equivalent

In standard mathmatics you cannot identify isomorphic objects without the use of an informal argument or abuse of notation: The issue is that the two equivalent objects aren't actually identical, they just behave the same in some way. This becomes necessary if you look at more complex objects than the ones equality was originally designed to tackle: a permutationsort and a quicksort are not the same, therefore you can't (at least in the original sense of equality) write permutationsort=quicksort. Of course you can invoke the notion of Leibniz equality and say that ∀x. permutationsort(x) = quicksort(x), therefore they are the same. However, you can't generally replace every occurrence of "quicksort" in your program with "permutationsort" because most likely your program is not going to finish before the heat-death of the universe. So for your program, you need to be able to express the notion of "they two algorithms have to be the same wrt. their (input,output) pairs and asymptotic runtime". However, if you ask your friend, the pure mathematician, you will notice he is quite fine with either one of them, because for the soundness of his new algorithm he just needs _some_ sorting algorithm: In fact, he wants that every sorting algorithm works, not just the specific one he chose to prove his algorithm with. The third person you go to is your old computational-complexity theory professor: From his point of view, permutationsort and quicksort aren't the same at all, but quicksort and matrix-multiplicationa are: after all, they are both P-TIME algorithms. Meanwhile your, at this point very confused, mathematics student comes up to you and asks "if we take a vector space with basis {(1,0),(0,1)} and transform it into a new vectorspace {(1,2),(0,1)}, are they still the same?" and simultaneously two mathmaticians stand up, one saying "yes of course, both describe the ℝ²" and the second will say "no they are not: clearly one is an orthogonal basis, while the other isn't". Depending on the proof you want to do, both can be right. Importantly here is that all of these aren't only considered "equivalent" they are considered "equal", just like you would consider the same algorithm written in Java and C++ as the same, even though they clearly aren't. Therefore, what you want to do is extend the notion of equality such that these notions of equivalence are covered by it. For that, you need a more fine-grained notion of equality, which leads to the equality to be "indexed" by its proof (after all, you need to know which "equality" you were talking about). This will very quickly lead you to the notion of "paths as equalities" and the univalence axiom. So you get rid of the uniqueness of identity axiom, and instead build different notions of equality on different "levels" to have all these notions of equality (and many more) in your system natively.

zwaps 5y ago
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? Fascinating stuff, though.
- hither_shores 5y ago
  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" That's the general idea, yeah.

zwaps 5y ago

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? Fascinating stuff, though.

hither_shores 5y ago
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" That's the general idea, yeah.