6 ms·

You raise a couple of important points. I agree that "a consortium of the greatest mathematicians" is a bit of a hyperbole, even though many of the contributors

You raise a couple of important points. I agree that "a consortium of the greatest mathematicians" is a bit of a hyperbole, even though many of the contributors to the HoTT book are extremely well-known in their areas of research, eaching listing numerous worthwhile contributions. Let me react to some of your statements more precisely. "In fact, most mathematicians regard homotopy type theory as some obscure stuff logicians and computer scientists do, with no relevance to their research." For the most part, any two mathematicians working on different subjects won't believe that each other's work is relevant to them. "Everybody can come up with random axioms." This is of course true, on face value, but the point of the univalence axiom is that it is firstly an extremely interesting axiom, secondly that it's an eminently practical axiom (vastly simplifying formal proofs in some areas), and thirdly that it's actually fulfilled in several models. "The concept of dependent types, on the other hand, has not existed in mathematics for thousands of years, seemingly without causing any harm." While dependent types were only made explicit in Martin-Löf's type theory in the 1970s, dependent types pop up everywhere. For instance the type of vectors of length n is a dependent type (dependent on the value n). "Why, exactly, is this awkward axiomatization of lcccs interesting?" It's because it's so simple to work syntactically. Just as informal proofs (written in English or a different human language) can be (in principle) be translated to formal proofs in ZFC or a different set theory, with a small bit of training you can recognize when an informal proof can be translated to extensional Martin-Löf type theory. In this way a single piece of informal proof gives rise to a multitude of theorems, one for each lccc. "and a proof, if it exists, will likely be extremely convoluted" Partly, this is exactly the point! The language of homotopy type theory makes it easy to work with infinity categories. By now the correspondence has been checked in many cases. In particular, the correspondence has always been known for the model of simplicial sets (which was, in fact, Voevodsky's starting point). Thus from the very beginning, we were able to use HoTT as a convenient synthetic language for doing algebraic topology. The thread you linked to is full of interesting food for thought. Be sure to also check out Mike Shulman's comments there! I'm happy to discuss this further. :-)

mbid 9y ago
Hi Ingo, I'm pleasantly surprised to see an actual researcher here. For the most part, any two mathematicians working on different subjects won't believe that each other's work is relevant to them. This is somewhat true, but I think reasearch in type theory is connected to that in other branches of mathematics (if you want to call type theory maths) very weakly in comparison. There are some connections to category theory, but they are far to weak given that type theory should essentially be a branch of categorical logic -- the one that deals with the initial so-and-so category and its computational properties. The point of the univalence axiom is that it is firstly an extremely interesting axiom I agree that the underlying ideas are interesting. But I think it's much clearer to see what's going on if you know what an object classifier is. Can't say much about the rest. I mean, yeah, it's of course true that the univalence axiom is not just a randomly generated formula, and people have thought hard about it. For instance the type of vectors of length n is a dependent type (dependent on the value n)." What do you gain in comparison to "a vector of length n is a vector such that its length is equal to n"? "Why, exactly, is this awkward axiomatization of lcccs interesting?" It's because it's so simple to work syntactically. Just as informal proofs (written in English or a different human language) can be (in principle) be translated to formal proofs in ZFC or a different set theory, with a small bit of training you can recognize when an informal proof can be translated to extensional Martin-Löf type theory. In this way a single piece of informal proof gives rise to a multitude of theorems, one for each lccc. I agree with your last sentence strongly, but I don't think you need type theory to do that. Why can't you translate your informal proof into any other, possibly more convenient or intuitive syntax instead? Wouldn't it be incredibly random if intensional type theory, which was not defined as a syntax for infinity lccc at all, be the best way to do this? At one point in the discussion I've linked to, Shulman explains the type theoretic proof for "the fundamental group of S^1 is Z", as presented in the HoTT book I believe. Lurie is of course not impressed, because the proof is also not hard to do for infinity toposes and basically the same if you know what an object classifier does and what the circle is. So to somebody like Lurie, formalizing things in type theory means translating his intuition to type theory and feeding it to a computer. If he read a theorem formalized in type theory, he'd have to translate it back to infinity category theory again. "and a proof, if it exists, will likely be extremely convoluted" Partly, this is exactly the point! The language of homotopy type theory makes it easy to work with infinity categories. By now the correspondence has been checked in many cases. In particular, the correspondence has always been known for the model of simplicial sets (which was, in fact, Voevodsky's starting point). Thus from the very beginning, we were able to use HoTT as a convenient synthetic language for doing algebraic topology. I agree that there may be value in finding more "rigid", equivalent ways to define infinity categories. For example, simplicially enriched categories instead of simplicial sets. But that intensional type theory is the right trade-off to be made (without making type checking impossible) would be extremely surprising to me.

mbid 9y ago

Hi Ingo, I'm pleasantly surprised to see an actual researcher here. For the most part, any two mathematicians working on different subjects won't believe that each other's work is relevant to them. This is somewhat true, but I think reasearch in type theory is connected to that in other branches of mathematics (if you want to call type theory maths) very weakly in comparison. There are some connections to category theory, but they are far to weak given that type theory should essentially be a branch of categorical logic -- the one that deals with the initial so-and-so category and its computational properties. The point of the univalence axiom is that it is firstly an extremely interesting axiom I agree that the underlying ideas are interesting. But I think it's much clearer to see what's going on if you know what an object classifier is. Can't say much about the rest. I mean, yeah, it's of course true that the univalence axiom is not just a randomly generated formula, and people have thought hard about it. For instance the type of vectors of length n is a dependent type (dependent on the value n)." What do you gain in comparison to "a vector of length n is a vector such that its length is equal to n"? "Why, exactly, is this awkward axiomatization of lcccs interesting?" It's because it's so simple to work syntactically. Just as informal proofs (written in English or a different human language) can be (in principle) be translated to formal proofs in ZFC or a different set theory, with a small bit of training you can recognize when an informal proof can be translated to extensional Martin-Löf type theory. In this way a single piece of informal proof gives rise to a multitude of theorems, one for each lccc. I agree with your last sentence strongly, but I don't think you need type theory to do that. Why can't you translate your informal proof into any other, possibly more convenient or intuitive syntax instead? Wouldn't it be incredibly random if intensional type theory, which was not defined as a syntax for infinity lccc at all, be the best way to do this? At one point in the discussion I've linked to, Shulman explains the type theoretic proof for "the fundamental group of S^1 is Z", as presented in the HoTT book I believe. Lurie is of course not impressed, because the proof is also not hard to do for infinity toposes and basically the same if you know what an object classifier does and what the circle is. So to somebody like Lurie, formalizing things in type theory means translating his intuition to type theory and feeding it to a computer. If he read a theorem formalized in type theory, he'd have to translate it back to infinity category theory again. "and a proof, if it exists, will likely be extremely convoluted" Partly, this is exactly the point! The language of homotopy type theory makes it easy to work with infinity categories. By now the correspondence has been checked in many cases. In particular, the correspondence has always been known for the model of simplicial sets (which was, in fact, Voevodsky's starting point). Thus from the very beginning, we were able to use HoTT as a convenient synthetic language for doing algebraic topology. I agree that there may be value in finding more "rigid", equivalent ways to define infinity categories. For example, simplicially enriched categories instead of simplicial sets. But that intensional type theory is the right trade-off to be made (without making type checking impossible) would be extremely surprising to me.