8 ms·

To the folks in this thread who think they know better than researchers at the forefront of foundational mathematics: I encourage you to learn type theory, and

To the folks in this thread who think they know better than researchers at the forefront of foundational mathematics: I encourage you to learn type theory, and especially homotopy type theory. In doing so, you'll be forced to confront the various notions of judgmental and propositional equality. You'll see why it's useful to have a formal justification for treating isomorphic objects as equal (this is called "univalence"), which is something you may have even been doing informally/subconsciously all along. In particular, homotopy type theory is a type theory, which means it looks like a programming language. So people here might find it a bit more familiar than, say, higher category theory. It'll be much easier if you know functional programming, so you may need to learn that first if you haven't already.

spekcular 5y ago
This is not "foundational mathematics." This is about the foundations of algebraic topology. The experts in the foundations of mathematics as a whole (set theorists, logicians, model theorists, etc.) don't care about homotopy type theory. It's sort of pointless for the study of the foundations of mathematics. That is, they really just care about ZF or ZFC, because those are already formulated so that they are maximally useful for foundational investigations. (And the e.g. reverse mathematics people who want to work outside of ZF/ZFC already have more direct ways of doing so.) Some idea of what people in foundations think about day-to-day can be gleaned by searching the Foundations of Math mailing list archive: https://cs.nyu.edu/pipermail/fom/ https://cs.nyu.edu/pipermail/fom/ In particular: don't confuse higher category theory (of interest to the algebraic topology community at large) with homotopy type theory (which is not). Jacob Lurie has a rather pointed conversation with Urs Schreiber about this, linked to here: https://mathematicswithoutapologies.wordpress.com/2015/05/18/jacob-lurie-explains-and-elaborates-on-his-no-comment/ https://mathematicswithoutapologies.wordpress.com/2015/05/18.... edit: I'd love to hear from the downvoters why they disagree with this take. It's pretty standard, afaik.
- zozbot234 5y ago
  > I'd love to hear from the downvoters why they disagree with this take. It's pretty standard, afaik. Because it's obtuse. There are well-known ways of phrasing all of this stuff in set theory (or rather, "legitimate" varieties of set theory) should anyone really care, replicating type-theoretical constructions by adding increasingly large "inaccessible cardinals" to one's pre-existing notion of set. But it's a pointless exercise when the type-theoretical description of these foundations is so much easier to work with. It's only useful if one believes that "set theory" is the only legitimate language for talking about anything foundational, which is again quite silly.
  - spekcular 5y ago
    In what sense is type theory "easier to work with"? For what purpose? ZFC exists largely because it's a useful framework for proving meta-mathematical theorems. In this sense, it is extremely convenient to work with. Also, I'm not sure what "all of this stuff" refers to here re: your comment about inaccessible cardinals. You don't need large cardinals to do 99.99% of modern mathematics (essentially, everything but set/proof theory). ZFC is good enough (and you can usually get away with something weaker).
    - Ericson2314 5y ago
      Frankly we are sick of set theorist traditionalists complaining about type theory, category theory, and other new things without actually bothering to understand them at all. After multiple decades, it's clear you all are never going to bother to learn our stuff nearly as well as we bothered to learn your stuff. This "debate" is thus completely unproductive without any good agreed-upon foundation to argue form. (How ironic!)
      - spekcular 5y ago
        First, I'm not a set theorist. Second, one of the major motivations for introducing type theory in mathematics was to assist with computer-aided formalization efforts, which has had some success and has a promising future (e.g. the stuff the Lean community has been doing lately). This is great! I'm not complaining at all. But I do think trumpeting HoTT as a new, improved foundation of mathematics evinces a misunderstanding of what people who work on foundations actually want out of a foundation of mathematics; or even more broadly, the mistaken belief that finding a new foundation of mathematics is an interesting project in the 21st century. Lurie's comment here explains a bit more: https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-299 https://mathematicswithoutapologies.wordpress.com/2015/05/13... (And clearly, Lurie is not some ignorant traditionalist. There's a substantive disagreement that can't be reduced to people not wanting to learn "your stuff.")
