3 ms·

One thing I did not find in thr article is what the improvement here is. If I read it (and some of the comments here) correctly the idea is to replace equality

by rocqua 5y ago

One thing I did not find in thr article is what the improvement here is. If I read it (and some of the comments here) correctly the idea is to replace equality from ZFC (so isomorphic sets) with equality in categories (so isomorphic objects in a k-category). The article says something about better describing all the isomorphisms, but doesn't explain why that is better. A comment here suggested to me that this system might make it easier to rigorously 'compose' different types of equivalence relationships. Something like "this field extension has a galois group 'equivalent' to A. And field extensions of A have this other property so this field extensions must also have this property". Am I on the right track as to what improvements this system offers?

Twisol 5y ago
As a relative layperson alongside you, I'm not sure what precise deficit Lurie is addressing. But having spent some deep time in a proof assistant (Agda) lately, I think there is a related issue. Formally, equality can be "intensional" or "extensional". An intensional theory equality says that things are the same only when they are defined the same way. So, for instance, "the set of even primes" and "the set of primes less than 3" are not intensionally the same. In contrast, an extensional theory says that things are the same when they behave the same. Both sets answer the same membership questions the same way -- 2 is the only element of either -- so they are the same set. ZFC is fundamentally extensional -- one of its axioms is literally called the axiom of extensionality, defining equality in terms of membership. In deeply identifying the above sets, we lose some of the ability to distinguish them formally and model the way in which they are equivalent. That's one guess. Another, less specific guess is that it's much like how the dual of a vector space is isomorphic to the original vector space, but in a way that depends on certain arbitrary choices. Meanwhile, the dual of the dual is naturally isomorphic to the original vector space. Thus, there are qualities of equivalence that we're interested in. (But this example is perfectly well captured by linear algebra as it stands.)
mattalex 5y ago
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.
throwaway81523 5y ago
The article is just not very good. You might like Emily Riehl's article in Scientific American last year: https://www.scientificamerican.com/article/infinity-category-theory-offers-a-birds-eye-view-of-mathematics1/ https://www.scientificamerican.com/article/infinity-category...

by rocqua 5y ago

Twisol 5y ago

As a relative layperson alongside you, I'm not sure what precise deficit Lurie is addressing. But having spent some deep time in a proof assistant (Agda) lately, I think there is a related issue. Formally, equality can be "intensional" or "extensional". An intensional theory equality says that things are the same only when they are defined the same way. So, for instance, "the set of even primes" and "the set of primes less than 3" are not intensionally the same. In contrast, an extensional theory says that things are the same when they behave the same. Both sets answer the same membership questions the same way -- 2 is the only element of either -- so they are the same set. ZFC is fundamentally extensional -- one of its axioms is literally called the axiom of extensionality, defining equality in terms of membership. In deeply identifying the above sets, we lose some of the ability to distinguish them formally and model the way in which they are equivalent. That's one guess. Another, less specific guess is that it's much like how the dual of a vector space is isomorphic to the original vector space, but in a way that depends on certain arbitrary choices. Meanwhile, the dual of the dual is naturally isomorphic to the original vector space. Thus, there are qualities of equivalence that we're interested in. (But this example is perfectly well captured by linear algebra as it stands.)

mattalex 5y ago

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.

throwaway81523 5y ago

The article is just not very good. You might like Emily Riehl's article in Scientific American last year: https://www.scientificamerican.com/article/infinity-category-theory-offers-a-birds-eye-view-of-mathematics1/ https://www.scientificamerican.com/article/infinity-category...