4 ms·

The problem is that you have model everything in a lossy way to make that work. If you want to say that 2 green apples plus 2 red apples equals 4 apples, you ha

by lmm 1y ago

The problem is that you have model everything in a lossy way to make that work. If you want to say that 2 green apples plus 2 red apples equals 4 apples, you have to just say that you have 2 apples plus 2 apples, and you can't then go back and ask what colour your apples are. Whereas in homotopy type theory you can say a red apple is equivalent to a green apple, and that equivalence is a mathematical object you can manipulate in nice ways, but if you ever need to go back and work with the colour again it's still there.

auggierose 1y ago
> 2 green apples plus 2 red apples equals 4 apples What a load of malarkey. This statement is not a problem for traditional mathematics. I have 2 green apples and 2 red apples right here in my bag (eh, set), and the size of the set is 4, and all elements of the set are apples, some of them are red, some are green. What is the problem? I can tell you: type theory.
- lmm 1y ago
  > I have 2 green apples and 2 red apples right here in my bag (eh, set), and the size of the set is 4, and all elements of the set are apples, some of them are red, some are green. Well, is your set equal to a set of 3 green apples and 1 red apple, or not? (And actually how can you have multiple green apples in the same set if they're equal?)
  - auggierose 1y ago
    Just because two apples are both green doesn't mean that they are equal. In fact, if there are two apples, that means they are definitely not equal, otherwise there would be just one green apple. No, the set is not equal to a set of 3 green apples and 1 red apple, under the assumption that a green apple cannot be a red apple (and vice versa). Any more questions?
    - lmm 1y ago
      > Just because two apples are both green doesn't mean that they are equal. In fact, if there are two apples, that means they are definitely not equal, otherwise there would be just one green apple. Well, a green apple had better be equal to itself. So if you've got a green apple and another green apple that isn't equal to the first, you're already in trouble and going to have to resort to hacks like numbering them. > No, the set is not equal to a set of 3 green apples and 1 red apple, under the assumption that a green apple cannot be a red apple (and vice versa). What if you want to manipulate it in a context where you only care about the number of apples, not their colour?
      - auggierose 1y ago
        > Well, a green apple had better be equal to itself. So if you've got a green apple and another green apple that isn't equal to the first, you're already in trouble and going to have to resort to hacks like numbering them. Nope, no trouble at all. Those troubles only exist in your type-infested mind. > What if you want to manipulate it in a context where you only care about the number of apples, not their colour? Then I'll do just that. Lol, you can't make this shit up.
paulddraper 1y ago
This “apple” thing…is it colored or not? You can’t start with one definition and then throw in another. Does two equal two? What if the first one is written in a larger font?
- lmm 1y ago
  > Does two equal two? What if the first one is written in a larger font? Exactly. Obviously they're different, but they're equivalent for most purposes. In traditional mathematics you have to handle this in a very awkward way: you have to say there's some kind of platonic ideal of two, and then writing two in one font or another forms a model of this platonic ideal of two. Then you can work with the platonic ideal of two, and add two and two and get four - but you've already forgotten which font you're in. Whereas if you say that twos in one font are equivalent to twos in another font or to some canonical platonic ideal of two, you can lift the fact that two plus two is equal to four back along those equivalences and get a four in the right font. (Or, more commonly, you just ignore that detail and say that you've got something equivalent to four - but you haven't erased the details, they're always there if you need them).
  - auggierose 1y ago
    > Obviously they're different, but they're equivalent for most purposes That is not even wrong. You are mixing up syntax and semantics, and that is because type theorists don't have a concept of semantics.
    - lmm 1y ago
      > That is not even wrong. You are mixing up syntax and semantics, and that is because type theorists don't have a concept of semantics. Right back at you. I don't have to treat notation as something different from semantics, because I'm working in a theory that can handle both elegantly and consistently. Conventional mathematics struggles to describe mathematics as it is actually performed - working mathematicians rely extensively on "abuse of notation", but set-theoretic metamathematics pretends this is out of scope or safe to ignore.

by lmm 1y ago

auggierose 1y ago

> 2 green apples plus 2 red apples equals 4 apples What a load of malarkey. This statement is not a problem for traditional mathematics. I have 2 green apples and 2 red apples right here in my bag (eh, set), and the size of the set is 4, and all elements of the set are apples, some of them are red, some are green. What is the problem? I can tell you: type theory.

lmm 1y ago
> I have 2 green apples and 2 red apples right here in my bag (eh, set), and the size of the set is 4, and all elements of the set are apples, some of them are red, some are green. Well, is your set equal to a set of 3 green apples and 1 red apple, or not? (And actually how can you have multiple green apples in the same set if they're equal?)
- auggierose 1y ago
  Just because two apples are both green doesn't mean that they are equal. In fact, if there are two apples, that means they are definitely not equal, otherwise there would be just one green apple. No, the set is not equal to a set of 3 green apples and 1 red apple, under the assumption that a green apple cannot be a red apple (and vice versa). Any more questions?
  - lmm 1y ago
    > Just because two apples are both green doesn't mean that they are equal. In fact, if there are two apples, that means they are definitely not equal, otherwise there would be just one green apple. Well, a green apple had better be equal to itself. So if you've got a green apple and another green apple that isn't equal to the first, you're already in trouble and going to have to resort to hacks like numbering them. > No, the set is not equal to a set of 3 green apples and 1 red apple, under the assumption that a green apple cannot be a red apple (and vice versa). What if you want to manipulate it in a context where you only care about the number of apples, not their colour?
    - auggierose 1y ago
      > Well, a green apple had better be equal to itself. So if you've got a green apple and another green apple that isn't equal to the first, you're already in trouble and going to have to resort to hacks like numbering them. Nope, no trouble at all. Those troubles only exist in your type-infested mind. > What if you want to manipulate it in a context where you only care about the number of apples, not their colour? Then I'll do just that. Lol, you can't make this shit up.

paulddraper 1y ago

This “apple” thing…is it colored or not? You can’t start with one definition and then throw in another. Does two equal two? What if the first one is written in a larger font?

lmm 1y ago
> Does two equal two? What if the first one is written in a larger font? Exactly. Obviously they're different, but they're equivalent for most purposes. In traditional mathematics you have to handle this in a very awkward way: you have to say there's some kind of platonic ideal of two, and then writing two in one font or another forms a model of this platonic ideal of two. Then you can work with the platonic ideal of two, and add two and two and get four - but you've already forgotten which font you're in. Whereas if you say that twos in one font are equivalent to twos in another font or to some canonical platonic ideal of two, you can lift the fact that two plus two is equal to four back along those equivalences and get a four in the right font. (Or, more commonly, you just ignore that detail and say that you've got something equivalent to four - but you haven't erased the details, they're always there if you need them).
- auggierose 1y ago
  > Obviously they're different, but they're equivalent for most purposes That is not even wrong. You are mixing up syntax and semantics, and that is because type theorists don't have a concept of semantics.
  - lmm 1y ago
    > That is not even wrong. You are mixing up syntax and semantics, and that is because type theorists don't have a concept of semantics. Right back at you. I don't have to treat notation as something different from semantics, because I'm working in a theory that can handle both elegantly and consistently. Conventional mathematics struggles to describe mathematics as it is actually performed - working mathematicians rely extensively on "abuse of notation", but set-theoretic metamathematics pretends this is out of scope or safe to ignore.