- Twisol 5y ago
  I've read rather too much of the fascinating comments thread you've indirectly linked to, but this nugget by Mike Shulman in that thread seems especially relevant to the present one: > If we distill it down from the categorical heights, this brings us back to John Baez’s pithy quote about equality: “Every interesting equation is a lie.” The only obviously true equation is x=x, but it carries no (or little) information. Any other equation, like x=y, is “a lie” because x and y are not the same thing; yet what is interesting about the equality is that they are nevertheless the same in some way. But knowing the equation doesn’t mean that we should forget all about y and use only x; the point of having the equation is that we can pass back and forth between x and y, according to which is most appropriate in any given context.
- enugu 5y ago
  Not downvoting,in particular there are useful links in your post. But note that by foundations one has atleast two different meanings. One meaning being examining the consistency of axioms or finding weakest set of axioms for a theorem. The other meaning being - finding a foundation in which a given mathematical theory is naturally and easily described, analogus to designing a programming language in which the programs are easy to describe. Most of the time in mathematics, this is done by defining high level concepts and working from there - no need to change the foundational axioms or rules of inference. But sometimes we need more - for instance, if you read the book "Synthetic Differential Geometry", infinitesimals are naturally embedded in the theory by working in a cartesian closed category of sets. One can either embed this in ZFC using cumbersome models, or change the logic itself(remove the law of excluded middle). The logic in HOTT deals with equality in a more careful way than the usual foundations. This is not restricted to algebraic topology alone - it certainly includes algebraic geometry and tackles a general issue which will plausibly have many more applications once the technology is available. The field of noncommutative geometry, in the style of Connes, is also about this as the problem of taking quotients is another way of the stating the issue with equality. It is a work in progress and might take some time before bearing substantive fruit, but note that the current alternative is that any student learning higher level mathematics at the level of Lurie's books has to go through a huge amount of foundational material while the ideas themselves may not be intrinsically complicated. Instead, this complexity is an artifact of embedding the theory in current foundations like the SDG example mentioned above. With a new foundations, there is the possibility that we can teach the material at this level to students except that there are some tweaks in foundations.
  - spekcular 5y ago
    I don't have much to say here that I didn't already say above about the meta-mathematical issues. However, about object-level mathematical issues, you write: "It is a work in progress and might take some time before bearing substantive fruit, but note that the current alternative is that any student learning higher level mathematics at the level of Lurie's books has to go through a huge amount of foundational material while the ideas themselves may not be intrinsically complicated. Instead, this complexity is an artifact of embedding the theory in current foundations like the SDG example mentioned above." Higher category theory is not the same thing as homotopy type theory. One does not need to learn anything about the foundations of mathematics to read and understand Lurie's work. As far as I know, issues of ZFC vs type theory simply do not arise. You can just pick up Higher Topos Theory and start reading, assuming you have a strong background in algebraic topology. The linked article is only about higher category theory and making sure all of its claims are written down in a clear and rigorous fashion to be maximally useful to workers in the field. It has nothing to do with the foundations of mathematics as a whole.
