9 ms·

I find it strange that HoTT and HoTT-adjacent stuff gets posted here so often. Even in the world of pure mathematics, this is a backwater. As I understand it,

I find it strange that HoTT and HoTT-adjacent stuff gets posted here so often. Even in the world of pure mathematics, this is a backwater. As I understand it, the two main selling points are providing a foundation for mathematics and a framework for automated theorem proving, but: 1) We already have a perfectly good foundation of mathematics. It's called ZFC [1], and it does everything we need it to do. If all HoTT does is give a theory that's mutually interpretable with ZFC, that's not interesting (at least to mainstream workers in the foundations of mathematics, who would rather tackle substantive problems). There are also people like Per-Martin Lof who want to use HoTT as a vehicle for doing mathematics with intuitionistic logic, and in particular denying the law of excluded middle, but at that point you've let the mask slip and you're advocating something that interests approximately zero mainstream mathematicians. 2) It's not at all clear HoTT, or type theory in general, is the best solution for formalizing mathematics. It could be, it couldn't be, but this is ultimately an empirical question . Some comments on the state of the field are given in [2]. [2]: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa...

s17n 6y ago
It's popular at CMU? It got a huge-for-pure-math grant 5 years ago (https://homotopytypetheory.org/2014/04/29/hott-awarded-a-muri/ https://homotopytypetheory.org/2014/04/29/hott-awarded-a-mur...)? Idk.
andrewla 6y ago
> vehicle for doing mathematics with intuitionistic logic, and in particular denying the law of excluded middle I think this is the basis for the enthusiasm, almost entirely. There's a growing perception that a lot of mathematical abstractions that are purely naval-gazing have arisen from ZFC, and the intuitionalists and finitists are gaining followers amongst amateur and upcoming mathematicians. I don't have data to back this, just a feeling that I get. And I think in particular this is attractive to programmers because this skews closer to what we've learned about computability and program design, and I think there's even some hope of moving forward from obscure notation and single-letter variable names towards a syntax for doing mathematics that can be more expressive and easier to verify.
- boyobo 6y ago
  You don't need anything like HoTT to start using multi-letter variable names. E.g. https://mitpress.mit.edu/books/functional-differential-geometry https://mitpress.mit.edu/books/functional-differential-geome...
  - foxes 6y ago
    I just had a flip through this book, yes all the differential geometry is there, but I think its a bit of a let down. If I think "functional" I want to think more abstractly in terms of categories, functors, functions. The Lisp code in this book is truly not doing anything for me. Seems like a kind of direct numerical computation/translation. I actually think it would be better to do it in Haskell which seems like it would at least let you identify some more generic structures (oh we can actually implement this idea x as a functor/monad blah blah).
- taliesinb 6y ago
  Couldn’t agree more. A great example of a mathematics popularizer along these lines is Norman Wildberger, who has an astonishing range of videos on youtube about an amazing range of mathematical topics. Here’s an interview with him: https://youtu.be/E_dGqavx5AU https://youtu.be/E_dGqavx5AU . My personal feeling is that a lot of beautiful and interesting mathematics will arise as a result of an intuitionist, finitist, computationalist rethinking of the foundations of mathematics.
