6 ms·

Homotopy Type Theory and Higher Inductive Types

119 points by tw1010 9y ago

sigsergv 9y ago
This articly is quite hard to read and follow. I have some background in math but can't follow the logic in the article because author is constantly jumping from one topic to anonther. Artificial “questions” from imaginary layman are not helping, instead they confuse and dilute attention.
- aisofteng 9y ago
  I found it quite straightforward. There isn't any "jumping around".
- SolarNet 9y ago
  The questions are not the problem. They are a variation of the Socratic method and are super useful - when used correctly - for checking your understanding, and following where the author is going to go next. The problem is that the text is full of grammar, spelling, and punctuation errors. There are missing words, confusingly run on sentences, etc. It's an unnatural read because it hasn't had an editor.
amenghra 9y ago
https://www.cl.cam.ac.uk/~sd601/thesis.pdf https://www.cl.cam.ac.uk/~sd601/thesis.pdf might provide useful background reading for those who aren’t familiar with type theories.
danidiaz 9y ago
Introductory talk: "A Functional Programmer's Guide to Homotopy Type Theory" https://www.youtube.com/watch?v=caSOTjr1z18 https://www.youtube.com/watch?v=caSOTjr1z18
mathgenius 9y ago
Computerphile did some videos on voevodsky and homotopy type theory: https://www.youtube.com/watch?v=v5a5BYZwRx8 https://www.youtube.com/watch?v=v5a5BYZwRx8 (watch those eyes! I like how they bug out when he gets really excited.)
mbid 9y ago
In 2013, a consortium of the greatest mathematicians published a massive volume which reboots our conception of mathematics. Ok, here's a rant by a frustrated student who's spent way too much time drinking the cool-aid. None of the authors, except for Voevodsky, is widely known among professional mathematicians. And Voevodsky is not known because of his work on HoTT. In fact, most mathematicians regard homotopy type theory as some obscure stuff logicians and computer scientists do, with no relevance to their research. And they're most certainly right. "greatest mathematicians". Nobody would call a mathematician "great" for coming up with a definition. (No, Grothendieck is not an example, because he actually put his definitions to use and solved hard problems.) Yet there are no interesting theorems proved via the univalence axiom which weren't known before. Thus, the "greatest" mathematical achievement of the HoTT community seems to have been coming up with the univalence axiom. Everybody can come up with random axioms. Thus, I'd say their greatest accomplishment is not actually mathematical but social, because they managed to market this "breakthrough" the way it has been. The whole process of how type theory research seems to work is completely absurd. Type theorists first create a syntax and later come up with a semantics for it. In other words, they first think about how they want to say something before they even know what to say. For example, the semantics of dependent Per Martin-Löf type theory were developed only 10-15 years after Martin-Löf came up with his syntax. A few years ago, somebody finally published a proof that the semantics of extensional Martin-Löf type theory is equivalent to locally cartesian closed categories (lccc's). It's not hard to understand what an lccc is, and state their defining operations/axioms. lcccs pop up everywhere. The concept of dependent types, on the other hand, has not existed in mathematics for thousands of years, seemingly without causing any harm. Nobody gained any interesting new insights by understanding dependent types, to my knowledge. Why, exactly, is this awkward axiomatization of lcccs interesting? And the same happens for intensional type theory with the univalence axiom. It's been blurted out for years that this syntax's semantics should be equivalent to infinity lcccs. Yet there is still no proof, no evidence that HoTT is the easiest axiomatization or the easiest to work with, and a proof, if it exists, will likely be extremely convoluted because it has to deal with all the peculiarities of a syntax that was created without having infinity categories in mind. A language that makes it hard to understand what it means has failed. If you don't believe me (and there is now reason why you should), please read this thread [1]. Lurie, the expert on infinity categories (well, there are others, but he's written the canonical tome), debates with type theorists about the usefulness of HoTT. I believe it ends with Lurie not seeing any usefulness and calling it a day. [1] https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment https://mathematicswithoutapologies.wordpress.com/2015/05/13...
mathgenius 9y ago
> I mean, when you actually use integers, do you really picture them as equivalence classes of the Cartesian square of natural numbers? Yes, accountants really do think of integers this way: these are assets and liabilities.
auggierose 9y ago
I really wish somebody could explain the Univalence axiom to me. Without assuming that I know category theory or algebraic topology. You know, just like you can explain the axioms of set theory pretty easily. I mean, if it is a foundation, there should be an easy way to explain it. And not in metaphors, please, but in a precise way.
- Koshkin 9y ago
  I doubt that it can be explained in less than fifteen pages. https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf
  - auggierose 9y ago
    Well, it is a start. Fourteen pages anyone? Once we are down to five pages I'll give it a(nother) shot.
    - agumonkey 9y ago
      you should read it, it's an easy one, at least it's how I feel after reading 3 pages (usually I stop long before that)
      - dvt 9y ago
        It's not bad, but man the way the author throws around multivariate (e.g. non-curried) functions all over the place is sooo confusing. I remember reading a λ-calculus book that would do that and it's really not fun to try and parse (see the bottom of pg. 7). But I will say it's very cool to see how HoTT derives all the basic tools you'd use in propositional calculus (A: A -> A, :(A -> (B -> C)) -> ((A->B) -> (A->C)), and so on).
    - oneestrong 9y ago
      In example 2.2, to distinguish between an element and a function a better example is to consider a constant such as 7 can be an element of R or a constant function. With type theory notation, 1:R versus \x:R.1, another important point is that you have to specify the arity of the function, so that 1:R, \(x:R).1, \(x:R,y:R).1, \(x:C,y:C).1 are four different types, the first a constant, the second a constant function of one real variable, and the last a function of arity two whose variable type is the C the complex field. I'm reading page four, perhaps type theory can distinguish among pure function, lazy functions, side-effect functions and other types of functions that are implemented by a procedure which can be lazy or not. So pi:R,(\x:R.pi) and (\x:Haskell-Action()).pi in which the last is a non pure lazy program for computing all digits of pi, are two different types, that is they belong to different universes.

119 points by tw1010 9y ago

This articly is quite hard to read and follow. I have some background in math but can't follow the logic in the article because author is constantly jumping from one topic to anonther. Artificial “questions” from imaginary layman are not helping, instead they confuse and dilute attention.

aisofteng 9y ago
I found it quite straightforward. There isn't any "jumping around".
SolarNet 9y ago
The questions are not the problem. They are a variation of the Socratic method and are super useful - when used correctly - for checking your understanding, and following where the author is going to go next. The problem is that the text is full of grammar, spelling, and punctuation errors. There are missing words, confusingly run on sentences, etc. It's an unnatural read because it hasn't had an editor.

amenghra 9y ago

https://www.cl.cam.ac.uk/~sd601/thesis.pdf https://www.cl.cam.ac.uk/~sd601/thesis.pdf might provide useful background reading for those who aren’t familiar with type theories.

danidiaz 9y ago

Introductory talk: "A Functional Programmer's Guide to Homotopy Type Theory" https://www.youtube.com/watch?v=caSOTjr1z18 https://www.youtube.com/watch?v=caSOTjr1z18

mathgenius 9y ago

Computerphile did some videos on voevodsky and homotopy type theory: https://www.youtube.com/watch?v=v5a5BYZwRx8 https://www.youtube.com/watch?v=v5a5BYZwRx8 (watch those eyes! I like how they bug out when he gets really excited.)

mbid 9y ago

In 2013, a consortium of the greatest mathematicians published a massive volume which reboots our conception of mathematics. Ok, here's a rant by a frustrated student who's spent way too much time drinking the cool-aid. None of the authors, except for Voevodsky, is widely known among professional mathematicians. And Voevodsky is not known because of his work on HoTT. In fact, most mathematicians regard homotopy type theory as some obscure stuff logicians and computer scientists do, with no relevance to their research. And they're most certainly right. "greatest mathematicians". Nobody would call a mathematician "great" for coming up with a definition. (No, Grothendieck is not an example, because he actually put his definitions to use and solved hard problems.) Yet there are no interesting theorems proved via the univalence axiom which weren't known before. Thus, the "greatest" mathematical achievement of the HoTT community seems to have been coming up with the univalence axiom. Everybody can come up with random axioms. Thus, I'd say their greatest accomplishment is not actually mathematical but social, because they managed to market this "breakthrough" the way it has been. The whole process of how type theory research seems to work is completely absurd. Type theorists first create a syntax and later come up with a semantics for it. In other words, they first think about how they want to say something before they even know what to say. For example, the semantics of dependent Per Martin-Löf type theory were developed only 10-15 years after Martin-Löf came up with his syntax. A few years ago, somebody finally published a proof that the semantics of extensional Martin-Löf type theory is equivalent to locally cartesian closed categories (lccc's). It's not hard to understand what an lccc is, and state their defining operations/axioms. lcccs pop up everywhere. The concept of dependent types, on the other hand, has not existed in mathematics for thousands of years, seemingly without causing any harm. Nobody gained any interesting new insights by understanding dependent types, to my knowledge. Why, exactly, is this awkward axiomatization of lcccs interesting? And the same happens for intensional type theory with the univalence axiom. It's been blurted out for years that this syntax's semantics should be equivalent to infinity lcccs. Yet there is still no proof, no evidence that HoTT is the easiest axiomatization or the easiest to work with, and a proof, if it exists, will likely be extremely convoluted because it has to deal with all the peculiarities of a syntax that was created without having infinity categories in mind. A language that makes it hard to understand what it means has failed. If you don't believe me (and there is now reason why you should), please read this thread [1]. Lurie, the expert on infinity categories (well, there are others, but he's written the canonical tome), debates with type theorists about the usefulness of HoTT. I believe it ends with Lurie not seeing any usefulness and calling it a day. [1] https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment https://mathematicswithoutapologies.wordpress.com/2015/05/13...

mathgenius 9y ago

> I mean, when you actually use integers, do you really picture them as equivalence classes of the Cartesian square of natural numbers? Yes, accountants really do think of integers this way: these are assets and liabilities.

auggierose 9y ago

I really wish somebody could explain the Univalence axiom to me. Without assuming that I know category theory or algebraic topology. You know, just like you can explain the axioms of set theory pretty easily. I mean, if it is a foundation, there should be an easy way to explain it. And not in metaphors, please, but in a precise way.

Koshkin 9y ago
I doubt that it can be explained in less than fifteen pages. https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf
- auggierose 9y ago
  Well, it is a start. Fourteen pages anyone? Once we are down to five pages I'll give it a(nother) shot.
  - agumonkey 9y ago
    you should read it, it's an easy one, at least it's how I feel after reading 3 pages (usually I stop long before that)
    - dvt 9y ago
      It's not bad, but man the way the author throws around multivariate (e.g. non-curried) functions all over the place is sooo confusing. I remember reading a λ-calculus book that would do that and it's really not fun to try and parse (see the bottom of pg. 7). But I will say it's very cool to see how HoTT derives all the basic tools you'd use in propositional calculus (A: A -> A, :(A -> (B -> C)) -> ((A->B) -> (A->C)), and so on).
  - oneestrong 9y ago
    In example 2.2, to distinguish between an element and a function a better example is to consider a constant such as 7 can be an element of R or a constant function. With type theory notation, 1:R versus \x:R.1, another important point is that you have to specify the arity of the function, so that 1:R, \(x:R).1, \(x:R,y:R).1, \(x:C,y:C).1 are four different types, the first a constant, the second a constant function of one real variable, and the last a function of arity two whose variable type is the C the complex field. I'm reading page four, perhaps type theory can distinguish among pure function, lazy functions, side-effect functions and other types of functions that are implemented by a procedure which can be lazy or not. So pi:R,(\x:R.pi) and (\x:Haskell-Action()).pi in which the last is a non pure lazy program for computing all digits of pi, are two different types, that is they belong to different universes.