- jules 5y ago
  ZFC is the x86 assembly language of foundations. Saying that ZFC is good enough because you can do all of mathematics in it is like saying that we don't need Java/Rust/Python because x86 assembly is good enough because x86 assembly is Turing complete. True, but that's missing the point of what people are trying to do with higher level languages. You can theoretically do everything you want in ZFC, but it's low level and a bit outdated and you don't actually want to write formal proofs in it. We know from experience that it is possible to translate the kinds of proofs that people do on paper into formal ZFC proofs, at least in theory. The mathematicians that study ZFC-like foundations are OK with that "in theory"-qualifier and are instead investigating the theoretical properties of the foundations. The goals of (homotopy) type theory are very different: they are trying to be suitable for actually doing modern mathematics in, and computer proof assistants are being developed that make it possible to actually write down formal proofs in them, in the form of proof code. For this to work it needs to be possible to translate all the kinds of arguments that mathematicians write down on paper into formal proof steps. It is not sufficient to remark that it is theoretically possible to find some kind of translation: it must actually be done for the computer to accept the validity, and the burden must not lie on the mathematician writing down the proof. Instead, the system must make it easy to write down the steps that the mathematician wants to do. One of the kinds of arguments that mathematicians use on paper is that if A is isomorphic to B, then a theorem about A automatically gives you a corresponding theorem about B. Homotopy type theory is trying to formally enable this kind of reasoning. In summary, the foundations people interested in ZFC have a very different goal than than the foundations people interested in (homotopy) type theory. The fact that the ZFC people are perfectly happy with ZFC and only care about ZFC doesn't mean much. The goals of the type theory people are not achieved by ZFC, not by a long shot. Note that it is not the case that the general body of mathematicians cares about ZFC and does not care about HoTT. They care neither about HoTT nor about ZFC. The nod to ZFC that mathematicians give when pressed is mere lip service; most mathematicians would not even be able to list the axioms of ZFC. Only foundations people care about ZFC, and the kind of foundations that the ZFC people care about is irrelevant to the practice of general mathematics.
  - lapinot 5y ago
    > ZFC is the x86 assembly language of foundations. > The goals of (homotopy) type theory are very different: they are trying to be suitable for actually doing modern mathematics > Only foundations people care about ZFC, and the kind of foundations that the ZFC people care about is irrelevant to the practice of general mathematics. Exactly this, thanks!
- anfelor 5y ago
  I agree with you that this is really about the foundations of algebraic topology, but what makes you say that these are not the foundations of mathematics? In the community of computer-aided formalization, a lot of interest in modern type theory arose, because some things in algebraic topology just couldn't easily be done in the old First-order-logic + ZFC framework: For example, Kevin Buzzard once asked if Isabelle/HOL (which even uses higher-order-logic) can even be used to formalize schemes! (It turns out that it is possible if you do it in a special way with locales... but the Lean formalization still seems more elegant). Of course, there is a consistency proof of Leans type theory using inaccessible cardinals, so the construction of schemes carries over to ZFC+large cardinals, but then it is not very understandable anymore. I agree with your point about HoTT not being useful to the algebraic topology community, but this seems orthogonal to its usefulness in formalization: I also would not expect Lean's type theory to be directly useful to working mathematicians. Instead it can make formalization easy or even possible: Even Jacob Lurie seems to acknowledge that it could be useful for that and only disputes that it does not bring new insights on an intuitive, informal level. My reading of the discussion is that some HoTT proponents see HoTT as a new language of mathematics (similar to category theory) and that Lurie does not believe that this perspective adds much, but that he does believe that one can use that perspective to understand the theorems. In the linked discussion Voevodsky points out that "Calculus of Inductive Constructions, the type theory that we currently using to formalize mathematics in the univalent style [and basically what Lean uses] is surprisingly convenient for doing mathematics at the level of sets and categories (and maybe 2-categories). As for mathematics of higher h-levels it is, in practice, of very little use. Note that this is a great advance of what was before as before we did not even have a system for doing abstract mathematics both formally and conveniently at the level of sets." [0] This highlights how crucial type theory is to do modern algebraic topology, even as he seems to claim that HoTT actually can not formalize Lurie's work? Still, he seems to agree that dependent type theories were a step in the right direction (unsurprisingly, since he founded HoTT) and that more work is needed for finding new foundations for mathematics. Indeed, the, as you write below, "mistaken belief that finding a new foundation of mathematics is an interesting project in the 21st century" is something that some people in foundations (and close to the Lean community) like Jeremy Avigad are actively pursuing: see e.g. https://arxiv.org/pdf/2009.09541.pdf https://arxiv.org/pdf/2009.09541.pdf [0]: https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-270 https://mathematicswithoutapologies.wordpress.com/2015/05/13...
