3 ms·

I did not call it gibberish. I said it was gibberish TO ME. Which is a big difference. Chapter 2 lost me at the point where infinity-groupoids entered the game

I did not call it gibberish. I said it was gibberish TO ME. Which is a big difference. Chapter 2 lost me at the point where infinity-groupoids entered the game. Until then everything was easy to understand. From then on I would have to seriously sit down and work with the book. With regard to constructive criticism: I told you what I want, make it easier to understand, and tell me what the value is for me (a non-constructive classical applied mathematician / programmer / engineer). Yep, I did not tell you HOW to get there. I see how that can be annoying for a constructive mathematician. So, maybe you can tell me: Why should I care about the univalence axiom as a non-constructivist ?

ek 13y ago
To be clear, constructive mathematics are new to me as well. The section in the introduction titled "Constructivity" may help you -- it is about trying to come to grips with the constructive nature of type theory. The short answer is that much of the mathematics that we might want to do does not require the law of the excluded middle or the axiom of choice at all when approached from a type-theoretic point of view. Higher inductive types eliminate the reliance classical logic will frequently have on either of these. To quote an example from this section, "In set-theoretic foundations, the statement 'every fully faithful and essentially surjective functor is an equivalence of categories' is equivalent to the axiom of choice. But with the univalence axiom, it is just true; see Chapter 9." The emphasis that you are placing on the fact that type theory happens to be a constructive logic is perhaps causing you to miss the point. Homotopy type theory is not about advocating constructivism. The "big idea" is that HoTT is a foundation that computers can already reason about easily, based on the work that has already been invested into developing sufficiently powerful dependently typed languages (Coq, Agda). Because it is possible to formulate set theory, category theory, and even real numbers (all discussed in part 2 of the book) within the framework of homotopy type theory, it should be possible to extend these formulations to encompass more and more results from the rest of the mathematics. Because HoTT has already been shown to be implementable (in the form of a library for Coq), this means that any math that is done informally under homotopy type theory can be carried directly into a formal, machine-checkable series of theorems and proofs, in the form of a Coq development. To expect this material to be readable and useful to every average Joe right away is asking far too much of any new idea in mathematics. This is cutting edge research, and there is still too much even the people closest to this material don't understand yet. As another comment on yours alluded to, at one time your equivalent in the 1700s would have written off calculus as indecipherable and judged it not likely to succeed as a result.
- auggierose 13y ago
  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.

ek 13y ago

To be clear, constructive mathematics are new to me as well. The section in the introduction titled "Constructivity" may help you -- it is about trying to come to grips with the constructive nature of type theory. The short answer is that much of the mathematics that we might want to do does not require the law of the excluded middle or the axiom of choice at all when approached from a type-theoretic point of view. Higher inductive types eliminate the reliance classical logic will frequently have on either of these. To quote an example from this section, "In set-theoretic foundations, the statement 'every fully faithful and essentially surjective functor is an equivalence of categories' is equivalent to the axiom of choice. But with the univalence axiom, it is just true; see Chapter 9." The emphasis that you are placing on the fact that type theory happens to be a constructive logic is perhaps causing you to miss the point. Homotopy type theory is not about advocating constructivism. The "big idea" is that HoTT is a foundation that computers can already reason about easily, based on the work that has already been invested into developing sufficiently powerful dependently typed languages (Coq, Agda). Because it is possible to formulate set theory, category theory, and even real numbers (all discussed in part 2 of the book) within the framework of homotopy type theory, it should be possible to extend these formulations to encompass more and more results from the rest of the mathematics. Because HoTT has already been shown to be implementable (in the form of a library for Coq), this means that any math that is done informally under homotopy type theory can be carried directly into a formal, machine-checkable series of theorems and proofs, in the form of a Coq development. To expect this material to be readable and useful to every average Joe right away is asking far too much of any new idea in mathematics. This is cutting edge research, and there is still too much even the people closest to this material don't understand yet. As another comment on yours alluded to, at one time your equivalent in the 1700s would have written off calculus as indecipherable and judged it not likely to succeed as a result.

auggierose 13y ago
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.