4 ms·

To be clear, constructive mathematics is not new to me. I just don't see the point of it. That mathematics can be done in a machine-checkable way was known lon

To be clear, constructive mathematics is not new to me. I just don't see the point of it. That mathematics can be done in a machine-checkable way was known long before HoTT. Nothing new there. For example, I've had no (particular) difficulty mechanising surreal numbers without using HoTT for this. Also real numbers can be done easily without HoTT. So again: Why should I care about the univalence axiom? If you cannot answer that, I am not sure you know what you are talking about. And also, maybe you are a little bit underestimating the links between HoTT and constructivism.

fmap 13y ago
Since you are using the word "constructivism" so often, there is probably some sort of misunderstanding. Constructivism usually refers to the philosophical school of thought which rejects the axiom of excluded middle for fairly dogmatic reasons. Most people who learn about this are appalled, since excluded middle appears to be consistent and useful. In particular, intuitionistic set theory is weird and unintuitive - most people don't bother with it. This has little to do with the reason for constructive logic in HoTT or any type theory. Models of type theory collapse if you add excluded middle and you cannot interpret the resulting structure in any particularly useful way. Without excluded middle you have more freedom in designing new axioms. This is the reason why HoTT is constructive: You have a choice between classical logic and univalence. The latter turns out to be more useful.
- auggierose 13y ago
  So are you saying that adding the law of excluded middle would make HoTT inconsistent? That does not sound very useful.
  - fmap 13y ago
    You get a choice between univalence and excluded middle. The whole argument is that univalence is more useful in practice. Briefly, in Martin-Löf type theory equalities are very strong, but you do not have many tools for proving new equalities. Univalence is one answer to this problem. So the choice is roughly between "having more equalities" (univalence) or "making everything decidable" (excluded middle). Additionally, in HoTT you can embed classical set theory at "h-level 1". Basically, you get a slightly weaker form of excluded middle + choice, which is nevertheless sufficient for building a model of classical ZFC. The reverse is not possible, as far as I know.
    - auggierose 13y ago
      In short: I don't get a choice between univalence and excluded middle, I HAVE to choose between univalence and excluded middle. Which is an easy choice for me: I choose excluded middle.
      - fmap 13y ago
        Sorry if I wasn't clear about this, but you can embed classical mathematics in a type theory with univalence. If you look into the HoTT book, there is a chapter on set theory in type theory. The general form of excluded middle is inconsistent, because it would collapse the structures on which univalence is built. This means that classical mathematics still works as expected, so long as you have the assumption that you are working with things that are "set-like". Additionally you can make any type "set-like", since this amounts to manually collapsing its equality type. However... the truth is that most of the time excluded middle is unnecessary (in a type theory). Having nice equality types is so much more useful that, honestly, you are not making an informed decision.
        auggierose 13y ago
        Sigh. It is really hard to get straight answers out of constructivists / type theorists. So let's say I am writing a theorem proving system based on HoTT (with univalence). Can I then do the classic proof of the irrationality of the square root 2 in that system? Then this would be classical mathematics as I expect it.
        auggierose 13y ago
        Answer to the answer to my comment :-) : This is exactly the answer I expected. It was a little bit of a trap, I have to admit that. I didn't ask for any proof of the irrationality of square root 2. I asked specifically for the classic proof. Which I cannot do. So it is not classic mathematics as usual. An honest answer to this whole thread would have been: "No, you cannot do classical mathematics as you were used too. You have to give stuff up, but I think that you will gain other stuff in exchange, and in my opinion this other stuff is more valuable than the stuff you gave up."

fmap 13y ago

Since you are using the word "constructivism" so often, there is probably some sort of misunderstanding. Constructivism usually refers to the philosophical school of thought which rejects the axiom of excluded middle for fairly dogmatic reasons. Most people who learn about this are appalled, since excluded middle appears to be consistent and useful. In particular, intuitionistic set theory is weird and unintuitive - most people don't bother with it. This has little to do with the reason for constructive logic in HoTT or any type theory. Models of type theory collapse if you add excluded middle and you cannot interpret the resulting structure in any particularly useful way. Without excluded middle you have more freedom in designing new axioms. This is the reason why HoTT is constructive: You have a choice between classical logic and univalence. The latter turns out to be more useful.

auggierose 13y ago
So are you saying that adding the law of excluded middle would make HoTT inconsistent? That does not sound very useful.
- fmap 13y ago
  You get a choice between univalence and excluded middle. The whole argument is that univalence is more useful in practice. Briefly, in Martin-Löf type theory equalities are very strong, but you do not have many tools for proving new equalities. Univalence is one answer to this problem. So the choice is roughly between "having more equalities" (univalence) or "making everything decidable" (excluded middle). Additionally, in HoTT you can embed classical set theory at "h-level 1". Basically, you get a slightly weaker form of excluded middle + choice, which is nevertheless sufficient for building a model of classical ZFC. The reverse is not possible, as far as I know.
  - auggierose 13y ago
    In short: I don't get a choice between univalence and excluded middle, I HAVE to choose between univalence and excluded middle. Which is an easy choice for me: I choose excluded middle.
    - fmap 13y ago
      Sorry if I wasn't clear about this, but you can embed classical mathematics in a type theory with univalence. If you look into the HoTT book, there is a chapter on set theory in type theory. The general form of excluded middle is inconsistent, because it would collapse the structures on which univalence is built. This means that classical mathematics still works as expected, so long as you have the assumption that you are working with things that are "set-like". Additionally you can make any type "set-like", since this amounts to manually collapsing its equality type. However... the truth is that most of the time excluded middle is unnecessary (in a type theory). Having nice equality types is so much more useful that, honestly, you are not making an informed decision.
      - auggierose 13y ago
        Sigh. It is really hard to get straight answers out of constructivists / type theorists. So let's say I am writing a theorem proving system based on HoTT (with univalence). Can I then do the classic proof of the irrationality of the square root 2 in that system? Then this would be classical mathematics as I expect it.
        auggierose 13y ago
        Answer to the answer to my comment :-) : This is exactly the answer I expected. It was a little bit of a trap, I have to admit that. I didn't ask for any proof of the irrationality of square root 2. I asked specifically for the classic proof. Which I cannot do. So it is not classic mathematics as usual. An honest answer to this whole thread would have been: "No, you cannot do classical mathematics as you were used too. You have to give stuff up, but I think that you will gain other stuff in exchange, and in my opinion this other stuff is more valuable than the stuff you gave up."