isaac21259 5y ago
Curious how approachable you think homotopy type theory is to people who think they know better than researchers? Simple type systems would be understandable (Haskell has type systems similar to System F and rust has an affine your system) but if anything being a programmer may add obstacles to understand HoTT since programmers (generally) have never had the opportunity to learn topology or anything else that HoTT builds on. Also not everything in HoTT has a clear computational interpretation, notably the univalence axiom. That said I encourage everyone who's interested to investigate this but I don't think it's realistic without having a solid foundation in mathematics. (And I also agree with the sibling comment that HoTT isn't really used as a foundation of mathematics.)
- stepchowfun 5y ago
  I don't think it's an easy journey—not because the material is intrinsically difficult, but because almost all resources are written for mathematicians and computer scientists. I think a "homotopy type theory for programmers" book/blog/playlist could be a big hit. I've been considering putting something like that together. I view the relationship between HoTT and topology as similar to that of functional programming and category theory: you don't need to know the latter to learn the former, but having that extra background can certainly help.
  - isaac21259 5y ago
    I was also considering writing some introductory stuff about HoTT but I don't think it's possible to avoid talking about topology, homotopy theory, and category theory in depth like you can with, say Haskell and category theory. This is because the stuff that makes HoTT so cool cannot be separated from it's mathematical foundations. How would you explain truncated types without going fairly deep into the math? Or the circle type? Sure both of these could be explained as instances of higher inductive types but that explanation is missing a lot.
    - Koshkin 5y ago
      As already has been done with category theory, you need to target a specific audience, whether it is programmers, scientists, engineers, or mathematicians, and illustrate the concepts by giving examples from their area of expertise, if possible.
jimbob45 5y ago
[Deleted]
- stepchowfun 5y ago
  I see where you're coming from, but it's hard to appreciate the subtle issues surrounding the notion(s) of equality without actually investing some time into doing formal mathematics. My claim is that type theory is a good avenue to explore this subject matter, since you can check your work and get instant feedback with a type checker. Anyway, I sympathize with your sentiment that it can be hard to know whether something is worth learning without knowing if or how that knowledge will be useful to you. I feel that way about many topics myself.
rcshubhadeep 5y ago
A bit more context can be found here. It was very enjoyable as a video https://youtu.be/WLkMBMUk48E https://youtu.be/WLkMBMUk48E
momentoftop 5y ago
> You'll see why it's useful to have a formal justification for treating isomorphic objects as equal (this is called "univalence"), which is something you may have even been doing informally/subconsciously all along. Would you be able to discuss how this compares to quotienting? It sounds similar, but I assume has very important differences. I have, very formally, been doing quotienting. I identify an equivalence relation, quotient it, prove that the properties and operations of interest are well-defined when lifted to the equivalence classes, and then work exclusively at the level of the equivalence classes and the lifted operations. Say, when I work exclusively with reals, which are equivalence classes of Cauchy sequences, or with cosets in group theory.

spekcular 5y ago

This is not "foundational mathematics." This is about the foundations of algebraic topology. The experts in the foundations of mathematics as a whole (set theorists, logicians, model theorists, etc.) don't care about homotopy type theory. It's sort of pointless for the study of the foundations of mathematics. That is, they really just care about ZF or ZFC, because those are already formulated so that they are maximally useful for foundational investigations. (And the e.g. reverse mathematics people who want to work outside of ZF/ZFC already have more direct ways of doing so.) Some idea of what people in foundations think about day-to-day can be gleaned by searching the Foundations of Math mailing list archive: https://cs.nyu.edu/pipermail/fom/ https://cs.nyu.edu/pipermail/fom/ In particular: don't confuse higher category theory (of interest to the algebraic topology community at large) with homotopy type theory (which is not). Jacob Lurie has a rather pointed conversation with Urs Schreiber about this, linked to here: https://mathematicswithoutapologies.wordpress.com/2015/05/18/jacob-lurie-explains-and-elaborates-on-his-no-comment/ https://mathematicswithoutapologies.wordpress.com/2015/05/18.... edit: I'd love to hear from the downvoters why they disagree with this take. It's pretty standard, afaik.