- auggierose 6y ago
  I am not sure HoTT is your best bet if you want to get away from obscure notation and naval-gazing. Just kidding. But seriously, ZFC is probably the easiest foundation you can have for proper mathematics. Anything else is more complicated (if you think otherwise, you probably just don't understand it).
remexre 6y ago
I think Cubical Type Theory (derived from HoTT) is a part of the future for general-purpose dependently-typed programming -- it has canonicity, which I'd argue is necessary for a general-purpose programming language, and it being suitable for a foundation of mathematics nigh-guarantees it's powerful enough to express whatever properties are useful in the domain.
- harveywi 6y ago
  So you're saying that cubical type theory will be a good fit for cubical programming?
- curryhoward 6y ago
  > it has canonicity, which I'd argue is necessary for a general-purpose programming language MLTT, even without HoTT/CTT, already features canonicity, no? (At least for positive types.) I thought the main advantage of HoTT is that you can define non-trivial equalities, and the advantage of CTT in particular is that univalence can be derived in it (rather than introducing it as a non-computational axiom).
  - remexre 6y ago
    Right, I think I'd put univalence in my list of "I want this for my dream general-purpose dependently-typed programming language" features; being able to prove properties on simple representations of data and transport those properties to more optimized forms is pretty important, imo.
voxl 6y ago
Your first point is hysterical considering we as computer scientists use many many different programming languages. Nah the math people are fine with assembly, even though they don't actually use it in their work.
- boyobo 6y ago
  That's a flawed analogy. Mathematicians do use 'higher level languages', that's precisely why most of them don't care about HoTT vs set theory. Just like a web dev usually does not care about the instruction set of the processor.
  - voxl 6y ago
    Its not flawed because the correct analogy is: pen and paper Turing machines versus Python.
    - boyobo 6y ago
      Now I'm not sure what your point is. Are you suggesting that HoTT is to python as ZFC is to turing machine tape?
      - zrkrlc 6y ago
        Nitpick, but I think what you meant to say what "HoTT is to ZFC as Python is to Turing machine tape". Hope it helps.
nickdrozd 6y ago
> ...a vehicle for doing mathematics with intuitionistic logic, and in particular denying the law of excluded middle... Intuitionists don't deny the law of excluded middle, they just don't admit it as an axiom. From a classical perspective this looks like denial, since accepting the law means that you have to accept or deny everything, but from an intuitionistic perspective that kind of reasoning looks like begging the question.
throwawaygh 6y ago
> I find it strange that HoTT and HoTT-adjacent stuff gets posted here so often. I don't have any dog in this fight, but I also find it super interesting that this topic gets to the 1st page so often. TBH I think answering that question is more interesting that litigating foundations.
ajkjk 6y ago
I think people are excited about the connection to type theory (tangentially connected to tech) as well as the idea that this field and the book are being developed in such an open-source way.
pgustafs 6y ago
> If all HoTT does is give a theory that's mutually interpretable with ZFC, that's not interesting. "If all python does is give a theory that's mutually interpretable with x86 assembly, that's not interesting." The point is to have better language support for expressing the things you want to reason about. I don't find it so far-fetched to be interested in better ways of reasoning about equality of types (both as a programmer and as a mathematician).
- spekcular 6y ago
  I don't think this is a good analogy. No one "does mathematics" in ZFC. Mathematicians don't express their reasoning in set-theoretic axioms; they do so in common language proofs. You can see this by opening any graduate textbook or journal. Mainstream mathematicians are not being prevented from proving theorems because they lack "better ways of reasoning about equality of types." The importance of ZFC is that it ensures our common language reasoning isn't incoherent (among other things). Once you've done that, you don't need to do it again.
  - pgustafs 6y ago
    Mathematicians use implicit DSLs approximately embedded in natural language to write proofs. Formalizing these DSLs in ZFC is a nightmare because its axioms are arcane and far from common mathematical discourse (much like assembly). On the other hand, the type formers and rules of (say) MLTT are natural generalizations of the rules of ordinary logic. > Mainstream mathematicians are not being prevented from proving theorems because they lack "better ways of reasoning about equality of types." How do you know? I've made the mistake of assuming that the definition of a certain morphism is natural with respect to a certain object when it wasn't (coevaluation in a rigid monoidal category). Better language for equality and naturality are precisely what HoTT provides. More importantly, the hope is that type theory will not only provide better language, but relieve us of the tedium of checking proofs by hand. > The importance of ZFC is that it ensures our common language reasoning isn't incoherent. I don't think this is true. AFAIK, no one has written down the definition of (say) a scheme from first principles in ZFC. In fact, if you care about coherence/verification, you should care even more about type theory. IIRC this is what drew Voevodsky to type theory in the first place -- https://mathoverflow.net/questions/234492/what-is-the-mistake-in-the-proof-of-the-homotopy-hypothesis-by-kapranov-and-voev https://mathoverflow.net/questions/234492/what-is-the-mistak...
gnulinux 6y ago
What's the point of this comment? It's useful to some people therefore people study it. Why assume it needs to be useful to all mathematicians? It is useful for my own work, and thus I study it, why isn't this as simple as that?
- da39a3ee 6y ago
  What an extraordinary comment. You seem to be missing various points: - Mathematics is a very large field. - For beginners, it is necessary to have wiser people than yourself put up some signposts. I found the comment you're referring to very illuminating. I'm not naively assuming the author's view is the only one, or "correct", but s/he certainly like they have some familiarity with graduate/research level mathematics in relevant areas. So it was very helpful to see, at least from the point of view of some mathematicians, that this is not considered an important area. I was left wondering whether the author of that comment understood the importance of this stuff in computer science (i.e. in academic approaches to programming languages, might be the right term, I don't know, I'm pretty ignorant of these areas myself), or whether they were only able to criticize it from the point of view of pure mathematics.
  - oisdk 6y ago
    > s/he certainly like they have some familiarity with graduate/research level mathematics in relevant areas You should not assume this about any anonymous person on the internet.
- spekcular 6y ago
  I don't know what your work is, but for the vast majority of people learning HoTT is a complete waste of time. There are many intelligent and curious people reading HN, who might be tempted to spend time understanding it because its somewhat frequent appearance here gives the (false) impression that it plays some important role in modern mathematics. I regret spending the (large) amount of time I did learning what it is about, only to realize that's not much actual content there, and I would hope my post saves other people that trouble. There is a lot of far more interesting, elegant, and useful mathematics out there, imo.
guerrilla 6y ago
You don't sound like you've heard of the Curry-Howard isomorphism. We want practical dependently typed programming languages, ZFC is useless for that. Furthermore, LEM is never denied, it's just not adopted as an axion and thus requires proof per case.
creata 6y ago
1. ZFC does everything you need it to do. It's a really hard set of axioms for me to justify compared to MLTT, and it's important to me how "obvious" some set of axioms is. MLTT also has the advantage that it's very easy to use without encoding everything into well-founded, untyped trees, which is nice. 2. What are these "substantive problems"? I don't have any experience in foundations, so I'm genuinely curious. 3. Sure, intuitionistic mathematics has very little popularity, but a lot of that popularity is among computer scientists, for fairly obvious reasons. 4. The HoTT book and the nLab are two of the most out-in-the-open developments in math I've seen --- the HoTT book was even written in a public GitHub repo iirc. Naturally that has a lot of appeal for HN. If you have anything similar (blogs, wikis, etc.) for mainstream foundations, I'd love to read them. 5. Yeah, personally, I'm not really convinced that HoTT is a good idea, but I guess we'll just have to wait and see.
- spekcular 6y ago
  1. ZFC is fairly "obvious" when taught the right way. Unfortunately, most people do have not the privilege of a good set theory instructor. 2. Whether V equals Ultimate L, for example. There's "pop math" coverage available [1], as well as more technical introductions by Woodin if you Google for them. 3. I'm not sure what reasons you're referring to; can you enlighten me? I can guess, but the ones I'm guessing are not very good, and I'd rather not attribute weak arguments to you or them. 4. The Stacks Project, for one [2]. It covers most of the foundations of modern algebraic geometry, is of extremely high quality, and is regularly cited in research papers. [1]: https://www.quantamagazine.org/to-settle-infinity-question-a-new-law-of-mathematics-20131126/ https://www.quantamagazine.org/to-settle-infinity-question-a... [2]: https://stacks.math.columbia.edu/ https://stacks.math.columbia.edu/
  - mkehrt 6y ago
    3. I am not sure what GP meant with this, but I do know that in type theory, intuitionistic logic is very important. The propositions of intuitionistic logic correspond exactly to the types of types programs in certain models of programming languages, and the proofs of intuitionistic logic to well-typed programs in those models. This is called the Curry-Howard isomorphism, and has been a very fruitful source of inspiration for type theory. For example, it was originally noted for intuitionistic propositional logic only, but adding universal quantification gives a type theory with so-called parametric polymorphism, which was later developed into generics in Java and other languages. I have seen modal logic used to model distributed computation, and linear logic inspired work which eventually led to Rust's borrow checker.
jcoq 6y ago
There are numerous advantages to having a complete categorical or type-theoretic foundations of mathematics, especially one as constructive as HoTT. The main advantages in my areas of research would be that proofs in "higher-category theory" would become less cumbersome. Many set-theoretic proofs in this area are non-informative because they are are messy and opaque. This is the real promise offered by any alternative theory or explanation: insight. Besides the immediate usefulness: if "all HoTT does is give a theory that's mutually interpretable with ZFC", then holy shit what an accomplishment! You seem to have a fundamental misunderstanding about the nature of mathematical research. Most fields of research do nothing but "give a theory that's mutually interpretable" with some other field, or at least did so initially.
giraj 6y ago
I wouldn't be surprised to see anything related to type-theory on here. And I disagree that many people doing HoTT today are proposing it as an alternative foundation in anything except (categorical) homotopy theory, and I'd like to know where you see anyone doing that. Intuitionism in HoTT isn't about constructivity, which I agree is rejected by mainstream mathematicians. It's about the models of the theory. For example, LEM doesn't hold in the category of bundles over the circle (see my other comment on here). If you think of the axiom of choice as "every surjection has a section", then this doesn't hold for topological spaces. (Take the double cover of the circle; there's no continuous section.) I disagree that these examples are uninteresting to mainstream mathematicians.
mkehrt 6y ago
My (educated layman) understanding is that there actually is a useful thing that HoTT gives us as a foundation for mathematics. that ZFC does not. This is the translation of proofs from one structure to an isomorphic one. For example, if I have, say, a group, and I prove something about it, you would think that the proof would hold for all isomorphic groups. Under ZFC this isn't true, or at least we don't get it for free. Under HoTT, we get this for free.
foxes 6y ago
I would guess most mathematicians do not truly fully use ZFC at all. I think there is a lot of mathematics that is done which is actually independent of ZFC, its more expressive than needed (if we look at reverse mathematics).
librexpr 6y ago
As an amateur who nowadays works a lot with ZFC (but who doesn't know HoTT) and who is very interested in foundations, I don't think that learning HoTT is a waste of time, I'm sure HoTT is great and I'm glad there are people working on it. However, my time is limited, so I can't really afford to spend months going down a rabbit hole if it's not going to help me with my work. So I appreciate that you shared your experience, it was helpful in making me decide to stay focused on what I'm already doing.
- Ericson2314 6y ago
  You should really learn type theory even if you aren't interested in HoTT specifically. ZFC is a pretty ugly formalization. My "empirical" evidence for this is most working mathematicians today do not care about foundations at all, whereas with something better, they might.
  - fractionalhare 6y ago
    Most mathematicians still wouldn't care about foundations if you came up with better foundations. It's a separate area of research from most other fields of mathematics, it's not relevant to what most of them are researching, and they just don't have any interest in it. And unlike category theory more broadly, they don't particularly benefit by studying foundations deeply. It doesn't provide any improvement to their own area of study. Everything I've just said is completely uncontroversial among mathematicians, for what it's worth. The comment I just wrote has probably been expressed on r/math dozens of times at this point.
    - Ericson2314 6y ago
      Yes I agree with that. Let me fix my phrasing: they still wouldn't all suddenly start researching mathematical foundations, but they might apply foundational tools to what they are doing. Really "foundations" is a word that emphasizes the ZFC "learn and ignore" approach. The type theory / category theory approach might better be called "framing", in that it begins in the pilings below the basement but also goes all the way to the roof.
pcstl 6y ago
HoTT is very interesting to people working on programming language theory. I, for one, expect we will see a handful of very interesting research programming languages coming out in the near-future with HoTT-based features, which will allow a lot of stuff which is currently inefficient to do in functional languages to be implemented in very efficient (and provably safe) ways. Sure, that's very much a niche and we can't be sure anything practical will come out of it, but for some of us it's interesting in its own right. :) I understand how this isn't interesting to folks working on pure math, just as category theory likely isn't, but it's the fact that these mathematical abstractions map so well onto (certain kinds of) programming that makes them such recurrent topics on HN.
jes5199 6y ago
the audience here tends to have more of a Computer Science background rather than a traditional Mathematics background, and HoTT feels more like a CS theory than like traditional math. When I read about the kind of reasoning that lead to ZFC, I get frustrated because that style of thinking feels unnatural to me. HoTT feels more like how I think, when I’m trying to solve problems. Not that I could productively do math research in either system - I’m not a mathematician at all! It’s just an aesthetic judgement.
black_knight 6y ago
> There are also people like Per-Martin Lof who want to use HoTT… Sorry, but this is plainly false. Per does not want to use HoTT. My impression is that he finds HoTT mildly interesting, and has not really used/advocated it. And, you are implicitly calling him and Voedvodsky "not a mainstream mathematician", which is rather offensive considering their contributions to statistics (Per) and homotopy theory (Vladimir). Your comment comes out as very reactionary. There is room for a lot of both HoTT (weather classical logic is used or not) and set theory in modern mathematics. In fact, doing set theory in HoTT is a very pleasant experience!
- spekcular 6y ago
  Martin-Lof went to at least one early HoTT conference and his interest is clearly in intuitionistic type theory, so I don't think my statement is inaccurate. Anyway, the broader point is that there's a community of people whose interest comes from that viewpoint. I also don't think it's inaccurate or offensive to say Martin-Lof no longer works in mainstream mathematics. He hasn't done statistics since the 70s. Voevodsky was of course a great mathematician, but it seems quite clear that his work in type theory was not mainstream mathematics and not of interest to most mathematicians (quantifying over, say, people who hold jobs as postdocs or professors in math departments worldwide). Whether the work is valuable is a separate question, but the sociological point is, imo, pretty inarguable.
Kutta 6y ago
> We already have a perfectly good foundation of mathematics. It's called ZFC [1] This is completely missing a core point of category theory and type theory (which is about categories equipped with certain extra structure), which is to work is settings which can be flexibly tightened or loosened in order to do constructions which are as general as possible. A theorem in HoTT is far more widely applicable than a theorem in ZFC; HoTT can be interpreted in any higher Gröthendieck topos, ZFC can be only intepreted in a certain class of 1-toposes. In HoTT, we can simply assume choice and LEM to internally reproduce ZFC. In ZFC, univalence is false and cannot be assumed. > It's not at all clear HoTT, or type theory in general, is the best solution for formalizing mathematics Xena project isn't too hot on HoTT indeed, but they will tell you that type theory in general is absolutely the best solution for formalizing mathematics. > in particular denying the law of excluded middle MLTT does not deny LEM, nor HoTT. The point is not to deny LEM, but to work in a more general system which does not necessarily assume it.
Certhas 6y ago
The vast majority of people that design and write rigorously formal systems to express complex real world ideas and behaviours are programmers. They are rigorous, not in the sense that anything is ever proven about their formal systems, but in the sense that they are interpreted rigorously as to their formal consequences by computers. This is really different to how I as a physicist might use equations to express ideas to other physicists, and if I can't exactly formalize what the equation means that isn't always relevant. This is of course an unorthodox way to frame what programmers do, but I think it's relevant to your last comment. What is a good foundation for formal systems is an empirical question, and empirically, type theory is extremely important to programmers. Set theory not at all.

s17n 6y ago

It's popular at CMU? It got a huge-for-pure-math grant 5 years ago (https://homotopytypetheory.org/2014/04/29/hott-awarded-a-muri/ https://homotopytypetheory.org/2014/04/29/hott-awarded-a-mur...)? Idk.

andrewla 6y ago

> vehicle for doing mathematics with intuitionistic logic, and in particular denying the law of excluded middle I think this is the basis for the enthusiasm, almost entirely. There's a growing perception that a lot of mathematical abstractions that are purely naval-gazing have arisen from ZFC, and the intuitionalists and finitists are gaining followers amongst amateur and upcoming mathematicians. I don't have data to back this, just a feeling that I get. And I think in particular this is attractive to programmers because this skews closer to what we've learned about computability and program design, and I think there's even some hope of moving forward from obscure notation and single-letter variable names towards a syntax for doing mathematics that can be more expressive and easier to verify.

boyobo 6y ago
You don't need anything like HoTT to start using multi-letter variable names. E.g. https://mitpress.mit.edu/books/functional-differential-geometry https://mitpress.mit.edu/books/functional-differential-geome...
- foxes 6y ago
  I just had a flip through this book, yes all the differential geometry is there, but I think its a bit of a let down. If I think "functional" I want to think more abstractly in terms of categories, functors, functions. The Lisp code in this book is truly not doing anything for me. Seems like a kind of direct numerical computation/translation. I actually think it would be better to do it in Haskell which seems like it would at least let you identify some more generic structures (oh we can actually implement this idea x as a functor/monad blah blah).
taliesinb 6y ago
Couldn’t agree more. A great example of a mathematics popularizer along these lines is Norman Wildberger, who has an astonishing range of videos on youtube about an amazing range of mathematical topics. Here’s an interview with him: https://youtu.be/E_dGqavx5AU https://youtu.be/E_dGqavx5AU . My personal feeling is that a lot of beautiful and interesting mathematics will arise as a result of an intuitionist, finitist, computationalist rethinking of the foundations of mathematics.
auggierose 6y ago
I am not sure HoTT is your best bet if you want to get away from obscure notation and naval-gazing. Just kidding. But seriously, ZFC is probably the easiest foundation you can have for proper mathematics. Anything else is more complicated (if you think otherwise, you probably just don't understand it).

remexre 6y ago

I think Cubical Type Theory (derived from HoTT) is a part of the future for general-purpose dependently-typed programming -- it has canonicity, which I'd argue is necessary for a general-purpose programming language, and it being suitable for a foundation of mathematics nigh-guarantees it's powerful enough to express whatever properties are useful in the domain.

harveywi 6y ago
So you're saying that cubical type theory will be a good fit for cubical programming?
curryhoward 6y ago
> it has canonicity, which I'd argue is necessary for a general-purpose programming language MLTT, even without HoTT/CTT, already features canonicity, no? (At least for positive types.) I thought the main advantage of HoTT is that you can define non-trivial equalities, and the advantage of CTT in particular is that univalence can be derived in it (rather than introducing it as a non-computational axiom).
- remexre 6y ago
  Right, I think I'd put univalence in my list of "I want this for my dream general-purpose dependently-typed programming language" features; being able to prove properties on simple representations of data and transport those properties to more optimized forms is pretty important, imo.

voxl 6y ago

Your first point is hysterical considering we as computer scientists use many many different programming languages. Nah the math people are fine with assembly, even though they don't actually use it in their work.

boyobo 6y ago
That's a flawed analogy. Mathematicians do use 'higher level languages', that's precisely why most of them don't care about HoTT vs set theory. Just like a web dev usually does not care about the instruction set of the processor.
- voxl 6y ago
  Its not flawed because the correct analogy is: pen and paper Turing machines versus Python.
  - boyobo 6y ago
    Now I'm not sure what your point is. Are you suggesting that HoTT is to python as ZFC is to turing machine tape?
    - zrkrlc 6y ago
      Nitpick, but I think what you meant to say what "HoTT is to ZFC as Python is to Turing machine tape". Hope it helps.

nickdrozd 6y ago

> ...a vehicle for doing mathematics with intuitionistic logic, and in particular denying the law of excluded middle... Intuitionists don't deny the law of excluded middle, they just don't admit it as an axiom. From a classical perspective this looks like denial, since accepting the law means that you have to accept or deny everything, but from an intuitionistic perspective that kind of reasoning looks like begging the question.

throwawaygh 6y ago

> I find it strange that HoTT and HoTT-adjacent stuff gets posted here so often. I don't have any dog in this fight, but I also find it super interesting that this topic gets to the 1st page so often. TBH I think answering that question is more interesting that litigating foundations.

ajkjk 6y ago

I think people are excited about the connection to type theory (tangentially connected to tech) as well as the idea that this field and the book are being developed in such an open-source way.

pgustafs 6y ago

> If all HoTT does is give a theory that's mutually interpretable with ZFC, that's not interesting. "If all python does is give a theory that's mutually interpretable with x86 assembly, that's not interesting." The point is to have better language support for expressing the things you want to reason about. I don't find it so far-fetched to be interested in better ways of reasoning about equality of types (both as a programmer and as a mathematician).

spekcular 6y ago
I don't think this is a good analogy. No one "does mathematics" in ZFC. Mathematicians don't express their reasoning in set-theoretic axioms; they do so in common language proofs. You can see this by opening any graduate textbook or journal. Mainstream mathematicians are not being prevented from proving theorems because they lack "better ways of reasoning about equality of types." The importance of ZFC is that it ensures our common language reasoning isn't incoherent (among other things). Once you've done that, you don't need to do it again.
- pgustafs 6y ago
  Mathematicians use implicit DSLs approximately embedded in natural language to write proofs. Formalizing these DSLs in ZFC is a nightmare because its axioms are arcane and far from common mathematical discourse (much like assembly). On the other hand, the type formers and rules of (say) MLTT are natural generalizations of the rules of ordinary logic. > Mainstream mathematicians are not being prevented from proving theorems because they lack "better ways of reasoning about equality of types." How do you know? I've made the mistake of assuming that the definition of a certain morphism is natural with respect to a certain object when it wasn't (coevaluation in a rigid monoidal category). Better language for equality and naturality are precisely what HoTT provides. More importantly, the hope is that type theory will not only provide better language, but relieve us of the tedium of checking proofs by hand. > The importance of ZFC is that it ensures our common language reasoning isn't incoherent. I don't think this is true. AFAIK, no one has written down the definition of (say) a scheme from first principles in ZFC. In fact, if you care about coherence/verification, you should care even more about type theory. IIRC this is what drew Voevodsky to type theory in the first place -- https://mathoverflow.net/questions/234492/what-is-the-mistake-in-the-proof-of-the-homotopy-hypothesis-by-kapranov-and-voev https://mathoverflow.net/questions/234492/what-is-the-mistak...

gnulinux 6y ago

What's the point of this comment? It's useful to some people therefore people study it. Why assume it needs to be useful to all mathematicians? It is useful for my own work, and thus I study it, why isn't this as simple as that?

da39a3ee 6y ago
What an extraordinary comment. You seem to be missing various points: - Mathematics is a very large field. - For beginners, it is necessary to have wiser people than yourself put up some signposts. I found the comment you're referring to very illuminating. I'm not naively assuming the author's view is the only one, or "correct", but s/he certainly like they have some familiarity with graduate/research level mathematics in relevant areas. So it was very helpful to see, at least from the point of view of some mathematicians, that this is not considered an important area. I was left wondering whether the author of that comment understood the importance of this stuff in computer science (i.e. in academic approaches to programming languages, might be the right term, I don't know, I'm pretty ignorant of these areas myself), or whether they were only able to criticize it from the point of view of pure mathematics.
- oisdk 6y ago
  > s/he certainly like they have some familiarity with graduate/research level mathematics in relevant areas You should not assume this about any anonymous person on the internet.
spekcular 6y ago
I don't know what your work is, but for the vast majority of people learning HoTT is a complete waste of time. There are many intelligent and curious people reading HN, who might be tempted to spend time understanding it because its somewhat frequent appearance here gives the (false) impression that it plays some important role in modern mathematics. I regret spending the (large) amount of time I did learning what it is about, only to realize that's not much actual content there, and I would hope my post saves other people that trouble. There is a lot of far more interesting, elegant, and useful mathematics out there, imo.

guerrilla 6y ago

You don't sound like you've heard of the Curry-Howard isomorphism. We want practical dependently typed programming languages, ZFC is useless for that. Furthermore, LEM is never denied, it's just not adopted as an axion and thus requires proof per case.

creata 6y ago

1. ZFC does everything you need it to do. It's a really hard set of axioms for me to justify compared to MLTT, and it's important to me how "obvious" some set of axioms is. MLTT also has the advantage that it's very easy to use without encoding everything into well-founded, untyped trees, which is nice. 2. What are these "substantive problems"? I don't have any experience in foundations, so I'm genuinely curious. 3. Sure, intuitionistic mathematics has very little popularity, but a lot of that popularity is among computer scientists, for fairly obvious reasons. 4. The HoTT book and the nLab are two of the most out-in-the-open developments in math I've seen --- the HoTT book was even written in a public GitHub repo iirc. Naturally that has a lot of appeal for HN. If you have anything similar (blogs, wikis, etc.) for mainstream foundations, I'd love to read them. 5. Yeah, personally, I'm not really convinced that HoTT is a good idea, but I guess we'll just have to wait and see.

spekcular 6y ago
1. ZFC is fairly "obvious" when taught the right way. Unfortunately, most people do have not the privilege of a good set theory instructor. 2. Whether V equals Ultimate L, for example. There's "pop math" coverage available [1], as well as more technical introductions by Woodin if you Google for them. 3. I'm not sure what reasons you're referring to; can you enlighten me? I can guess, but the ones I'm guessing are not very good, and I'd rather not attribute weak arguments to you or them. 4. The Stacks Project, for one [2]. It covers most of the foundations of modern algebraic geometry, is of extremely high quality, and is regularly cited in research papers. [1]: https://www.quantamagazine.org/to-settle-infinity-question-a-new-law-of-mathematics-20131126/ https://www.quantamagazine.org/to-settle-infinity-question-a... [2]: https://stacks.math.columbia.edu/ https://stacks.math.columbia.edu/
- mkehrt 6y ago
  3. I am not sure what GP meant with this, but I do know that in type theory, intuitionistic logic is very important. The propositions of intuitionistic logic correspond exactly to the types of types programs in certain models of programming languages, and the proofs of intuitionistic logic to well-typed programs in those models. This is called the Curry-Howard isomorphism, and has been a very fruitful source of inspiration for type theory. For example, it was originally noted for intuitionistic propositional logic only, but adding universal quantification gives a type theory with so-called parametric polymorphism, which was later developed into generics in Java and other languages. I have seen modal logic used to model distributed computation, and linear logic inspired work which eventually led to Rust's borrow checker.

jcoq 6y ago

There are numerous advantages to having a complete categorical or type-theoretic foundations of mathematics, especially one as constructive as HoTT. The main advantages in my areas of research would be that proofs in "higher-category theory" would become less cumbersome. Many set-theoretic proofs in this area are non-informative because they are are messy and opaque. This is the real promise offered by any alternative theory or explanation: insight. Besides the immediate usefulness: if "all HoTT does is give a theory that's mutually interpretable with ZFC", then holy shit what an accomplishment! You seem to have a fundamental misunderstanding about the nature of mathematical research. Most fields of research do nothing but "give a theory that's mutually interpretable" with some other field, or at least did so initially.

giraj 6y ago

I wouldn't be surprised to see anything related to type-theory on here. And I disagree that many people doing HoTT today are proposing it as an alternative foundation in anything except (categorical) homotopy theory, and I'd like to know where you see anyone doing that. Intuitionism in HoTT isn't about constructivity, which I agree is rejected by mainstream mathematicians. It's about the models of the theory. For example, LEM doesn't hold in the category of bundles over the circle (see my other comment on here). If you think of the axiom of choice as "every surjection has a section", then this doesn't hold for topological spaces. (Take the double cover of the circle; there's no continuous section.) I disagree that these examples are uninteresting to mainstream mathematicians.

mkehrt 6y ago

My (educated layman) understanding is that there actually is a useful thing that HoTT gives us as a foundation for mathematics. that ZFC does not. This is the translation of proofs from one structure to an isomorphic one. For example, if I have, say, a group, and I prove something about it, you would think that the proof would hold for all isomorphic groups. Under ZFC this isn't true, or at least we don't get it for free. Under HoTT, we get this for free.

foxes 6y ago

I would guess most mathematicians do not truly fully use ZFC at all. I think there is a lot of mathematics that is done which is actually independent of ZFC, its more expressive than needed (if we look at reverse mathematics).

librexpr 6y ago

As an amateur who nowadays works a lot with ZFC (but who doesn't know HoTT) and who is very interested in foundations, I don't think that learning HoTT is a waste of time, I'm sure HoTT is great and I'm glad there are people working on it. However, my time is limited, so I can't really afford to spend months going down a rabbit hole if it's not going to help me with my work. So I appreciate that you shared your experience, it was helpful in making me decide to stay focused on what I'm already doing.

Ericson2314 6y ago
You should really learn type theory even if you aren't interested in HoTT specifically. ZFC is a pretty ugly formalization. My "empirical" evidence for this is most working mathematicians today do not care about foundations at all, whereas with something better, they might.
- fractionalhare 6y ago
  Most mathematicians still wouldn't care about foundations if you came up with better foundations. It's a separate area of research from most other fields of mathematics, it's not relevant to what most of them are researching, and they just don't have any interest in it. And unlike category theory more broadly, they don't particularly benefit by studying foundations deeply. It doesn't provide any improvement to their own area of study. Everything I've just said is completely uncontroversial among mathematicians, for what it's worth. The comment I just wrote has probably been expressed on r/math dozens of times at this point.
  - Ericson2314 6y ago
    Yes I agree with that. Let me fix my phrasing: they still wouldn't all suddenly start researching mathematical foundations, but they might apply foundational tools to what they are doing. Really "foundations" is a word that emphasizes the ZFC "learn and ignore" approach. The type theory / category theory approach might better be called "framing", in that it begins in the pilings below the basement but also goes all the way to the roof.

pcstl 6y ago

HoTT is very interesting to people working on programming language theory. I, for one, expect we will see a handful of very interesting research programming languages coming out in the near-future with HoTT-based features, which will allow a lot of stuff which is currently inefficient to do in functional languages to be implemented in very efficient (and provably safe) ways. Sure, that's very much a niche and we can't be sure anything practical will come out of it, but for some of us it's interesting in its own right. :) I understand how this isn't interesting to folks working on pure math, just as category theory likely isn't, but it's the fact that these mathematical abstractions map so well onto (certain kinds of) programming that makes them such recurrent topics on HN.

jes5199 6y ago

the audience here tends to have more of a Computer Science background rather than a traditional Mathematics background, and HoTT feels more like a CS theory than like traditional math. When I read about the kind of reasoning that lead to ZFC, I get frustrated because that style of thinking feels unnatural to me. HoTT feels more like how I think, when I’m trying to solve problems. Not that I could productively do math research in either system - I’m not a mathematician at all! It’s just an aesthetic judgement.

black_knight 6y ago

> There are also people like Per-Martin Lof who want to use HoTT… Sorry, but this is plainly false. Per does not want to use HoTT. My impression is that he finds HoTT mildly interesting, and has not really used/advocated it. And, you are implicitly calling him and Voedvodsky "not a mainstream mathematician", which is rather offensive considering their contributions to statistics (Per) and homotopy theory (Vladimir). Your comment comes out as very reactionary. There is room for a lot of both HoTT (weather classical logic is used or not) and set theory in modern mathematics. In fact, doing set theory in HoTT is a very pleasant experience!

spekcular 6y ago
Martin-Lof went to at least one early HoTT conference and his interest is clearly in intuitionistic type theory, so I don't think my statement is inaccurate. Anyway, the broader point is that there's a community of people whose interest comes from that viewpoint. I also don't think it's inaccurate or offensive to say Martin-Lof no longer works in mainstream mathematics. He hasn't done statistics since the 70s. Voevodsky was of course a great mathematician, but it seems quite clear that his work in type theory was not mainstream mathematics and not of interest to most mathematicians (quantifying over, say, people who hold jobs as postdocs or professors in math departments worldwide). Whether the work is valuable is a separate question, but the sociological point is, imo, pretty inarguable.

Kutta 6y ago

> We already have a perfectly good foundation of mathematics. It's called ZFC [1] This is completely missing a core point of category theory and type theory (which is about categories equipped with certain extra structure), which is to work is settings which can be flexibly tightened or loosened in order to do constructions which are as general as possible. A theorem in HoTT is far more widely applicable than a theorem in ZFC; HoTT can be interpreted in any higher Gröthendieck topos, ZFC can be only intepreted in a certain class of 1-toposes. In HoTT, we can simply assume choice and LEM to internally reproduce ZFC. In ZFC, univalence is false and cannot be assumed. > It's not at all clear HoTT, or type theory in general, is the best solution for formalizing mathematics Xena project isn't too hot on HoTT indeed, but they will tell you that type theory in general is absolutely the best solution for formalizing mathematics. > in particular denying the law of excluded middle MLTT does not deny LEM, nor HoTT. The point is not to deny LEM, but to work in a more general system which does not necessarily assume it.

Certhas 6y ago

The vast majority of people that design and write rigorously formal systems to express complex real world ideas and behaviours are programmers. They are rigorous, not in the sense that anything is ever proven about their formal systems, but in the sense that they are interpreted rigorously as to their formal consequences by computers. This is really different to how I as a physicist might use equations to express ideas to other physicists, and if I can't exactly formalize what the equation means that isn't always relevant. This is of course an unorthodox way to frame what programmers do, but I think it's relevant to your last comment. What is a good foundation for formal systems is an empirical question, and empirically, type theory is extremely important to programmers. Set theory not at all.