zozbot234 5y ago
> I'd love to hear from the downvoters why they disagree with this take. It's pretty standard, afaik. Because it's obtuse. There are well-known ways of phrasing all of this stuff in set theory (or rather, "legitimate" varieties of set theory) should anyone really care, replicating type-theoretical constructions by adding increasingly large "inaccessible cardinals" to one's pre-existing notion of set. But it's a pointless exercise when the type-theoretical description of these foundations is so much easier to work with. It's only useful if one believes that "set theory" is the only legitimate language for talking about anything foundational, which is again quite silly.
- spekcular 5y ago
  In what sense is type theory "easier to work with"? For what purpose? ZFC exists largely because it's a useful framework for proving meta-mathematical theorems. In this sense, it is extremely convenient to work with. Also, I'm not sure what "all of this stuff" refers to here re: your comment about inaccessible cardinals. You don't need large cardinals to do 99.99% of modern mathematics (essentially, everything but set/proof theory). ZFC is good enough (and you can usually get away with something weaker).
  - Ericson2314 5y ago
    Frankly we are sick of set theorist traditionalists complaining about type theory, category theory, and other new things without actually bothering to understand them at all. After multiple decades, it's clear you all are never going to bother to learn our stuff nearly as well as we bothered to learn your stuff. This "debate" is thus completely unproductive without any good agreed-upon foundation to argue form. (How ironic!)
    - spekcular 5y ago
      First, I'm not a set theorist. Second, one of the major motivations for introducing type theory in mathematics was to assist with computer-aided formalization efforts, which has had some success and has a promising future (e.g. the stuff the Lean community has been doing lately). This is great! I'm not complaining at all. But I do think trumpeting HoTT as a new, improved foundation of mathematics evinces a misunderstanding of what people who work on foundations actually want out of a foundation of mathematics; or even more broadly, the mistaken belief that finding a new foundation of mathematics is an interesting project in the 21st century. Lurie's comment here explains a bit more: https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-299 https://mathematicswithoutapologies.wordpress.com/2015/05/13... (And clearly, Lurie is not some ignorant traditionalist. There's a substantive disagreement that can't be reduced to people not wanting to learn "your stuff.")
Twisol 5y ago
I've read rather too much of the fascinating comments thread you've indirectly linked to, but this nugget by Mike Shulman in that thread seems especially relevant to the present one: > If we distill it down from the categorical heights, this brings us back to John Baez’s pithy quote about equality: “Every interesting equation is a lie.” The only obviously true equation is x=x, but it carries no (or little) information. Any other equation, like x=y, is “a lie” because x and y are not the same thing; yet what is interesting about the equality is that they are nevertheless the same in some way. But knowing the equation doesn’t mean that we should forget all about y and use only x; the point of having the equation is that we can pass back and forth between x and y, according to which is most appropriate in any given context.
enugu 5y ago
Not downvoting,in particular there are useful links in your post. But note that by foundations one has atleast two different meanings. One meaning being examining the consistency of axioms or finding weakest set of axioms for a theorem. The other meaning being - finding a foundation in which a given mathematical theory is naturally and easily described, analogus to designing a programming language in which the programs are easy to describe. Most of the time in mathematics, this is done by defining high level concepts and working from there - no need to change the foundational axioms or rules of inference. But sometimes we need more - for instance, if you read the book "Synthetic Differential Geometry", infinitesimals are naturally embedded in the theory by working in a cartesian closed category of sets. One can either embed this in ZFC using cumbersome models, or change the logic itself(remove the law of excluded middle). The logic in HOTT deals with equality in a more careful way than the usual foundations. This is not restricted to algebraic topology alone - it certainly includes algebraic geometry and tackles a general issue which will plausibly have many more applications once the technology is available. The field of noncommutative geometry, in the style of Connes, is also about this as the problem of taking quotients is another way of the stating the issue with equality. It is a work in progress and might take some time before bearing substantive fruit, but note that the current alternative is that any student learning higher level mathematics at the level of Lurie's books has to go through a huge amount of foundational material while the ideas themselves may not be intrinsically complicated. Instead, this complexity is an artifact of embedding the theory in current foundations like the SDG example mentioned above. With a new foundations, there is the possibility that we can teach the material at this level to students except that there are some tweaks in foundations.
- spekcular 5y ago
  I don't have much to say here that I didn't already say above about the meta-mathematical issues. However, about object-level mathematical issues, you write: "It is a work in progress and might take some time before bearing substantive fruit, but note that the current alternative is that any student learning higher level mathematics at the level of Lurie's books has to go through a huge amount of foundational material while the ideas themselves may not be intrinsically complicated. Instead, this complexity is an artifact of embedding the theory in current foundations like the SDG example mentioned above." Higher category theory is not the same thing as homotopy type theory. One does not need to learn anything about the foundations of mathematics to read and understand Lurie's work. As far as I know, issues of ZFC vs type theory simply do not arise. You can just pick up Higher Topos Theory and start reading, assuming you have a strong background in algebraic topology. The linked article is only about higher category theory and making sure all of its claims are written down in a clear and rigorous fashion to be maximally useful to workers in the field. It has nothing to do with the foundations of mathematics as a whole.
jules 5y ago
ZFC is the x86 assembly language of foundations. Saying that ZFC is good enough because you can do all of mathematics in it is like saying that we don't need Java/Rust/Python because x86 assembly is good enough because x86 assembly is Turing complete. True, but that's missing the point of what people are trying to do with higher level languages. You can theoretically do everything you want in ZFC, but it's low level and a bit outdated and you don't actually want to write formal proofs in it. We know from experience that it is possible to translate the kinds of proofs that people do on paper into formal ZFC proofs, at least in theory. The mathematicians that study ZFC-like foundations are OK with that "in theory"-qualifier and are instead investigating the theoretical properties of the foundations. The goals of (homotopy) type theory are very different: they are trying to be suitable for actually doing modern mathematics in, and computer proof assistants are being developed that make it possible to actually write down formal proofs in them, in the form of proof code. For this to work it needs to be possible to translate all the kinds of arguments that mathematicians write down on paper into formal proof steps. It is not sufficient to remark that it is theoretically possible to find some kind of translation: it must actually be done for the computer to accept the validity, and the burden must not lie on the mathematician writing down the proof. Instead, the system must make it easy to write down the steps that the mathematician wants to do. One of the kinds of arguments that mathematicians use on paper is that if A is isomorphic to B, then a theorem about A automatically gives you a corresponding theorem about B. Homotopy type theory is trying to formally enable this kind of reasoning. In summary, the foundations people interested in ZFC have a very different goal than than the foundations people interested in (homotopy) type theory. The fact that the ZFC people are perfectly happy with ZFC and only care about ZFC doesn't mean much. The goals of the type theory people are not achieved by ZFC, not by a long shot. Note that it is not the case that the general body of mathematicians cares about ZFC and does not care about HoTT. They care neither about HoTT nor about ZFC. The nod to ZFC that mathematicians give when pressed is mere lip service; most mathematicians would not even be able to list the axioms of ZFC. Only foundations people care about ZFC, and the kind of foundations that the ZFC people care about is irrelevant to the practice of general mathematics.
- lapinot 5y ago
  > ZFC is the x86 assembly language of foundations. > The goals of (homotopy) type theory are very different: they are trying to be suitable for actually doing modern mathematics > Only foundations people care about ZFC, and the kind of foundations that the ZFC people care about is irrelevant to the practice of general mathematics. Exactly this, thanks!
anfelor 5y ago
I agree with you that this is really about the foundations of algebraic topology, but what makes you say that these are not the foundations of mathematics? In the community of computer-aided formalization, a lot of interest in modern type theory arose, because some things in algebraic topology just couldn't easily be done in the old First-order-logic + ZFC framework: For example, Kevin Buzzard once asked if Isabelle/HOL (which even uses higher-order-logic) can even be used to formalize schemes! (It turns out that it is possible if you do it in a special way with locales... but the Lean formalization still seems more elegant). Of course, there is a consistency proof of Leans type theory using inaccessible cardinals, so the construction of schemes carries over to ZFC+large cardinals, but then it is not very understandable anymore. I agree with your point about HoTT not being useful to the algebraic topology community, but this seems orthogonal to its usefulness in formalization: I also would not expect Lean's type theory to be directly useful to working mathematicians. Instead it can make formalization easy or even possible: Even Jacob Lurie seems to acknowledge that it could be useful for that and only disputes that it does not bring new insights on an intuitive, informal level. My reading of the discussion is that some HoTT proponents see HoTT as a new language of mathematics (similar to category theory) and that Lurie does not believe that this perspective adds much, but that he does believe that one can use that perspective to understand the theorems. In the linked discussion Voevodsky points out that "Calculus of Inductive Constructions, the type theory that we currently using to formalize mathematics in the univalent style [and basically what Lean uses] is surprisingly convenient for doing mathematics at the level of sets and categories (and maybe 2-categories). As for mathematics of higher h-levels it is, in practice, of very little use. Note that this is a great advance of what was before as before we did not even have a system for doing abstract mathematics both formally and conveniently at the level of sets." [0] This highlights how crucial type theory is to do modern algebraic topology, even as he seems to claim that HoTT actually can not formalize Lurie's work? Still, he seems to agree that dependent type theories were a step in the right direction (unsurprisingly, since he founded HoTT) and that more work is needed for finding new foundations for mathematics. Indeed, the, as you write below, "mistaken belief that finding a new foundation of mathematics is an interesting project in the 21st century" is something that some people in foundations (and close to the Lean community) like Jeremy Avigad are actively pursuing: see e.g. https://arxiv.org/pdf/2009.09541.pdf https://arxiv.org/pdf/2009.09541.pdf [0]: https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-270 https://mathematicswithoutapologies.wordpress.com/2015/05/13...

isaac21259 5y ago

Curious how approachable you think homotopy type theory is to people who think they know better than researchers? Simple type systems would be understandable (Haskell has type systems similar to System F and rust has an affine your system) but if anything being a programmer may add obstacles to understand HoTT since programmers (generally) have never had the opportunity to learn topology or anything else that HoTT builds on. Also not everything in HoTT has a clear computational interpretation, notably the univalence axiom. That said I encourage everyone who's interested to investigate this but I don't think it's realistic without having a solid foundation in mathematics. (And I also agree with the sibling comment that HoTT isn't really used as a foundation of mathematics.)

stepchowfun 5y ago
I don't think it's an easy journey—not because the material is intrinsically difficult, but because almost all resources are written for mathematicians and computer scientists. I think a "homotopy type theory for programmers" book/blog/playlist could be a big hit. I've been considering putting something like that together. I view the relationship between HoTT and topology as similar to that of functional programming and category theory: you don't need to know the latter to learn the former, but having that extra background can certainly help.
- isaac21259 5y ago
  I was also considering writing some introductory stuff about HoTT but I don't think it's possible to avoid talking about topology, homotopy theory, and category theory in depth like you can with, say Haskell and category theory. This is because the stuff that makes HoTT so cool cannot be separated from it's mathematical foundations. How would you explain truncated types without going fairly deep into the math? Or the circle type? Sure both of these could be explained as instances of higher inductive types but that explanation is missing a lot.
  - Koshkin 5y ago
    As already has been done with category theory, you need to target a specific audience, whether it is programmers, scientists, engineers, or mathematicians, and illustrate the concepts by giving examples from their area of expertise, if possible.

jimbob45 5y ago

[Deleted]

stepchowfun 5y ago
I see where you're coming from, but it's hard to appreciate the subtle issues surrounding the notion(s) of equality without actually investing some time into doing formal mathematics. My claim is that type theory is a good avenue to explore this subject matter, since you can check your work and get instant feedback with a type checker. Anyway, I sympathize with your sentiment that it can be hard to know whether something is worth learning without knowing if or how that knowledge will be useful to you. I feel that way about many topics myself.

rcshubhadeep 5y ago

A bit more context can be found here. It was very enjoyable as a video https://youtu.be/WLkMBMUk48E https://youtu.be/WLkMBMUk48E

momentoftop 5y ago

> You'll see why it's useful to have a formal justification for treating isomorphic objects as equal (this is called "univalence"), which is something you may have even been doing informally/subconsciously all along. Would you be able to discuss how this compares to quotienting? It sounds similar, but I assume has very important differences. I have, very formally, been doing quotienting. I identify an equivalence relation, quotient it, prove that the properties and operations of interest are well-defined when lifted to the equivalence classes, and then work exclusively at the level of the equivalence classes and the lifted operations. Say, when I work exclusively with reals, which are equivalence classes of Cauchy sequences, or with cosets in group theory.