*[HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?@ 2019-10-27 14:41 Nicolas Alexander Schmidt2019-10-27 17:22 ` Bas Spitters 2019-11-03 7:29 ` Michael Shulman 0 siblings, 2 replies; 32+ messages in thread From: Nicolas Alexander Schmidt @ 2019-10-27 14:41 UTC (permalink / raw) To: Homotopy Type Theory In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 talk at IAS, Voevodsky talks about the history of his project of "univalent mathematics" and his motivation for starting it. Namely, he mentions that he found existing proof assistants at that time (in 2000) to be impractical for the kinds of mathematics he was interested in. Unfortunately, he doesn't go into details of what mathematics he was exactly interested in (I'm guessing something to do with homotopy theory) or why exactly existing proof assistants weren't practical for formalizing them. Judging by the things he mentions in his talk, it seems that (roughly) his rejection of those proof assistants was based on the view that predicate logic + ZFC is not expressive enough. In other words, there is too much lossy encoding needed in order to translate from the platonic world of mathematical ideas to this formal language. Comparing the situation to computer programming languages, one might say that predicate logic is like Assembly in that even though everything can be encoded in that language, it is not expressive enough to directly talk about higher level concepts, diminishing its practical value for reasoning about mathematics. In particular, those systems are not adequate for *interactive* development of *new* mathematics (as opposed to formalization of existing theories). Perhaps I am just misinterpreting what Voevodsky said. In this case, I hope someone can correct me. However even if this wasn't *his* view, to me it seems to be a view held implicitly in the HoTT community. In any case, it's a view that one might reasonably hold. However I wonder how reasonable that view actually is, i.e. whether e.g. Mizar really is that much more impractical than HoTT-Coq or Agda, given that people have been happily formalizing mathematics in it for 46 years now. And, even though by browsing the contents of "Formalized Mathematics" one can get the impression that the work consists mostly of formalizing early 20th century mathematics, neither the UniMath nor the HoTT library for example contain a proof of Fubini's theorem. So, to put this into one concrete question, how (if at all) is HoTT-Coq more practical than Mizar for the purpose of formalizing mathematics, outside the specific realm of synthetic homotopy theory? -- Nicolas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz. ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-10-27 14:41 [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Nicolas Alexander Schmidt@ 2019-10-27 17:22 ` Bas Spitters2019-11-03 11:38 ` Bas Spitters 2019-11-03 7:29 ` Michael Shulman 1 sibling, 1 reply; 32+ messages in thread From: Bas Spitters @ 2019-10-27 17:22 UTC (permalink / raw) To: Nicolas Alexander Schmidt;+Cc:Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 3429 bytes --] I believe it refers to his 2-theories: https://www.ias.edu/ideas/2014/voevodsky-origins On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt < zero@fromzerotoinfinity.xyz> wrote: > In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 talk > at IAS, Voevodsky talks about the history of his project of "univalent > mathematics" and his motivation for starting it. Namely, he mentions > that he found existing proof assistants at that time (in 2000) to be > impractical for the kinds of mathematics he was interested in. > > Unfortunately, he doesn't go into details of what mathematics he was > exactly interested in (I'm guessing something to do with homotopy > theory) or why exactly existing proof assistants weren't practical for > formalizing them. Judging by the things he mentions in his talk, it > seems that (roughly) his rejection of those proof assistants was based > on the view that predicate logic + ZFC is not expressive enough. In > other words, there is too much lossy encoding needed in order to > translate from the platonic world of mathematical ideas to this formal > language. > > Comparing the situation to computer programming languages, one might say > that predicate logic is like Assembly in that even though everything can > be encoded in that language, it is not expressive enough to directly > talk about higher level concepts, diminishing its practical value for > reasoning about mathematics. In particular, those systems are not > adequate for *interactive* development of *new* mathematics (as opposed > to formalization of existing theories). > > Perhaps I am just misinterpreting what Voevodsky said. In this case, I > hope someone can correct me. However even if this wasn't *his* view, to > me it seems to be a view held implicitly in the HoTT community. In any > case, it's a view that one might reasonably hold. > > However I wonder how reasonable that view actually is, i.e. whether e.g. > Mizar really is that much more impractical than HoTT-Coq or Agda, given > that people have been happily formalizing mathematics in it for 46 years > now. And, even though by browsing the contents of "Formalized > Mathematics" one can get the impression that the work consists mostly of > formalizing early 20th century mathematics, neither the UniMath nor the > HoTT library for example contain a proof of Fubini's theorem. > > So, to put this into one concrete question, how (if at all) is HoTT-Coq > more practical than Mizar for the purpose of formalizing mathematics, > outside the specific realm of synthetic homotopy theory? > > > -- > > Nicolas > > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuTfkp%3DPNeYE8bpO20APnTBdpzqJNfUekE5ECrr0vD5cww%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 4657 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-10-27 14:41 [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Nicolas Alexander Schmidt 2019-10-27 17:22 ` Bas Spitters@ 2019-11-03 7:29 ` Michael Shulman1 sibling, 0 replies; 32+ messages in thread From: Michael Shulman @ 2019-11-03 7:29 UTC (permalink / raw) To: Nicolas Alexander Schmidt;+Cc:Homotopy Type Theory I know hardly anything about Mizar, so I can't comment on it. And I don't know for sure exactly what Voevodsky meant (and perhaps no one now does). But I am pretty sure that he was not thinking about synthetic homotopy theory at the time, because the possibility of synthetic homotopy theory wasn't really even imagined until later on (specifically, with the advent of higher inductive types). Instead, I expect he was thinking about category theory and higher category theory. The advantage of univalence in such contexts is that it formalizes the isomorphism-invariant behavior of category theory, incorporating it directly into the logical structure of the foundations so that you don't have to worry about whether your theorems are invariant under isomorphism, or prove explicitly that they are. Is this a substantial advantage over a ZFC-based system? Maybe, maybe not. (One might argue that it's not much of an advantage at all until univalence becomes "computational", as with cubical type theories, so that transporting along it can be done automatically by the proof assistant.) But there are other points to consider. Firstly, before even getting to univalence, there is a difference between membership-based set theories and type theories, which is more closely analogous to the assembly language / high level programming language divide. Type-theoretic foundations for mathematics, like strongly/statically typed programming languages, provide automatic "error-checking" for the user, catching various kinds of mistakes at "compile time", and allow more intelligent compiler optimization and inference due to the more informative nature of types. Dependent type theories are even better at this. And just as the advantages of static typing are not belied by the fact that a lot of people happily write code in dynamically typed languages, so the advantages of typed mathematics for formalization are not belied by the fact that some mathematicians are happy to do without them. It's worth noting that many of the recent high-profile formalizations of *recent* mathematical results, such as the four-color theorem, the odd-order theorem, and the Kepler conjecture, use type-theoretic proof assistants like Coq and HOL rather than set-theoretic ones like Mizar. From this perspective, the advantage of HoTT/UF is that it "fixes" certain infelicities in previously existing type theories. Now we understand quotients better and have more tools for doing without setoids; now we know what the equality type of the universe is; now we are better at computing with function extensionality and propositional extensionality; etc. So HoTT/UF gives us the benefits of a type-theoretic foundation while ameliorating some of the traditional disadvantages of that approach. But in my own opinion (which is, I believe, rather different from Voevodsky's, at least in emphasis), all of this is kind of beside the point. It's like arguing about whether or not my laptop can play movies better than an 80s-era VCR; it overlooks the main point that my laptop does *so much more* than just play movies. The real advantage of type-theoretic, and homotopy-type-theoretic, foundations, is that they have a plethora of categorical and higher-categorical models. Proving a theorem once, in constructive homotopy type theory, automatically entails the "internal" truth of the corresponding theorem in all higher toposes. I think this is a much more important selling point than whether or not we get a more practical system for formalizing plain old set-based mathematics. Mike On Sun, Oct 27, 2019 at 7:41 AM Nicolas Alexander Schmidt <zero@fromzerotoinfinity.xyz> wrote: > > In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 talk > at IAS, Voevodsky talks about the history of his project of "univalent > mathematics" and his motivation for starting it. Namely, he mentions > that he found existing proof assistants at that time (in 2000) to be > impractical for the kinds of mathematics he was interested in. > > Unfortunately, he doesn't go into details of what mathematics he was > exactly interested in (I'm guessing something to do with homotopy > theory) or why exactly existing proof assistants weren't practical for > formalizing them. Judging by the things he mentions in his talk, it > seems that (roughly) his rejection of those proof assistants was based > on the view that predicate logic + ZFC is not expressive enough. In > other words, there is too much lossy encoding needed in order to > translate from the platonic world of mathematical ideas to this formal > language. > > Comparing the situation to computer programming languages, one might say > that predicate logic is like Assembly in that even though everything can > be encoded in that language, it is not expressive enough to directly > talk about higher level concepts, diminishing its practical value for > reasoning about mathematics. In particular, those systems are not > adequate for *interactive* development of *new* mathematics (as opposed > to formalization of existing theories). > > Perhaps I am just misinterpreting what Voevodsky said. In this case, I > hope someone can correct me. However even if this wasn't *his* view, to > me it seems to be a view held implicitly in the HoTT community. In any > case, it's a view that one might reasonably hold. > > However I wonder how reasonable that view actually is, i.e. whether e.g. > Mizar really is that much more impractical than HoTT-Coq or Agda, given > that people have been happily formalizing mathematics in it for 46 years > now. And, even though by browsing the contents of "Formalized > Mathematics" one can get the impression that the work consists mostly of > formalizing early 20th century mathematics, neither the UniMath nor the > HoTT library for example contain a proof of Fubini's theorem. > > So, to put this into one concrete question, how (if at all) is HoTT-Coq > more practical than Mizar for the purpose of formalizing mathematics, > outside the specific realm of synthetic homotopy theory? > > > -- > > Nicolas > > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQxVHxFhGzoSvMU9iw5_z9kgjD7w3c_VEYX5ANH-mOS_0g%40mail.gmail.com. ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-10-27 17:22 ` Bas Spitters@ 2019-11-03 11:38 ` Bas Spitters2019-11-03 11:52 ` David Roberts 0 siblings, 1 reply; 32+ messages in thread From: Bas Spitters @ 2019-11-03 11:38 UTC (permalink / raw) To: Nicolas Alexander Schmidt;+Cc:Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 3752 bytes --] There's also VV homotopy lambda calculus, which he later abandoned for MLTT: https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters <b.a.w.spitters@gmail.com> wrote: > I believe it refers to his 2-theories: > https://www.ias.edu/ideas/2014/voevodsky-origins > > On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt < > zero@fromzerotoinfinity.xyz> wrote: > >> In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 talk >> at IAS, Voevodsky talks about the history of his project of "univalent >> mathematics" and his motivation for starting it. Namely, he mentions >> that he found existing proof assistants at that time (in 2000) to be >> impractical for the kinds of mathematics he was interested in. >> >> Unfortunately, he doesn't go into details of what mathematics he was >> exactly interested in (I'm guessing something to do with homotopy >> theory) or why exactly existing proof assistants weren't practical for >> formalizing them. Judging by the things he mentions in his talk, it >> seems that (roughly) his rejection of those proof assistants was based >> on the view that predicate logic + ZFC is not expressive enough. In >> other words, there is too much lossy encoding needed in order to >> translate from the platonic world of mathematical ideas to this formal >> language. >> >> Comparing the situation to computer programming languages, one might say >> that predicate logic is like Assembly in that even though everything can >> be encoded in that language, it is not expressive enough to directly >> talk about higher level concepts, diminishing its practical value for >> reasoning about mathematics. In particular, those systems are not >> adequate for *interactive* development of *new* mathematics (as opposed >> to formalization of existing theories). >> >> Perhaps I am just misinterpreting what Voevodsky said. In this case, I >> hope someone can correct me. However even if this wasn't *his* view, to >> me it seems to be a view held implicitly in the HoTT community. In any >> case, it's a view that one might reasonably hold. >> >> However I wonder how reasonable that view actually is, i.e. whether e.g. >> Mizar really is that much more impractical than HoTT-Coq or Agda, given >> that people have been happily formalizing mathematics in it for 46 years >> now. And, even though by browsing the contents of "Formalized >> Mathematics" one can get the impression that the work consists mostly of >> formalizing early 20th century mathematics, neither the UniMath nor the >> HoTT library for example contain a proof of Fubini's theorem. >> >> So, to put this into one concrete question, how (if at all) is HoTT-Coq >> more practical than Mizar for the purpose of formalizing mathematics, >> outside the specific realm of synthetic homotopy theory? >> >> >> -- >> >> Nicolas >> >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz >> . >> > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 5364 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-03 11:38 ` Bas Spitters@ 2019-11-03 11:52 ` David Roberts2019-11-03 19:13 ` Michael Shulman 0 siblings, 1 reply; 32+ messages in thread From: David Roberts @ 2019-11-03 11:52 UTC (permalink / raw) To: Bas Spitters, homotopytypetheory;+Cc:Nicolas Alexander Schmidt [-- Attachment #1: Type: text/plain, Size: 4939 bytes --] Forget even higher category theory. Kevin Buzzard now goes around telling the story of how even formally proving (using Lean) things in rather elementary commutative algebra from EGA that are stated as equalities was not obvious: the equality is really an isomorphism arising from a universal property. Forget trying to do anything motivic, when algebra is full of such equalities. This is not a problem with univalence, of course. David On Sun, 3 Nov 2019, 10:08 PM Bas Spitters <b.a.w.spitters@gmail.com> wrote: > There's also VV homotopy lambda calculus, which he later abandoned for > MLTT: > > https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf > > On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters <b.a.w.spitters@gmail.com> > wrote: > >> I believe it refers to his 2-theories: >> https://www.ias.edu/ideas/2014/voevodsky-origins >> >> On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt < >> zero@fromzerotoinfinity.xyz> wrote: >> >>> In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 talk >>> at IAS, Voevodsky talks about the history of his project of "univalent >>> mathematics" and his motivation for starting it. Namely, he mentions >>> that he found existing proof assistants at that time (in 2000) to be >>> impractical for the kinds of mathematics he was interested in. >>> >>> Unfortunately, he doesn't go into details of what mathematics he was >>> exactly interested in (I'm guessing something to do with homotopy >>> theory) or why exactly existing proof assistants weren't practical for >>> formalizing them. Judging by the things he mentions in his talk, it >>> seems that (roughly) his rejection of those proof assistants was based >>> on the view that predicate logic + ZFC is not expressive enough. In >>> other words, there is too much lossy encoding needed in order to >>> translate from the platonic world of mathematical ideas to this formal >>> language. >>> >>> Comparing the situation to computer programming languages, one might say >>> that predicate logic is like Assembly in that even though everything can >>> be encoded in that language, it is not expressive enough to directly >>> talk about higher level concepts, diminishing its practical value for >>> reasoning about mathematics. In particular, those systems are not >>> adequate for *interactive* development of *new* mathematics (as opposed >>> to formalization of existing theories). >>> >>> Perhaps I am just misinterpreting what Voevodsky said. In this case, I >>> hope someone can correct me. However even if this wasn't *his* view, to >>> me it seems to be a view held implicitly in the HoTT community. In any >>> case, it's a view that one might reasonably hold. >>> >>> However I wonder how reasonable that view actually is, i.e. whether e.g. >>> Mizar really is that much more impractical than HoTT-Coq or Agda, given >>> that people have been happily formalizing mathematics in it for 46 years >>> now. And, even though by browsing the contents of "Formalized >>> Mathematics" one can get the impression that the work consists mostly of >>> formalizing early 20th century mathematics, neither the UniMath nor the >>> HoTT library for example contain a proof of Fubini's theorem. >>> >>> So, to put this into one concrete question, how (if at all) is HoTT-Coq >>> more practical than Mizar for the purpose of formalizing mathematics, >>> outside the specific realm of synthetic homotopy theory? >>> >>> >>> -- >>> >>> Nicolas >>> >>> >>> -- >>> You received this message because you are subscribed to the Google >>> Groups "Homotopy Type Theory" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz >>> . >>> >> -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS16Vy7sGiEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 7151 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-03 11:52 ` David Roberts@ 2019-11-03 19:13 ` Michael Shulman2019-11-03 19:45 ` Valery Isaev 2019-11-04 18:42 ` Kevin Buzzard 0 siblings, 2 replies; 32+ messages in thread From: Michael Shulman @ 2019-11-03 19:13 UTC (permalink / raw) To: David Roberts;+Cc:Bas Spitters, homotopytypetheory, Nicolas Alexander Schmidt But does univalence a la Book HoTT *actually* make it easier to reason about such things? It allows us to write "=" rather than "\cong", but to construct such an equality we have to construct an isomorphism first, and to *use* such an equality we have to transport along it, and then we get lots of univalence-redexes that we have to manually reduce away. My experience formalizing math in HoTT/Coq is that it's much easier if you *avoid* turning equivalences into equalities except when absolutely necessary. (I don't have any experience formalizing math in a cubical proof assistant, but in that case at least you wouldn't have to manually reduce the univalence-redexes -- although it seems to me you'd still have to construct the isomorphism before you can apply univalence to make it an equality.) On Sun, Nov 3, 2019 at 3:57 AM David Roberts <droberts.65537@gmail.com> wrote: > > Forget even higher category theory. Kevin Buzzard now goes around telling the story of how even formally proving (using Lean) things in rather elementary commutative algebra from EGA that are stated as equalities was not obvious: the equality is really an isomorphism arising from a universal property. Forget trying to do anything motivic, when algebra is full of such equalities. This is not a problem with univalence, of course. > > David > > On Sun, 3 Nov 2019, 10:08 PM Bas Spitters <b.a.w.spitters@gmail.com> wrote: >> >> There's also VV homotopy lambda calculus, which he later abandoned for MLTT: >> https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf >> >> On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters <b.a.w.spitters@gmail.com> wrote: >>> >>> I believe it refers to his 2-theories: >>> https://www.ias.edu/ideas/2014/voevodsky-origins >>> >>> On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt <zero@fromzerotoinfinity.xyz> wrote: >>>> >>>> In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 talk >>>> at IAS, Voevodsky talks about the history of his project of "univalent >>>> mathematics" and his motivation for starting it. Namely, he mentions >>>> that he found existing proof assistants at that time (in 2000) to be >>>> impractical for the kinds of mathematics he was interested in. >>>> >>>> Unfortunately, he doesn't go into details of what mathematics he was >>>> exactly interested in (I'm guessing something to do with homotopy >>>> theory) or why exactly existing proof assistants weren't practical for >>>> formalizing them. Judging by the things he mentions in his talk, it >>>> seems that (roughly) his rejection of those proof assistants was based >>>> on the view that predicate logic + ZFC is not expressive enough. In >>>> other words, there is too much lossy encoding needed in order to >>>> translate from the platonic world of mathematical ideas to this formal >>>> language. >>>> >>>> Comparing the situation to computer programming languages, one might say >>>> that predicate logic is like Assembly in that even though everything can >>>> be encoded in that language, it is not expressive enough to directly >>>> talk about higher level concepts, diminishing its practical value for >>>> reasoning about mathematics. In particular, those systems are not >>>> adequate for *interactive* development of *new* mathematics (as opposed >>>> to formalization of existing theories). >>>> >>>> Perhaps I am just misinterpreting what Voevodsky said. In this case, I >>>> hope someone can correct me. However even if this wasn't *his* view, to >>>> me it seems to be a view held implicitly in the HoTT community. In any >>>> case, it's a view that one might reasonably hold. >>>> >>>> However I wonder how reasonable that view actually is, i.e. whether e.g. >>>> Mizar really is that much more impractical than HoTT-Coq or Agda, given >>>> that people have been happily formalizing mathematics in it for 46 years >>>> now. And, even though by browsing the contents of "Formalized >>>> Mathematics" one can get the impression that the work consists mostly of >>>> formalizing early 20th century mathematics, neither the UniMath nor the >>>> HoTT library for example contain a proof of Fubini's theorem. >>>> >>>> So, to put this into one concrete question, how (if at all) is HoTT-Coq >>>> more practical than Mizar for the purpose of formalizing mathematics, >>>> outside the specific realm of synthetic homotopy theory? >>>> >>>> >>>> -- >>>> >>>> Nicolas >>>> >>>> >>>> -- >>>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >>>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz. >> >> -- >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com. > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS16Vy7sGiEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQz47kSm9WbKDmUsndrpAJMkNwiWmVABqOFrVqyTOvSAbw%40mail.gmail.com. ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-03 19:13 ` Michael Shulman@ 2019-11-03 19:45 ` Valery Isaev2019-11-03 22:23 ` Martín Hötzel Escardó 2019-11-04 18:42 ` Kevin Buzzard 1 sibling, 1 reply; 32+ messages in thread From: Valery Isaev @ 2019-11-03 19:45 UTC (permalink / raw) To: Michael Shulman Cc: David Roberts, Bas Spitters, homotopytypetheory, Nicolas Alexander Schmidt [-- Attachment #1: Type: text/plain, Size: 7975 bytes --] The isomorphism invariance might be useful when you don't care about the actual stuff you get after transporting. If you have two different definitions of the same set, you can transport its *properties* along the isomorphism (that you still need to construct). For example, we can define rational numbers in two different ways: as arbitrary quotients and as reduced quotients. Then you can prove that they are isomorphic and that one of them gives you a field. Then you know that the other one is also a field. You may be interested in the actual definitions of the operations, but you dob't usually care about the actual proof of the properties. So, you construct the addition and the multiplication explicitly, but you get proofs that they determine a field "for free" from the other definition. If the proofs for one of the definitions is easier than for the other one, this might be a significant simplification. Regards, Valery Isaev вс, 3 нояб. 2019 г. в 22:13, Michael Shulman <shulman@sandiego.edu>: > But does univalence a la Book HoTT *actually* make it easier to reason > about such things? It allows us to write "=" rather than "\cong", but > to construct such an equality we have to construct an isomorphism > first, and to *use* such an equality we have to transport along it, > and then we get lots of univalence-redexes that we have to manually > reduce away. My experience formalizing math in HoTT/Coq is that it's > much easier if you *avoid* turning equivalences into equalities except > when absolutely necessary. (I don't have any experience formalizing > math in a cubical proof assistant, but in that case at least you > wouldn't have to manually reduce the univalence-redexes -- although it > seems to me you'd still have to construct the isomorphism before you > can apply univalence to make it an equality.) > > On Sun, Nov 3, 2019 at 3:57 AM David Roberts <droberts.65537@gmail.com> > wrote: > > > > Forget even higher category theory. Kevin Buzzard now goes around > telling the story of how even formally proving (using Lean) things in > rather elementary commutative algebra from EGA that are stated as > equalities was not obvious: the equality is really an isomorphism arising > from a universal property. Forget trying to do anything motivic, when > algebra is full of such equalities. This is not a problem with univalence, > of course. > > > > David > > > > On Sun, 3 Nov 2019, 10:08 PM Bas Spitters <b.a.w.spitters@gmail.com> > wrote: > >> > >> There's also VV homotopy lambda calculus, which he later abandoned for > MLTT: > >> > https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf > >> > >> On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters <b.a.w.spitters@gmail.com> > wrote: > >>> > >>> I believe it refers to his 2-theories: > >>> https://www.ias.edu/ideas/2014/voevodsky-origins > >>> > >>> On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt < > zero@fromzerotoinfinity.xyz> wrote: > >>>> > >>>> In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 > talk > >>>> at IAS, Voevodsky talks about the history of his project of "univalent > >>>> mathematics" and his motivation for starting it. Namely, he mentions > >>>> that he found existing proof assistants at that time (in 2000) to be > >>>> impractical for the kinds of mathematics he was interested in. > >>>> > >>>> Unfortunately, he doesn't go into details of what mathematics he was > >>>> exactly interested in (I'm guessing something to do with homotopy > >>>> theory) or why exactly existing proof assistants weren't practical for > >>>> formalizing them. Judging by the things he mentions in his talk, it > >>>> seems that (roughly) his rejection of those proof assistants was based > >>>> on the view that predicate logic + ZFC is not expressive enough. In > >>>> other words, there is too much lossy encoding needed in order to > >>>> translate from the platonic world of mathematical ideas to this formal > >>>> language. > >>>> > >>>> Comparing the situation to computer programming languages, one might > say > >>>> that predicate logic is like Assembly in that even though everything > can > >>>> be encoded in that language, it is not expressive enough to directly > >>>> talk about higher level concepts, diminishing its practical value for > >>>> reasoning about mathematics. In particular, those systems are not > >>>> adequate for *interactive* development of *new* mathematics (as > opposed > >>>> to formalization of existing theories). > >>>> > >>>> Perhaps I am just misinterpreting what Voevodsky said. In this case, I > >>>> hope someone can correct me. However even if this wasn't *his* view, > to > >>>> me it seems to be a view held implicitly in the HoTT community. In any > >>>> case, it's a view that one might reasonably hold. > >>>> > >>>> However I wonder how reasonable that view actually is, i.e. whether > e.g. > >>>> Mizar really is that much more impractical than HoTT-Coq or Agda, > given > >>>> that people have been happily formalizing mathematics in it for 46 > years > >>>> now. And, even though by browsing the contents of "Formalized > >>>> Mathematics" one can get the impression that the work consists mostly > of > >>>> formalizing early 20th century mathematics, neither the UniMath nor > the > >>>> HoTT library for example contain a proof of Fubini's theorem. > >>>> > >>>> So, to put this into one concrete question, how (if at all) is > HoTT-Coq > >>>> more practical than Mizar for the purpose of formalizing mathematics, > >>>> outside the specific realm of synthetic homotopy theory? > >>>> > >>>> > >>>> -- > >>>> > >>>> Nicolas > >>>> > >>>> > >>>> -- > >>>> You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > >>>> To unsubscribe from this group and stop receiving emails from it, > send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > >>>> To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz > . > >> > >> -- > >> You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > >> To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > >> To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com > . > > > > -- > > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS16Vy7sGiEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.com > . > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQz47kSm9WbKDmUsndrpAJMkNwiWmVABqOFrVqyTOvSAbw%40mail.gmail.com > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAA520ftr3b4cGi4vXdmJL-GbAVksV9ggrTAmqZ4E75P-ch1hVQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 11338 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-03 19:45 ` Valery Isaev@ 2019-11-03 22:23 ` Martín Hötzel Escardó2019-11-04 23:20 ` Nicolas Alexander Schmidt 0 siblings, 1 reply; 32+ messages in thread From: Martín Hötzel Escardó @ 2019-11-03 22:23 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 8618 bytes --] This discussion reminds me of this question: https://mathoverflow.net/questions/336191/cauchy-reals-and-dedekind-reals-satisfy-the-same-mathematical-theorems/336233?noredirect=1#comment840649_336233 M. On Sunday, 3 November 2019 19:46:32 UTC, Valery Isaev wrote: > > The isomorphism invariance might be useful when you don't care about the > actual stuff you get after transporting. If you have two different > definitions of the same set, you can transport its *properties* along the > isomorphism (that you still need to construct). For example, we can define > rational numbers in two different ways: as arbitrary quotients and as > reduced quotients. Then you can prove that they are isomorphic and that one > of them gives you a field. Then you know that the other one is also a > field. You may be interested in the actual definitions of the operations, > but you dob't usually care about the actual proof of the properties. So, > you construct the addition and the multiplication explicitly, but you get > proofs that they determine a field "for free" from the other definition. If > the proofs for one of the definitions is easier than for the other one, > this might be a significant simplification. > > Regards, > Valery Isaev > > > вс, 3 нояб. 2019 г. в 22:13, Michael Shulman <shu...@sandiego.edu > <javascript:>>: > >> But does univalence a la Book HoTT *actually* make it easier to reason >> about such things? It allows us to write "=" rather than "\cong", but >> to construct such an equality we have to construct an isomorphism >> first, and to *use* such an equality we have to transport along it, >> and then we get lots of univalence-redexes that we have to manually >> reduce away. My experience formalizing math in HoTT/Coq is that it's >> much easier if you *avoid* turning equivalences into equalities except >> when absolutely necessary. (I don't have any experience formalizing >> math in a cubical proof assistant, but in that case at least you >> wouldn't have to manually reduce the univalence-redexes -- although it >> seems to me you'd still have to construct the isomorphism before you >> can apply univalence to make it an equality.) >> >> On Sun, Nov 3, 2019 at 3:57 AM David Roberts <drober...@gmail.com >> <javascript:>> wrote: >> > >> > Forget even higher category theory. Kevin Buzzard now goes around >> telling the story of how even formally proving (using Lean) things in >> rather elementary commutative algebra from EGA that are stated as >> equalities was not obvious: the equality is really an isomorphism arising >> from a universal property. Forget trying to do anything motivic, when >> algebra is full of such equalities. This is not a problem with univalence, >> of course. >> > >> > David >> > >> > On Sun, 3 Nov 2019, 10:08 PM Bas Spitters <b.a.w...@gmail.com >> <javascript:>> wrote: >> >> >> >> There's also VV homotopy lambda calculus, which he later abandoned for >> MLTT: >> >> >> https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf >> >> >> >> On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters <b.a.w...@gmail.com >> <javascript:>> wrote: >> >>> >> >>> I believe it refers to his 2-theories: >> >>> https://www.ias.edu/ideas/2014/voevodsky-origins >> >>> >> >>> On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt < >> ze...@fromzerotoinfinity.xyz <javascript:>> wrote: >> >>>> >> >>>> In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 >> talk >> >>>> at IAS, Voevodsky talks about the history of his project of >> "univalent >> >>>> mathematics" and his motivation for starting it. Namely, he mentions >> >>>> that he found existing proof assistants at that time (in 2000) to be >> >>>> impractical for the kinds of mathematics he was interested in. >> >>>> >> >>>> Unfortunately, he doesn't go into details of what mathematics he was >> >>>> exactly interested in (I'm guessing something to do with homotopy >> >>>> theory) or why exactly existing proof assistants weren't practical >> for >> >>>> formalizing them. Judging by the things he mentions in his talk, it >> >>>> seems that (roughly) his rejection of those proof assistants was >> based >> >>>> on the view that predicate logic + ZFC is not expressive enough. In >> >>>> other words, there is too much lossy encoding needed in order to >> >>>> translate from the platonic world of mathematical ideas to this >> formal >> >>>> language. >> >>>> >> >>>> Comparing the situation to computer programming languages, one might >> say >> >>>> that predicate logic is like Assembly in that even though everything >> can >> >>>> be encoded in that language, it is not expressive enough to directly >> >>>> talk about higher level concepts, diminishing its practical value for >> >>>> reasoning about mathematics. In particular, those systems are not >> >>>> adequate for *interactive* development of *new* mathematics (as >> opposed >> >>>> to formalization of existing theories). >> >>>> >> >>>> Perhaps I am just misinterpreting what Voevodsky said. In this case, >> I >> >>>> hope someone can correct me. However even if this wasn't *his* view, >> to >> >>>> me it seems to be a view held implicitly in the HoTT community. In >> any >> >>>> case, it's a view that one might reasonably hold. >> >>>> >> >>>> However I wonder how reasonable that view actually is, i.e. whether >> e.g. >> >>>> Mizar really is that much more impractical than HoTT-Coq or Agda, >> given >> >>>> that people have been happily formalizing mathematics in it for 46 >> years >> >>>> now. And, even though by browsing the contents of "Formalized >> >>>> Mathematics" one can get the impression that the work consists >> mostly of >> >>>> formalizing early 20th century mathematics, neither the UniMath nor >> the >> >>>> HoTT library for example contain a proof of Fubini's theorem. >> >>>> >> >>>> So, to put this into one concrete question, how (if at all) is >> HoTT-Coq >> >>>> more practical than Mizar for the purpose of formalizing mathematics, >> >>>> outside the specific realm of synthetic homotopy theory? >> >>>> >> >>>> >> >>>> -- >> >>>> >> >>>> Nicolas >> >>>> >> >>>> >> >>>> -- >> >>>> You received this message because you are subscribed to the Google >> Groups "Homotopy Type Theory" group. >> >>>> To unsubscribe from this group and stop receiving emails from it, >> send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com >> <javascript:>. >> >>>> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz >> . >> >> >> >> -- >> >> You received this message because you are subscribed to the Google >> Groups "Homotopy Type Theory" group. >> >> To unsubscribe from this group and stop receiving emails from it, send >> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com <javascript:> >> . >> >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com >> . >> > >> > -- >> > You received this message because you are subscribed to the Google >> Groups "Homotopy Type Theory" group. >> > To unsubscribe from this group and stop receiving emails from it, send >> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com <javascript:> >> . >> > To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS16Vy7sGiEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.com >> . >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com <javascript:>. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQz47kSm9WbKDmUsndrpAJMkNwiWmVABqOFrVqyTOvSAbw%40mail.gmail.com >> . >> > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/2ca6c47c-6196-4b45-b82c-db79b2b6568c%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 15499 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-03 19:13 ` Michael Shulman 2019-11-03 19:45 ` Valery Isaev@ 2019-11-04 18:42 ` Kevin Buzzard2019-11-04 21:10 ` Michael Shulman ` (3 more replies) 1 sibling, 4 replies; 32+ messages in thread From: Kevin Buzzard @ 2019-11-04 18:42 UTC (permalink / raw) To: Michael Shulman Cc: David Roberts, Bas Spitters, homotopytypetheory, Nicolas Alexander Schmidt [-- Attachment #1: Type: text/plain, Size: 12458 bytes --] On Sun, 3 Nov 2019 at 19:13, Michael Shulman <shulman@sandiego.edu> wrote: > But does univalence a la Book HoTT *actually* make it easier to reason > about such things? I think this is a really interesting and important question. I guess David was referring to my scheme fail of 2018. I wanted to formalise the notion of a scheme a la Grothendieck and prove that if R was a commutative ring then Spec(R) was a scheme [I know it's a definition, but many mathematicians do seem to call it a theorem, in our ignorance]. I showed an undergraduate a specific lemma in ring theory ( https://stacks.math.columbia.edu/tag/00EJ) and said "that's what I want" and they formalised it for me. And then it turned out that I wanted something else: I didn't have R_f, I had something "canonically isomorphic" to it, a phrase we mathematicians like to pull out when the going gets tough and we can't be bothered to check that any more diagrams commute. By this point it was too late to turn back, and so I had to prove that 20 diagrams commuted and it wasn't much fun. I then got an MSc student to redo everything using universal properties more carefully in Lean and it worked like a dream https://github.com/ramonfmir/lean-scheme. A lot of people said to me at the time "you wouldn't have had this problem if you'd been using HoTT instead of DTT" and my response to this is still the (intentionally) provocative "go ahead and define schemes and prove that Spec(R) is a scheme in some HoTT system, and show me how it's better; note that we did have a problem, but we solved it in DTT". I would be particularly interested to see schemes done in Arend, because it always felt funny to me using UniMath in Coq (and similarly it feels funny to me to do HoTT in Lean 3 -- in both cases it could be argued that it's using a system to do something it wasn't designed to do). I think it's easy to theorise about this sort of thing but until it happens in practice in one or more of the HoTT systems I don't think we will understand the issue properly (or, more precisely, I don't think I will understand the issue properly). I have had extensive discussions with Martin Escardo about HoTT and he has certainly given me hope, but on the Lean chat I think people assumed schemes would be easy in Lean (I certainly did) and then we ran into this unexpected problem (which univalence is probably designed to solve), so the question is whether a univalent type theory runs into a different unexpected problem -- you push the carpet down somewhere and it pops up somewhere else. I know this is a HoTT list but the challenge is also open to the HOL people like the Isabelle/HOL experts. In contrast to HoTT theories, which I think should handle schemes fine, I think that simple type theory will have tremendous problems defining, for example, tensor products of sheaves of modules on a scheme, because these are dependent types. On the other hand my recent ArXiv paper with Commelin and Massot https://arxiv.org/abs/1910.12320 goes much further and formalises perfectoid spaces in dependent type theory. I would like the people on this list to see this as a challenge. I think that this century will see the rise of the theorem prover in mathematics and I am not naive enough to think that the one I currently use now is the one which is guaranteed to be the success story. Voevodsky was convinced that univalence was the right way to do modern mathematics but I'm doing it just fine in dependent type theory and now he's gone I really want to find someone who will take up the challenge and do some scheme theory in HoTT, but convincing professional mathematicians to get interested in this area is very difficult, and I speak as someone who's been trying to do it for two years now [I recommend you try the undergraduates instead, anyone who is interested in training people up -- plenty of undergraduates are capable of reading the definition of a scheme, if they know what rings and topological spaces are] To get back to the original question, my understanding was that Voevodsky had done a bunch of scheme theory and it had got him a Fields medal and it was this mathematics which he was interested in at the time. He wanted to formalise his big theorem, just like Hales did. Unfortunately he was historically earlier, and his mathematics involved far more conceptual objects than spheres in 3-space, so it was a much taller order. All the evidence is there to suggest that over the next 15 or so years his interests changed. The clearest evidence, in my mind, is that there is no definition of a scheme in UniMath. Moreover his story in his Cambridge talk https://www.newton.ac.uk/seminar/20170710113012301 about asking Suslin to reprove one of his results without using the axiom of choice (46 minutes in) kind of shocked me -- Suslin does not care about mathematics without choice, and the vast majority of mathematicians employed in mathematics departments feel the same, although I'm well aware that constructivism is taken more seriously on this list. I think it is interesting that Voevodsky failed to prove a constructive version of his theorem, because I think that some mathematics is better off not being constructive. It is exactly the interaction between constructivism and univalence which I do not understand well, and I think that a very good way to investigate it would be to do some highly non-constructive modern mathematics in a univalent type theory. Kevin PS many thanks to the people who have emailed me in the past telling me about how in the past I have used "HoTT", "univalence", "UniMath", interchangeably and incorrectly. Hopefully I am getting better but I am still keen to hear anything which I'm saying which is imprecise or incorrect. > It allows us to write "=" rather than "\cong", but > to construct such an equality we have to construct an isomorphism > first, and to *use* such an equality we have to transport along it, > and then we get lots of univalence-redexes that we have to manually > reduce away. My experience formalizing math in HoTT/Coq is that it's > much easier if you *avoid* turning equivalences into equalities except > when absolutely necessary. (I don't have any experience formalizing > math in a cubical proof assistant, but in that case at least you > wouldn't have to manually reduce the univalence-redexes -- although it > seems to me you'd still have to construct the isomorphism before you > can apply univalence to make it an equality.) > > On Sun, Nov 3, 2019 at 3:57 AM David Roberts <droberts.65537@gmail.com> > wrote: > > > > Forget even higher category theory. Kevin Buzzard now goes around > telling the story of how even formally proving (using Lean) things in > rather elementary commutative algebra from EGA that are stated as > equalities was not obvious: the equality is really an isomorphism arising > from a universal property. Forget trying to do anything motivic, when > algebra is full of such equalities. This is not a problem with univalence, > of course. > > > > David > > > > On Sun, 3 Nov 2019, 10:08 PM Bas Spitters <b.a.w.spitters@gmail.com> > wrote: > >> > >> There's also VV homotopy lambda calculus, which he later abandoned for > MLTT: > >> > https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf > >> > >> On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters <b.a.w.spitters@gmail.com> > wrote: > >>> > >>> I believe it refers to his 2-theories: > >>> https://www.ias.edu/ideas/2014/voevodsky-origins > >>> > >>> On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt < > zero@fromzerotoinfinity.xyz> wrote: > >>>> > >>>> In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 > talk > >>>> at IAS, Voevodsky talks about the history of his project of "univalent > >>>> mathematics" and his motivation for starting it. Namely, he mentions > >>>> that he found existing proof assistants at that time (in 2000) to be > >>>> impractical for the kinds of mathematics he was interested in. > >>>> > >>>> Unfortunately, he doesn't go into details of what mathematics he was > >>>> exactly interested in (I'm guessing something to do with homotopy > >>>> theory) or why exactly existing proof assistants weren't practical for > >>>> formalizing them. Judging by the things he mentions in his talk, it > >>>> seems that (roughly) his rejection of those proof assistants was based > >>>> on the view that predicate logic + ZFC is not expressive enough. In > >>>> other words, there is too much lossy encoding needed in order to > >>>> translate from the platonic world of mathematical ideas to this formal > >>>> language. > >>>> > >>>> Comparing the situation to computer programming languages, one might > say > >>>> that predicate logic is like Assembly in that even though everything > can > >>>> be encoded in that language, it is not expressive enough to directly > >>>> talk about higher level concepts, diminishing its practical value for > >>>> reasoning about mathematics. In particular, those systems are not > >>>> adequate for *interactive* development of *new* mathematics (as > opposed > >>>> to formalization of existing theories). > >>>> > >>>> Perhaps I am just misinterpreting what Voevodsky said. In this case, I > >>>> hope someone can correct me. However even if this wasn't *his* view, > to > >>>> me it seems to be a view held implicitly in the HoTT community. In any > >>>> case, it's a view that one might reasonably hold. > >>>> > >>>> However I wonder how reasonable that view actually is, i.e. whether > e.g. > >>>> Mizar really is that much more impractical than HoTT-Coq or Agda, > given > >>>> that people have been happily formalizing mathematics in it for 46 > years > >>>> now. And, even though by browsing the contents of "Formalized > >>>> Mathematics" one can get the impression that the work consists mostly > of > >>>> formalizing early 20th century mathematics, neither the UniMath nor > the > >>>> HoTT library for example contain a proof of Fubini's theorem. > >>>> > >>>> So, to put this into one concrete question, how (if at all) is > HoTT-Coq > >>>> more practical than Mizar for the purpose of formalizing mathematics, > >>>> outside the specific realm of synthetic homotopy theory? > >>>> > >>>> > >>>> -- > >>>> > >>>> Nicolas > >>>> > >>>> > >>>> -- > >>>> You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > >>>> To unsubscribe from this group and stop receiving emails from it, > send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > >>>> To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz > . > >> > >> -- > >> You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > >> To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > >> To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com > . > > > > -- > > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS16Vy7sGiEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.com > . > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQz47kSm9WbKDmUsndrpAJMkNwiWmVABqOFrVqyTOvSAbw%40mail.gmail.com > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb3s0%2BvweUaSQBMBNLa5mRc9F1jrsg2sSoFmcE_4%3DdAt1w%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 16518 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-04 18:42 ` Kevin Buzzard@ 2019-11-04 21:10 ` Michael Shulman2019-11-04 23:26 ` David Roberts ` (2 subsequent siblings) 3 siblings, 0 replies; 32+ messages in thread From: Michael Shulman @ 2019-11-04 21:10 UTC (permalink / raw) To: Kevin Buzzard Cc: David Roberts, Bas Spitters, homotopytypetheory, Nicolas Alexander Schmidt Valery has a good point that transporting properties along an equivalence is definitely somewhere that Book HoTT could get you some mileage. But I suspect that a more significant advantage would come from using a cubical type theory in which transport computes (as long as the equivalence was defined constructively -- a good reason to care about being constructive even putting aside philosophy and internal languages). I'd be curious to know what those 20 diagrams were. FWIW, I think that nowadays Coq *is* designed for Book HoTT, certainly more than Lean 3 is. My understanding is that Lean 3 is actually technically incompatible with univalence, whereas over the past decade the Coq developers have incorporated various new features requested by the HoTT community to improve compatibility, and the HoTT Coq library is I believe one of the test suites that new Coq versions are tested against to ensure that breakage is dealt with on one side or another. I'm not sure how a proof assistant could be more designed for Book HoTT than modern Coq and Agda are. (Arend is not designed for Book HoTT, but for a flavor of HoTT that's partway to a cubical theory, with an interval type representing paths.) On Mon, Nov 4, 2019 at 10:43 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > > > On Sun, 3 Nov 2019 at 19:13, Michael Shulman <shulman@sandiego.edu> wrote: >> >> But does univalence a la Book HoTT *actually* make it easier to reason >> about such things? > > > I think this is a really interesting and important question. > > I guess David was referring to my scheme fail of 2018. I wanted to formalise the notion of a scheme a la Grothendieck and prove that if R was a commutative ring then Spec(R) was a scheme [I know it's a definition, but many mathematicians do seem to call it a theorem, in our ignorance]. I showed an undergraduate a specific lemma in ring theory (https://stacks.math.columbia.edu/tag/00EJ) and said "that's what I want" and they formalised it for me. And then it turned out that I wanted something else: I didn't have R_f, I had something "canonically isomorphic" to it, a phrase we mathematicians like to pull out when the going gets tough and we can't be bothered to check that any more diagrams commute. By this point it was too late to turn back, and so I had to prove that 20 diagrams commuted and it wasn't much fun. I then got an MSc student to redo everything using universal properties more carefully in Lean and it worked like a dream https://github.com/ramonfmir/lean-scheme. A lot of people said to me at the time "you wouldn't have had this problem if you'd been using HoTT instead of DTT" and my response to this is still the (intentionally) provocative "go ahead and define schemes and prove that Spec(R) is a scheme in some HoTT system, and show me how it's better; note that we did have a problem, but we solved it in DTT". I would be particularly interested to see schemes done in Arend, because it always felt funny to me using UniMath in Coq (and similarly it feels funny to me to do HoTT in Lean 3 -- in both cases it could be argued that it's using a system to do something it wasn't designed to do). I think it's easy to theorise about this sort of thing but until it happens in practice in one or more of the HoTT systems I don't think we will understand the issue properly (or, more precisely, I don't think I will understand the issue properly). I have had extensive discussions with Martin Escardo about HoTT and he has certainly given me hope, but on the Lean chat I think people assumed schemes would be easy in Lean (I certainly did) and then we ran into this unexpected problem (which univalence is probably designed to solve), so the question is whether a univalent type theory runs into a different unexpected problem -- you push the carpet down somewhere and it pops up somewhere else. > > I know this is a HoTT list but the challenge is also open to the HOL people like the Isabelle/HOL experts. In contrast to HoTT theories, which I think should handle schemes fine, I think that simple type theory will have tremendous problems defining, for example, tensor products of sheaves of modules on a scheme, because these are dependent types. On the other hand my recent ArXiv paper with Commelin and Massot https://arxiv.org/abs/1910.12320 goes much further and formalises perfectoid spaces in dependent type theory. I would like the people on this list to see this as a challenge. I think that this century will see the rise of the theorem prover in mathematics and I am not naive enough to think that the one I currently use now is the one which is guaranteed to be the success story. Voevodsky was convinced that univalence was the right way to do modern mathematics but I'm doing it just fine in dependent type theory and now he's gone I really want to find someone who will take up the challenge and do some scheme theory in HoTT, but convincing professional mathematicians to get interested in this area is very difficult, and I speak as someone who's been trying to do it for two years now [I recommend you try the undergraduates instead, anyone who is interested in training people up -- plenty of undergraduates are capable of reading the definition of a scheme, if they know what rings and topological spaces are] > > To get back to the original question, my understanding was that Voevodsky had done a bunch of scheme theory and it had got him a Fields medal and it was this mathematics which he was interested in at the time. He wanted to formalise his big theorem, just like Hales did. Unfortunately he was historically earlier, and his mathematics involved far more conceptual objects than spheres in 3-space, so it was a much taller order. All the evidence is there to suggest that over the next 15 or so years his interests changed. The clearest evidence, in my mind, is that there is no definition of a scheme in UniMath. Moreover his story in his Cambridge talk https://www.newton.ac.uk/seminar/20170710113012301 about asking Suslin to reprove one of his results without using the axiom of choice (46 minutes in) kind of shocked me -- Suslin does not care about mathematics without choice, and the vast majority of mathematicians employed in mathematics departments feel the same, although I'm well aware that constructivism is taken more seriously on this list. I think it is interesting that Voevodsky failed to prove a constructive version of his theorem, because I think that some mathematics is better off not being constructive. It is exactly the interaction between constructivism and univalence which I do not understand well, and I think that a very good way to investigate it would be to do some highly non-constructive modern mathematics in a univalent type theory. > > Kevin > > PS many thanks to the people who have emailed me in the past telling me about how in the past I have used "HoTT", "univalence", "UniMath", interchangeably and incorrectly. Hopefully I am getting better but I am still keen to hear anything which I'm saying which is imprecise or incorrect. > > >> >> It allows us to write "=" rather than "\cong", but >> to construct such an equality we have to construct an isomorphism >> first, and to *use* such an equality we have to transport along it, >> and then we get lots of univalence-redexes that we have to manually >> reduce away. My experience formalizing math in HoTT/Coq is that it's >> much easier if you *avoid* turning equivalences into equalities except >> when absolutely necessary. (I don't have any experience formalizing >> math in a cubical proof assistant, but in that case at least you >> wouldn't have to manually reduce the univalence-redexes -- although it >> seems to me you'd still have to construct the isomorphism before you >> can apply univalence to make it an equality.) >> >> On Sun, Nov 3, 2019 at 3:57 AM David Roberts <droberts.65537@gmail.com> wrote: >> > >> > Forget even higher category theory. Kevin Buzzard now goes around telling the story of how even formally proving (using Lean) things in rather elementary commutative algebra from EGA that are stated as equalities was not obvious: the equality is really an isomorphism arising from a universal property. Forget trying to do anything motivic, when algebra is full of such equalities. This is not a problem with univalence, of course. >> > >> > David >> > >> > On Sun, 3 Nov 2019, 10:08 PM Bas Spitters <b.a.w.spitters@gmail.com> wrote: >> >> >> >> There's also VV homotopy lambda calculus, which he later abandoned for MLTT: >> >> https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf >> >> >> >> On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters <b.a.w.spitters@gmail.com> wrote: >> >>> >> >>> I believe it refers to his 2-theories: >> >>> https://www.ias.edu/ideas/2014/voevodsky-origins >> >>> >> >>> On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt <zero@fromzerotoinfinity.xyz> wrote: >> >>>> >> >>>> In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 talk >> >>>> at IAS, Voevodsky talks about the history of his project of "univalent >> >>>> mathematics" and his motivation for starting it. Namely, he mentions >> >>>> that he found existing proof assistants at that time (in 2000) to be >> >>>> impractical for the kinds of mathematics he was interested in. >> >>>> >> >>>> Unfortunately, he doesn't go into details of what mathematics he was >> >>>> exactly interested in (I'm guessing something to do with homotopy >> >>>> theory) or why exactly existing proof assistants weren't practical for >> >>>> formalizing them. Judging by the things he mentions in his talk, it >> >>>> seems that (roughly) his rejection of those proof assistants was based >> >>>> on the view that predicate logic + ZFC is not expressive enough. In >> >>>> other words, there is too much lossy encoding needed in order to >> >>>> translate from the platonic world of mathematical ideas to this formal >> >>>> language. >> >>>> >> >>>> Comparing the situation to computer programming languages, one might say >> >>>> that predicate logic is like Assembly in that even though everything can >> >>>> be encoded in that language, it is not expressive enough to directly >> >>>> talk about higher level concepts, diminishing its practical value for >> >>>> reasoning about mathematics. In particular, those systems are not >> >>>> adequate for *interactive* development of *new* mathematics (as opposed >> >>>> to formalization of existing theories). >> >>>> >> >>>> Perhaps I am just misinterpreting what Voevodsky said. In this case, I >> >>>> hope someone can correct me. However even if this wasn't *his* view, to >> >>>> me it seems to be a view held implicitly in the HoTT community. In any >> >>>> case, it's a view that one might reasonably hold. >> >>>> >> >>>> However I wonder how reasonable that view actually is, i.e. whether e.g. >> >>>> Mizar really is that much more impractical than HoTT-Coq or Agda, given >> >>>> that people have been happily formalizing mathematics in it for 46 years >> >>>> now. And, even though by browsing the contents of "Formalized >> >>>> Mathematics" one can get the impression that the work consists mostly of >> >>>> formalizing early 20th century mathematics, neither the UniMath nor the >> >>>> HoTT library for example contain a proof of Fubini's theorem. >> >>>> >> >>>> So, to put this into one concrete question, how (if at all) is HoTT-Coq >> >>>> more practical than Mizar for the purpose of formalizing mathematics, >> >>>> outside the specific realm of synthetic homotopy theory? >> >>>> >> >>>> >> >>>> -- >> >>>> >> >>>> Nicolas >> >>>> >> >>>> >> >>>> -- >> >>>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> >>>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> >>>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz. >> >> >> >> -- >> >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> >> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com. >> > >> > -- >> > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS16Vy7sGiEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.com. >> >> -- >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQz47kSm9WbKDmUsndrpAJMkNwiWmVABqOFrVqyTOvSAbw%40mail.gmail.com. > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb3s0%2BvweUaSQBMBNLa5mRc9F1jrsg2sSoFmcE_4%3DdAt1w%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQy4zN1wc%3Dw5-%2Beu2hBwtbUC-gtzjuYabiZWdb4yKZ7NUw%40mail.gmail.com. ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-03 22:23 ` Martín Hötzel Escardó@ 2019-11-04 23:20 ` Nicolas Alexander Schmidt2019-11-24 18:11 ` Kevin Buzzard 0 siblings, 1 reply; 32+ messages in thread From: Nicolas Alexander Schmidt @ 2019-11-04 23:20 UTC (permalink / raw) To: HomotopyTypeTheory Dear Bas, Michael, David, Valery, Martín and Kevin, thank you all for your replies. When I posed my question, I didn't expect there to be so much room for debate. In particular, I am surprised that it seems not at all clear how much univalence actually helps the practicality of doing formal proofs (as opposed to any theoretical benefits). Kevin, I would like to second Michael's interest in seeing these 20 commutative diagrams. Moreover, I'd also be very interested in seeing your "spaghetti code" (quote from the slides of your Big Proof talk): it seems it should be informative to see where your initial approach went wrong, and how much these problems and their solution had anything to do at all with the formal system you were working in. Are your original files perhaps available somewhere? -- Nicolas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinity.xyz. ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-04 18:42 ` Kevin Buzzard 2019-11-04 21:10 ` Michael Shulman@ 2019-11-04 23:26 ` David Roberts2019-11-05 15:43 ` Daniel R. Grayson 2019-11-05 23:14 ` Martín Hötzel Escardó 3 siblings, 0 replies; 32+ messages in thread From: David Roberts @ 2019-11-04 23:26 UTC (permalink / raw) To: Kevin Buzzard Cc: Michael Shulman, Bas Spitters, homotopytypetheory, Nicolas Alexander Schmidt Hi, Going back a step from DTT vs HoTT... > I think that simple type theory will have tremendous problems defining, for example, tensor products of sheaves of modules on a scheme, because these are dependent types. this is probably where VV found himself just under 20 years ago. I don't know what the state of play was around 2000, but certainly if he didn't know about Coq, then VV's options for formal proof systems were looking more like Mizar, MetaMath and similar, which are probably even worse than simple type-theory systems: imagine trying to formally define a scheme in the language of ZFC! Best regards, David David Roberts Webpage: https://ncatlab.org/nlab/show/David+Roberts Blog: https://thehighergeometer.wordpress.com On Tue, 5 Nov 2019 at 05:13, Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > > > On Sun, 3 Nov 2019 at 19:13, Michael Shulman <shulman@sandiego.edu> wrote: >> >> But does univalence a la Book HoTT *actually* make it easier to reason >> about such things? > > > I think this is a really interesting and important question. > > I guess David was referring to my scheme fail of 2018. I wanted to formalise the notion of a scheme a la Grothendieck and prove that if R was a commutative ring then Spec(R) was a scheme [I know it's a definition, but many mathematicians do seem to call it a theorem, in our ignorance]. I showed an undergraduate a specific lemma in ring theory (https://stacks.math.columbia.edu/tag/00EJ) and said "that's what I want" and they formalised it for me. And then it turned out that I wanted something else: I didn't have R_f, I had something "canonically isomorphic" to it, a phrase we mathematicians like to pull out when the going gets tough and we can't be bothered to check that any more diagrams commute. By this point it was too late to turn back, and so I had to prove that 20 diagrams commuted and it wasn't much fun. I then got an MSc student to redo everything using universal properties more carefully in Lean and it worked like a dream https://github.com/ramonfmir/lean-scheme. A lot of people said to me at the time "you wouldn't have had this problem if you'd been using HoTT instead of DTT" and my response to this is still the (intentionally) provocative "go ahead and define schemes and prove that Spec(R) is a scheme in some HoTT system, and show me how it's better; note that we did have a problem, but we solved it in DTT". I would be particularly interested to see schemes done in Arend, because it always felt funny to me using UniMath in Coq (and similarly it feels funny to me to do HoTT in Lean 3 -- in both cases it could be argued that it's using a system to do something it wasn't designed to do). I think it's easy to theorise about this sort of thing but until it happens in practice in one or more of the HoTT systems I don't think we will understand the issue properly (or, more precisely, I don't think I will understand the issue properly). I have had extensive discussions with Martin Escardo about HoTT and he has certainly given me hope, but on the Lean chat I think people assumed schemes would be easy in Lean (I certainly did) and then we ran into this unexpected problem (which univalence is probably designed to solve), so the question is whether a univalent type theory runs into a different unexpected problem -- you push the carpet down somewhere and it pops up somewhere else. > > I know this is a HoTT list but the challenge is also open to the HOL people like the Isabelle/HOL experts. In contrast to HoTT theories, which I think should handle schemes fine, I think that simple type theory will have tremendous problems defining, for example, tensor products of sheaves of modules on a scheme, because these are dependent types. On the other hand my recent ArXiv paper with Commelin and Massot https://arxiv.org/abs/1910.12320 goes much further and formalises perfectoid spaces in dependent type theory. I would like the people on this list to see this as a challenge. I think that this century will see the rise of the theorem prover in mathematics and I am not naive enough to think that the one I currently use now is the one which is guaranteed to be the success story. Voevodsky was convinced that univalence was the right way to do modern mathematics but I'm doing it just fine in dependent type theory and now he's gone I really want to find someone who will take up the challenge and do some scheme theory in HoTT, but convincing professional mathematicians to get interested in this area is very difficult, and I speak as someone who's been trying to do it for two years now [I recommend you try the undergraduates instead, anyone who is interested in training people up -- plenty of undergraduates are capable of reading the definition of a scheme, if they know what rings and topological spaces are] > > To get back to the original question, my understanding was that Voevodsky had done a bunch of scheme theory and it had got him a Fields medal and it was this mathematics which he was interested in at the time. He wanted to formalise his big theorem, just like Hales did. Unfortunately he was historically earlier, and his mathematics involved far more conceptual objects than spheres in 3-space, so it was a much taller order. All the evidence is there to suggest that over the next 15 or so years his interests changed. The clearest evidence, in my mind, is that there is no definition of a scheme in UniMath. Moreover his story in his Cambridge talk https://www.newton.ac.uk/seminar/20170710113012301 about asking Suslin to reprove one of his results without using the axiom of choice (46 minutes in) kind of shocked me -- Suslin does not care about mathematics without choice, and the vast majority of mathematicians employed in mathematics departments feel the same, although I'm well aware that constructivism is taken more seriously on this list. I think it is interesting that Voevodsky failed to prove a constructive version of his theorem, because I think that some mathematics is better off not being constructive. It is exactly the interaction between constructivism and univalence which I do not understand well, and I think that a very good way to investigate it would be to do some highly non-constructive modern mathematics in a univalent type theory. > > Kevin > > PS many thanks to the people who have emailed me in the past telling me about how in the past I have used "HoTT", "univalence", "UniMath", interchangeably and incorrectly. Hopefully I am getting better but I am still keen to hear anything which I'm saying which is imprecise or incorrect. > > >> >> It allows us to write "=" rather than "\cong", but >> to construct such an equality we have to construct an isomorphism >> first, and to *use* such an equality we have to transport along it, >> and then we get lots of univalence-redexes that we have to manually >> reduce away. My experience formalizing math in HoTT/Coq is that it's >> much easier if you *avoid* turning equivalences into equalities except >> when absolutely necessary. (I don't have any experience formalizing >> math in a cubical proof assistant, but in that case at least you >> wouldn't have to manually reduce the univalence-redexes -- although it >> seems to me you'd still have to construct the isomorphism before you >> can apply univalence to make it an equality.) >> >> On Sun, Nov 3, 2019 at 3:57 AM David Roberts <droberts.65537@gmail.com> wrote: >> > >> > Forget even higher category theory. Kevin Buzzard now goes around telling the story of how even formally proving (using Lean) things in rather elementary commutative algebra from EGA that are stated as equalities was not obvious: the equality is really an isomorphism arising from a universal property. Forget trying to do anything motivic, when algebra is full of such equalities. This is not a problem with univalence, of course. >> > >> > David >> > >> > On Sun, 3 Nov 2019, 10:08 PM Bas Spitters <b.a.w.spitters@gmail.com> wrote: >> >> >> >> There's also VV homotopy lambda calculus, which he later abandoned for MLTT: >> >> https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf >> >> >> >> On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters <b.a.w.spitters@gmail.com> wrote: >> >>> >> >>> I believe it refers to his 2-theories: >> >>> https://www.ias.edu/ideas/2014/voevodsky-origins >> >>> >> >>> On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt <zero@fromzerotoinfinity.xyz> wrote: >> >>>> >> >>>> In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 talk >> >>>> at IAS, Voevodsky talks about the history of his project of "univalent >> >>>> mathematics" and his motivation for starting it. Namely, he mentions >> >>>> that he found existing proof assistants at that time (in 2000) to be >> >>>> impractical for the kinds of mathematics he was interested in. >> >>>> >> >>>> Unfortunately, he doesn't go into details of what mathematics he was >> >>>> exactly interested in (I'm guessing something to do with homotopy >> >>>> theory) or why exactly existing proof assistants weren't practical for >> >>>> formalizing them. Judging by the things he mentions in his talk, it >> >>>> seems that (roughly) his rejection of those proof assistants was based >> >>>> on the view that predicate logic + ZFC is not expressive enough. In >> >>>> other words, there is too much lossy encoding needed in order to >> >>>> translate from the platonic world of mathematical ideas to this formal >> >>>> language. >> >>>> >> >>>> Comparing the situation to computer programming languages, one might say >> >>>> that predicate logic is like Assembly in that even though everything can >> >>>> be encoded in that language, it is not expressive enough to directly >> >>>> talk about higher level concepts, diminishing its practical value for >> >>>> reasoning about mathematics. In particular, those systems are not >> >>>> adequate for *interactive* development of *new* mathematics (as opposed >> >>>> to formalization of existing theories). >> >>>> >> >>>> Perhaps I am just misinterpreting what Voevodsky said. In this case, I >> >>>> hope someone can correct me. However even if this wasn't *his* view, to >> >>>> me it seems to be a view held implicitly in the HoTT community. In any >> >>>> case, it's a view that one might reasonably hold. >> >>>> >> >>>> However I wonder how reasonable that view actually is, i.e. whether e.g. >> >>>> Mizar really is that much more impractical than HoTT-Coq or Agda, given >> >>>> that people have been happily formalizing mathematics in it for 46 years >> >>>> now. And, even though by browsing the contents of "Formalized >> >>>> Mathematics" one can get the impression that the work consists mostly of >> >>>> formalizing early 20th century mathematics, neither the UniMath nor the >> >>>> HoTT library for example contain a proof of Fubini's theorem. >> >>>> >> >>>> So, to put this into one concrete question, how (if at all) is HoTT-Coq >> >>>> more practical than Mizar for the purpose of formalizing mathematics, >> >>>> outside the specific realm of synthetic homotopy theory? >> >>>> >> >>>> >> >>>> -- >> >>>> >> >>>> Nicolas >> >>>> >> >>>> >> >>>> -- >> >>>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> >>>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> >>>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz. >> >> >> >> -- >> >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> >> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com. >> > >> > -- >> > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS16Vy7sGiEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.com. >> >> -- >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQz47kSm9WbKDmUsndrpAJMkNwiWmVABqOFrVqyTOvSAbw%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM9-VQE6xR%2BRVsU54dBP4U1GkQ%2B9-MuxN%2BBMC40JKoo2GQ%40mail.gmail.com. ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-04 18:42 ` Kevin Buzzard 2019-11-04 21:10 ` Michael Shulman 2019-11-04 23:26 ` David Roberts@ 2019-11-05 15:43 ` Daniel R. Grayson2019-11-05 20:29 ` Yuhao Huang 2019-11-05 23:14 ` Martín Hötzel Escardó 3 siblings, 1 reply; 32+ messages in thread From: Daniel R. Grayson @ 2019-11-05 15:43 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1554 bytes --] Re: "To get back to the original question, my understanding was that Voevodsky had done a bunch of scheme theory and it had got him a Fields medal and it was this mathematics which he was interested in at the time. He wanted to formalise his big theorem, just like Hales did." I think he was more interested in formalizing things like his early work with Kapranov on higher categories, which turned out to have a mistake in it. He once told me that he wasn't interested in formalizing his proof of Bloch-Kato, because he was sure it was right. (I should have asked him at the time how he could be so sure!) Re: "The clearest evidence, in my mind, is that there is no definition of a scheme in UniMath." That's sort of accidental. In early 2014, expecting to speak at an algebraic geometry in the summer, he mentioned that one idea he had for his talk would be to formalize the definition of scheme in UniMath and speak about it. I think he was distracted from that by thinking about C-systems. The UniMath project aims at formalizing all of mathematics, so the definition of scheme is one of the next things that (still) needs to be done. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/cda95637-0ab0-4897-8e38-b5ebb288a658%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1913 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-05 15:43 ` Daniel R. Grayson@ 2019-11-05 20:29 ` Yuhao Huang2019-11-06 23:59 ` Daniel R. Grayson 0 siblings, 1 reply; 32+ messages in thread From: Yuhao Huang @ 2019-11-05 20:29 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 4927 bytes --] > > He once told me that he wasn't interested in formalizing his proof of > Bloch-Kato, because he was sure it was right. (I should have asked him at > the time how he could be so sure!) > Oh this is interesting... do you remember when this conversation was happening? Because in these slides ( https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_09_Bernays_3%20presentation.pdf) he said "Next year I am starting a project of univalent formalization of my proof of Milnor’s Conjecture using this formalization of set theory as the starting point." (Page 11) 在 2019年11月5日星期二 UTC-8上午7:43:06，Daniel R. Grayson写道： > > Re: "To get back to the original question, my understanding was that > Voevodsky had done a bunch of scheme theory and it had got him a Fields > medal and it was this mathematics which he was interested in at the time. > He wanted to formalise his big theorem, just like Hales did." > > I think he was more interested in formalizing things like his early work > with Kapranov on higher categories, which turned out to have a mistake in > it. He once told me that he wasn't interested in formalizing his proof of > Bloch-Kato, because he was sure it was right. (I should have asked him at > the time how he could be so sure!) > > Re: "The clearest evidence, in my mind, is that there is no definition of > a scheme in UniMath." > > That's sort of accidental. In early 2014, expecting to speak at an > algebraic geometry in the summer, he mentioned that one idea he had for his > talk would be to formalize the definition of scheme in UniMath and speak > about it. I think he was distracted from that by thinking about > C-systems. The UniMath project aims at formalizing all of mathematics, so > the definition of scheme is one of the next things that (still) needs to be > done. > 在 2019年11月5日星期二 UTC-8上午7:43:06，Daniel R. Grayson写道： > > Re: "To get back to the original question, my understanding was that > Voevodsky had done a bunch of scheme theory and it had got him a Fields > medal and it was this mathematics which he was interested in at the time. > He wanted to formalise his big theorem, just like Hales did." > > I think he was more interested in formalizing things like his early work > with Kapranov on higher categories, which turned out to have a mistake in > it. He once told me that he wasn't interested in formalizing his proof of > Bloch-Kato, because he was sure it was right. (I should have asked him at > the time how he could be so sure!) > > Re: "The clearest evidence, in my mind, is that there is no definition of > a scheme in UniMath." > > That's sort of accidental. In early 2014, expecting to speak at an > algebraic geometry in the summer, he mentioned that one idea he had for his > talk would be to formalize the definition of scheme in UniMath and speak > about it. I think he was distracted from that by thinking about > C-systems. The UniMath project aims at formalizing all of mathematics, so > the definition of scheme is one of the next things that (still) needs to be > done. > 在 2019年11月5日星期二 UTC-8上午7:43:06，Daniel R. Grayson写道： > > Re: "To get back to the original question, my understanding was that > Voevodsky had done a bunch of scheme theory and it had got him a Fields > medal and it was this mathematics which he was interested in at the time. > He wanted to formalise his big theorem, just like Hales did." > > I think he was more interested in formalizing things like his early work > with Kapranov on higher categories, which turned out to have a mistake in > it. He once told me that he wasn't interested in formalizing his proof of > Bloch-Kato, because he was sure it was right. (I should have asked him at > the time how he could be so sure!) > > Re: "The clearest evidence, in my mind, is that there is no definition of > a scheme in UniMath." > > That's sort of accidental. In early 2014, expecting to speak at an > algebraic geometry in the summer, he mentioned that one idea he had for his > talk would be to formalize the definition of scheme in UniMath and speak > about it. I think he was distracted from that by thinking about > C-systems. The UniMath project aims at formalizing all of mathematics, so > the definition of scheme is one of the next things that (still) needs to be > done. > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/0ef61665-eafd-40a0-8592-11bdd277d10b%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 5943 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-04 18:42 ` Kevin Buzzard ` (2 preceding siblings ...) 2019-11-05 15:43 ` Daniel R. Grayson@ 2019-11-05 23:14 ` Martín Hötzel Escardó2019-11-06 0:06 ` Stefan Monnier 3 siblings, 1 reply; 32+ messages in thread From: Martín Hötzel Escardó @ 2019-11-05 23:14 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1901 bytes --] On Monday, 4 November 2019 18:43:08 UTC, Kevin Buzzard wrote: > > It is exactly the interaction between constructivism and univalence which > I do not understand well, and I think that a very good way to investigate > it would be to do some highly non-constructive modern mathematics in a > univalent type theory > Regarding *old* mathematics, you have the well-ordering principle proved in UniMath (from the axiom of choice, of course). Regarding your doubt about the interaction, we have that univalence is orthogonal to constructivism. In fact, univalence is not *inherently* constructive. It was hard work to find a constructive interpretation of univalence (which happens to rely on cubical sets as in homotopy theory). In particular (even if I lam fond of constructive mathematics, as you know), I work with univalence axiomatically, as a black box, rather than as a construction, in my (formal and informal) mathematical developments. And I do prefer to work with univalence-as-a-specification rather than univalence-as-a-construction. There is nothing inherently constructive about univalence. There is no a priori interaction between univalence and constructivism. There is only an a posteriori interaction, constructed by some of the constructively minded members of this list. The constructivity of univalence was an open problem for a number of year, and I would say that, even if it is solved via the cubical model, it is far from being fully understood. Best, Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/cb153658-548a-4fe9-91ed-fc2e3db33723%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 2512 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-05 23:14 ` Martín Hötzel Escardó@ 2019-11-06 0:06 ` Stefan Monnier2019-11-11 18:26 ` Licata, Dan 0 siblings, 1 reply; 32+ messages in thread From: Stefan Monnier @ 2019-11-06 0:06 UTC (permalink / raw) To: Martín Hötzel Escardó;+Cc:Homotopy Type Theory > members of this list. The constructivity of univalence was an open problem > for a number of year, and I would say that, even if it is solved via the > cubical model, it is far from being fully understood. In my case, I still find it odd in a situation such as: data Foo : Set -> Set where bar : Foo UnaryNat since transport supposedly allows us to take a proof of equivalence between UnaryNat and BinaryNat and turn a `bar` into something of type `Foo BinaryNat` although I can't see any way to directly construct an object of this type. Stefan ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-05 20:29 ` Yuhao Huang@ 2019-11-06 23:59 ` Daniel R. Grayson0 siblings, 0 replies; 32+ messages in thread From: Daniel R. Grayson @ 2019-11-06 23:59 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1139 bytes --] Sorry, at this point I don't remember precisely. On Tuesday, November 5, 2019 at 2:29:56 PM UTC-6, Yuhao Huang wrote: > > He once told me that he wasn't interested in formalizing his proof of >> Bloch-Kato, because he was sure it was right. (I should have asked him at >> the time how he could be so sure!) >> > > Oh this is interesting... do you remember when this conversation was > happening? Because in these slides ( > https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_09_Bernays_3%20presentation.pdf) > he said "Next year I am starting a project of univalent formalization of my > proof of Milnor’s Conjecture using this formalization of set theory as the > starting point." (Page 11) > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/3811fd43-0b84-4ac0-adcd-de638ae3ad57%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 2425 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*2019-11-06 0:06 ` Stefan MonnierRe: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?@ 2019-11-11 18:26 ` Licata, Dan0 siblings, 0 replies; 32+ messages in thread From: Licata, Dan @ 2019-11-11 18:26 UTC (permalink / raw) To: Stefan Monnier;+Cc:Martín Hötzel Escardó, Homotopy Type Theory For inductive families, one thing you can do is to think of them in terms of the translation to parametrized inductive types and identity types, so > data Foo (A : Set) : Set where > bar : Id U A UnaryNat -> Foo A in which case bar applied to the Id U BinaryNat UnaryNat that you get from univalence gives a Foo BinaryNat. A related perspective is to think of some transports as additional constructors for inductive families; see e.g. this approach to inductive families in cubical type theory https://www.cs.cmu.edu/~ecavallo/works/popl19.pdf -Dan > On Nov 5, 2019, at 7:06 PM, Stefan Monnier <monnier@iro.umontreal.ca> wrote: > >> members of this list. The constructivity of univalence was an open problem >> for a number of year, and I would say that, even if it is solved via the >> cubical model, it is far from being fully understood. > > In my case, I still find it odd in a situation such as: > > data Foo : Set -> Set where > bar : Foo UnaryNat > > since transport supposedly allows us to take a proof of equivalence > between UnaryNat and BinaryNat and turn a `bar` into something of type > `Foo BinaryNat` although I can't see any way to directly construct an > object of this type. > > > Stefan > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/0CC0B8D7-3D66-42AD-A2D7-3B897A432B36%40wesleyan.edu. ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-04 23:20 ` Nicolas Alexander Schmidt@ 2019-11-24 18:11 ` Kevin Buzzard2019-11-26 0:25 ` Michael Shulman 2019-11-27 20:21 ` Nicolas Alexander Schmidt 0 siblings, 2 replies; 32+ messages in thread From: Kevin Buzzard @ 2019-11-24 18:11 UTC (permalink / raw) To: Nicolas Alexander Schmidt;+Cc:Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 8277 bytes --] > Kevin, I would like to second Michael's interest in seeing these 20 > commutative diagrams. Moreover, I'd also be very interested in seeing > your "spaghetti code" (quote from the slides of your Big Proof talk): it > seems it should be informative to see where your initial approach went > wrong, and how much these problems and their solution had anything to do > at all with the formal system you were working in. Are your original > files perhaps available somewhere? > Sorry for the delay. My original repo with a "bad" theorem is here: https://github.com/kbuzzard/lean-stacks-project The bad theorem is this: https://stacks.math.columbia.edu/tag/00EJ The problem is that the rings denoted R_{f_i} (localisations of rings) are typically defined to mathematicians as "this explicit construction here" as opposed to "the unique up to unique isomorphism ring having some explicit property" and, as a mathematician, I formalised (or more precisely got Imperial College maths undergraduates Chris Hughes and Kenny Lau to formalise) the explicit construction of the localisation and then the explicit theorem as stated in the stacks project, not understanding at the time that this would lead to trouble. When I came to apply it, I ran into the issue that on this page https://stacks.math.columbia.edu/tag/01HR we have the quote: "If f, g in R are such that D(f)=D(g), then by Lemma 26.5.1 there are canonical maps M_f->M_g and M_g->M_f which are mutually inverse. Hence [we can regard M_f and M_g as equal]". This is a typical mathematician's usage of the word "canonical" -- it means "I give you my mathematician's guarantee that I will never do anything to M_f which won't work in exactly the same way as M_g so you can replace one by the other and I won't mind". As I explained earlier, by the time I noticed this subtlety it was too late, and this led to this horrorshow: https://github.com/kbuzzard/lean-stacks-project/blob/7c2438e441547da6a5786a9a427fd78cbc407fa9/src/canonical_isomorphism_nonsense.lean#L268 plus the lines following, all of which is applied here https://github.com/kbuzzard/lean-stacks-project/blob/595aa1d6c5ce5a6fa0259c5a0a2226a91b07d96e/src/tag01HR.lean#L208 . That last link is justifying a whole bunch of rewrites along canonical isomorphisms. These were the general lemmas I needed to prove that if A -> B was a map, and if A was canonically isomorphic to A' and if B was canonically isomorphic to B' and A' -> B' was the corresponding map, then the image of A was canonically isomorphic to the image of A' etc, all in some very specific situation where "canonically isomorphic" was typically replaced by "unique isomorphism satisfying this list of properties". Note that this is crappy old code written by me when I had no idea what I was doing. One very interesting twist was this: the universal property of localisation for the localised ring R_f is a statement which says that under certain circumstances there is a unique ring homomorphism from R_f; however in https://stacks.math.columbia.edu/tag/00EJ the map beta in the statement of the lemma is *not* a ring homomorphism and so a naive application the universal property was actually *not enough*! One has to reformulate the lemma in terms of equalisers of ring homomorphisms and remove mention of beta. None of this is mentioned in the stacks project website because we are covered by the fact that everything is "canonical" so it's all bound to work -- and actually this is *true* -- we are very good at using this black magic word. All of this is fixed in Ramon Mir's MSc project https://github.com/ramonfmir/lean-scheme and the explanations of how it was fixed are in his write-up here https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf Briefly, one crucial input was that the localisation map R -> R_f could be characterised up to unique isomorphism in the category of R-algebras by something far more concrete than the universal property, and Ramon used this instead. In HoTT one might naively say that these problems would not arise because isomorphic things are equal. However my *current* opinion is that it is not as easy as this, because I believe that the correct "axiom" is that "canonically" isomorphic objects are equal and that the HoTT axiom is too strong. I developed some rather primitive tools to rewrite certain statements along certain kinds of isomorphisms with some naturality properties, and mathematicians would be happy with these ideas. I can quite believe that if you stick to homotopy types with the model in your mind as being topological spaces up to homotopy then the HoTT axiom is perfect. However there are things other than topological spaces in mathematics, for example commutative rings, and in my mind the HoTT axiom just looks weird and wrong in ring theory, and I expect it to backfire when HoTT people start doing some serious ring theory. I might be wrong. Part of me hopes I'm wrong, in fact. But this will remain my opinion until someone comes along and formalises the definition of a scheme in one of the HoTT theories and proves the "theorem" that an affine scheme is a scheme (I write "theorem" in quotes because it is a construction, not a theorem). I had the pleasure of meeting Thorsten Altenkirch earlier this week and I asked him why this had not been done yet, and he told me that they were just waiting for the right person to come along and do it. A year or so ago I was of the opinion that more mathematicians should be using Lean but now I have come to the conclusion that actually more mathematicians should be engaging with *all* of the theorem provers, so we can find out which provers are the most appropriate for which areas. By "mathematicians" here I really mean my ugly phrase "proper mathematicians", i.e. people doing algebra/number theory/geometry/topology etc, people who have absolutely no idea what a type is and would even struggle to list the axioms of set theory. These people with their "canonical" constructions (a phrase which has no meaning) are the problem, and they're very hard to reach because currently these systems offer them nothing they need. I wrote a silly game http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ to help my 1st years revise for my exam (and the game takes things much further than the contents of the course), and I'm writing a real number game too, to help my 1st years revise analysis for their January exam. It would not be hard to write analogous such games in one of the HoTT theories, I would imagine. From what I have seen, it seems to me that Isabelle is a fabulous tool for classical analysis, Coq is great for finite group theory, the Kepler conjecture is proved in other HOL systems, and the HoTT systems are great for the theory of topological spaces up to homotopy. But number theory has been around for millennia and unfortunately uses analysis, group theory and topological spaces, and I want one system which can do all of them. I think that we can only find out the limitations of these systems by doing a whole bunch of "proper mathematics" in all of them. I think it's appalling that none of them can even *state* the Hodge conjecture, for example. For me, that is a very simple reason for a "proper mathematician" to immediately reject all of them in 2019. But I digress. Kevin > > > -- > > Nicolas > > > > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinity.xyz > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb2AoMWBeCCJ5B8%3DDfa8UgmO1vbWf7a%3DdvfRqTFTdu61qA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 10887 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-24 18:11 ` Kevin Buzzard@ 2019-11-26 0:25 ` Michael Shulman2019-11-26 8:08 ` Ulrik Buchholtz 2019-11-26 19:14 ` Martín Hötzel Escardó 2019-11-27 20:21 ` Nicolas Alexander Schmidt 1 sibling, 2 replies; 32+ messages in thread From: Michael Shulman @ 2019-11-26 0:25 UTC (permalink / raw) To: Kevin Buzzard;+Cc:Homotopy Type Theory Thanks for sharing the details, Kevin! On Sun, Nov 24, 2019 at 10:11 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > In HoTT one might naively say that these problems would not arise because isomorphic things are equal. This thought is indeed too naive, but, I think, not for the reason you give. In a non-univalent type theory, you have to prove manually that everything in sight respects isomorphisms. This is I think the point you were making about why the original approach got so messy. HoTT does solve this problem: because isomorphisms can be made into equalities, everything automatically respects isomorphisms. The problem is that in traditional "Book" HoTT, when you make an isomorphism into an equality, the original isomorphism is only remembered "up to homotopy", and then when you apply the transport across that equality (i.e. you use the fact that everything automatically respects it), it takes work to prove that what you get out in fact coincides with what you thought it was supposed to be (i.e. the result of actually applying the isomorphism you started by defining). In fact, dealing with these "univalence-redexes" is so painful that when formalizing mathematics in Book HoTT we (at least, in the HoTT/Coq library) generally avoid making isomorphisms into equalities as much as possible! The only place you might get some mileage is when, as Valery pointed out, what you're transporting is the mere truth of a proposition and so it doesn't matter what the "result" of the transport is. So while it might be interesting to try to formalize schemes in Book HoTT, I wouldn't expect much improvement, and it's not a project I would wish on anyone. What I do think would be worth doing and comparing would be to formalize schemes in some kind of cubical type theory. In that case, univalence actually computes and so you can hope that the proof assistant can actually recover the original isomorphism for you automatically. This may not be quite true (https://groups.google.com/d/topic/homotopytypetheory/wCU0V8RD1LQ/discussion) but it's much closer to true, and I think it would be extremely interesting to formalize schemes in a cubical type theory and compare to your developments. In a nutshell, one could say that the composition algorithms of cubical type theory are a generic implementation of the fact that everything definable in type theory respects isomorphisms, so that essentially all of the nasty lemmas should be proven for you already -- with, moreover, the proofs that you would have given, rather than (as in Book HoTT) a proof that isn't very useful because it takes a lot of effort to extract the "correct" proof. > However my *current* opinion is that it is not as easy as this, because I believe that the correct "axiom" is that "canonically" isomorphic objects are equal and that the HoTT axiom is too strong. This doesn't really make sense to me; I can't figure out what you mean by "too strong". It's certainly not inconsistent, since we have semantic models; in particular, schemes defined in HoTT would specialize in the simplicial set model to the classical notion of scheme. And I can't imagine any way that the presence of univalence could "get in the way" or "backfire". Usually when people say that univalence sounds "wrong", it's because they're thinking of "equality" as a substitutive mere property and "isomorphic types as equal" as somehow collapsing to a categorical skeleton, which is of course a misconception -- HoTT instead expands the notion of "equality" to essentially mean "isomorphism" and requires transporting along it as a nontrivial action. I doubt that that's what you have in mind, but maybe you could explain what you do mean? > By "mathematicians" here I really mean my ugly phrase "proper mathematicians", i.e. people doing algebra/number theory/geometry/topology etc, people who have absolutely no idea what a type is and would even struggle to list the axioms of set theory. It would be nice if there were a phrase for this that didn't sound insulting to us "improper" mathematicians. Mac Lane's similar phrase "working mathematician" is not really any more flattering to the "non-working" mathematicians. (-: Mike -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQz3jn5jcjbeeK%2BG2dJ_n_AuZT43pSQ%2Bq5z8Roq_YFzQpw%40mail.gmail.com. ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-26 0:25 ` Michael Shulman@ 2019-11-26 8:08 ` Ulrik Buchholtz2019-11-26 19:14 ` Martín Hötzel Escardó 1 sibling, 0 replies; 32+ messages in thread From: Ulrik Buchholtz @ 2019-11-26 8:08 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 2008 bytes --] On Tuesday, November 26, 2019 at 1:25:37 AM UTC+1, Michael Shulman wrote: > > On Sun, Nov 24, 2019 at 10:11 AM Kevin Buzzard > > However my *current* opinion is that it is not as easy as this, because > I believe that the correct "axiom" is that "canonically" isomorphic objects > are equal and that the HoTT axiom is too strong. > > This doesn't really make sense to me; I can't figure out what you mean > by "too strong". > Of course I agree with Mike that univalence is not “too strong”: it merely implements the mathematically right notion of identity for types and other structures built from types, such as rings, etc. But if I may venture a guess, I'd say that Kevin wants a “canonical reflection rule”: canonical identifications should correspond to judgmental equalities. We've had some discussions before about the underlying meaning of judgmental equality (invoking Frege's Sinn/Bedeutung distinction among other ideas), but I don't know whether we tried saying judgmental/definitional equality should include canonical equality, whatever that is. This might be really useful, but I think we're still some ways off before we can implement this idea. The first question is whether “all diagrams of canonical identifications commute”. (Besides the obvious question of defining canonical identifications in the first place :-) But the adventurous can start by playing around by adding canonical identities as rewriting rules in Agda: see Jesper Cockx' recent blog post: https://jesper.sikanda.be/posts/hack-your-type-theory.html Ulrik -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/2f61877b-b4ef-405a-99cc-85da227c70bc%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 2645 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-26 0:25 ` Michael Shulman 2019-11-26 8:08 ` Ulrik Buchholtz@ 2019-11-26 19:14 ` Martín Hötzel Escardó2019-11-26 19:53 ` Kevin Buzzard 2019-11-27 10:12 ` Thorsten Altenkirch 1 sibling, 2 replies; 32+ messages in thread From: Martín Hötzel Escardó @ 2019-11-26 19:14 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 5058 bytes --] On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: > > HoTT instead expands the notion of "equality" to > essentially mean "isomorphism" and requires transporting along it as a > nontrivial action. I doubt that that's what you have in mind, but > maybe you could explain what you do mean? > I think terminology and notation alone cause a lot of confusion (and I have said this many times in this list in the past, before Kevin joined in). Much of the disagreement is not a real disagreement but a misunderstanding. * In HoTT, or in univalent mathematics, we use the terminology "equals" and the notation "=" for something that is not the same notion as in "traditional mathematics". * Before the univalence axiom, we had Martin-Loef's identity type. * It was *intended* to capture equality *as used by mathematicians* (constructive or not). * But it didn't. Hofmann and Streicher proved that. * The identity type captures something else. It certainly doesn't capture truth-valued equality by default. In particular, Voevosdky showed that it captures isomorphism of sets, and more generality equivalence of ∞-groupoids. But this is distorting history a bit. In the initial drafts of his "homotopy lambda calculus", he tried come up with a new construction in type theory to capture equivalence. It was only later that he found out that what he needed was precisely Martin-Loef's identity type. * So writing "x = y" for the identity type is a bit perverse. People may say, and they have said "but there is no other sensible notion of equality for such type theories. That may be so, but because, in any case, *it is not the same notion of equality*, we should not use the same symbol. * Similarly, writing "X ≃ Y" is a bit perverse, too. In truth-valued mathematics, "X ≃ Y" is most of the time intended to be truth-valued, not set-valued. (Exception: category theory. E.g. we write a long chain of isomorphisms to establish that two objects are isomorphic. Then we learn that the author of such a proof was not interested in the existence of an isomorphism, but instead to provide an example. Such a proof/construction is usually concluded by saying something like "by chasing the isomorphism, we see that we can take [...] as our desired isomorphism.) * With the above out of the way, we can consider the imprecise slogan "isomorphic types are equal". The one thing that the univalence axiom doesn't say is that isomorphic type are equal. What it does say is that the *identity type* Id X Y is in canonical bijection with the type X ≃ Y of equivalences. * What is the effect of this? - That the identity type behaves like isomorphism, rather than like equality. - And that isomorphism behaves a little bit like equality. The important thing above is "a little bit". In particular, we cannot *substitute* things by isomorphic things. We can only *transport* them (just like things work as usual with isomorphisms). * Usually, the univalence axioms is expressed as a relation between equality and isomorphism. Where by equality we don't mean equality but instead the identity type. A way to avoid these terminological problems is to formulate univalence as a property of isomorphisms, or more precisely equivalences. To show that all equivalences satisfy a given property, it is enough to prove that all the identity equivalence between any two types have this property. * So, as Mike says above, most of the time we can work with type equivalence rather than "type equality". And I do too. Something that is not well explained at all in the literature is when and how the univalence axiom *actually makes a difference*. (I guess this is not well understood. I used to thing that the univalence axioms makes a difference only for types that are not sets. But actually, for example, the univalence axiom is needed (in the absence of the K axiom) to prove that the type of ordinals is a set.) * One example: object classifiers, subtype classifiers, ... * Sometimes the univalence axiom may be *convenient* but *not needed*. I guess that Kevin is, in particular, saying precisely that. In all cases where he needs to transport constructions along isomorphisms, he is confident that this can be done without univalence. And I would agree with this assessment. Best, Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 6998 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-26 19:14 ` Martín Hötzel Escardó@ 2019-11-26 19:53 ` Kevin Buzzard2019-11-26 20:40 ` Martín Hötzel Escardó 2019-11-26 22:18 ` Michael Shulman 2019-11-27 10:12 ` Thorsten Altenkirch 1 sibling, 2 replies; 32+ messages in thread From: Kevin Buzzard @ 2019-11-26 19:53 UTC (permalink / raw) To: Martín Hötzel Escardó;+Cc:Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 9223 bytes --] Nicolas originally asked "So, to put this into one concrete question, how (if at all) is HoTT-Coq more practical than Mizar for the purpose of formalizing mathematics, outside the specific realm of synthetic homotopy theory?" One issue with this question is that different people mean different things by "mathematics". As someone who was until recently an outsider to formalising but very much a "working mathematician", I think I've made it pretty clear on this forum and others that for the majority of people in e.g. my maths department, they would say that none of the systems have really got anywhere concerning modern day mathematics, which is the kind of mathematics that the majority of mathematicians working in maths departments are interested in. This is a dismal state of affairs and one which I would love to help change, but it needs a cultural change within mathematics departments. The Mizar stuff I've seen has mostly been undergraduate level mathematics. UniMath seems to be a massive amount of category theory and not much undergraduate level mathematics at all. On the other hand, "there is a lot more category theory in the HoTT systems than in Mizar, so maybe Hott-Coq is more practical than Mizar for category theory" might be an answer to the original question. I'm interested in algebraic geometry, and in algebraic geometry there is this convention (explicitly flagged in Milne's book on etale cohomology) that the notation for "canonical isomorphism" (whatever that means) is "=". One can call this "mathematical equality" and it comes with a warning that it is not well-defined. I think one reason it's a challenge to formalise modern algebraic geometry is that none of the systems seem to have this kind of equality (perhaps because all of the systems demand well-defined definitions!). What I meant by my earlier post was that the `=` I have run into in Lean's type theory is too weak (canonically isomorphic things can't be proved to be equal) but the one I have run into in HoTT seems too strong (non-canonically isomorphic things are equal). It would not surprise me if different areas of mathematics had different concepts of equality. Mathematicians seem to use the concept very fluidly. Maybe it is the case that the areas where "mathematical equality" is closer to e.g. Lean's `=` or Mizar's `=` or UniMath's `=` or Isabelle/HOL's `=` or whatever, will find that formalising goes more easily in Lean's type theory/Mizar/HoTT/HOL or whatever. The biggest problem with this conjecture is that equality is mostly a cut-and-dried thing at undergraduate level, and there is not enough harder maths formalised in any of these systems (obviously there are several monumental theorems but I'm dreaming about far greater things) for us to start to check. Note that people like Riemann had no idea about set theory but did a lot of complex analysis, and he really only needed to worry about equality of complex numbers and equality of functions from the complexes to the complexes, so I don't think it's a coincidence that a whole bunch of complex analysis is done in Isabelle/HOL, which seems to me to be the "simplest logic" of the lot. Probably all the systems model this equality well. Kevin On Tue, 26 Nov 2019 at 19:14, Martín Hötzel Escardó < escardo.martin@gmail.com> wrote: > > > On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: >> >> HoTT instead expands the notion of "equality" to >> essentially mean "isomorphism" and requires transporting along it as a >> nontrivial action. I doubt that that's what you have in mind, but >> maybe you could explain what you do mean? >> > > I think terminology and notation alone cause a lot of confusion (and I > have said this many times in this list in the past, before Kevin joined > in). > > Much of the disagreement is not a real disagreement but a > misunderstanding. > > * In HoTT, or in univalent mathematics, we use the terminology > "equals" and the notation "=" for something that is not the same > notion as in "traditional mathematics". > > * Before the univalence axiom, we had Martin-Loef's identity type. > > * It was *intended* to capture equality *as used by mathematicians* > (constructive or not). > > * But it didn't. Hofmann and Streicher proved that. > > * The identity type captures something else. > > It certainly doesn't capture truth-valued equality by default. > > In particular, Voevosdky showed that it captures isomorphism of > sets, and more generality equivalence of ∞-groupoids. > > But this is distorting history a bit. > > In the initial drafts of his "homotopy lambda calculus", he tried > come up with a new construction in type theory to capture > equivalence. > > It was only later that he found out that what he needed was > precisely Martin-Loef's identity type. > > * So writing "x = y" for the identity type is a bit perverse. > > People may say, and they have said "but there is no other sensible > notion of equality for such type theories. > > That may be so, but because, in any case, *it is not the same > notion of equality*, we should not use the same symbol. > > * Similarly, writing "X ≃ Y" is a bit perverse, too. > > In truth-valued mathematics, "X ≃ Y" is most of the time intended > to be truth-valued, not set-valued. > > (Exception: category theory. E.g. we write a long chain of > isomorphisms to establish that two objects are isomorphic. Then we > learn that the author of such a proof was not interested in the > existence of an isomorphism, but instead to provide an > example. Such a proof/construction is usually concluded by saying > something like "by chasing the isomorphism, we see that we can take > [...] as our desired isomorphism.) > > > * With the above out of the way, we can consider the imprecise slogan > "isomorphic types are equal". > > The one thing that the univalence axiom doesn't say is that > isomorphic type are equal. > > What it does say is that the *identity type* Id X Y is in canonical > bijection with the type X ≃ Y of equivalences. > > * What is the effect of this? > > - That the identity type behaves like isomorphism, rather than like > equality. > > - And that isomorphism behaves a little bit like equality. > > The important thing above is "a little bit". > > In particular, we cannot *substitute* things by isomorphic > things. We can only *transport* them (just like things work as > usual with isomorphisms). > > * Usually, the univalence axioms is expressed as a relation between > equality and isomorphism. > > Where by equality we don't mean equality but instead the identity > type. > > A way to avoid these terminological problems is to formulate > univalence as a property of isomorphisms, or more precisely > equivalences. > > To show that all equivalences satisfy a given property, it is > enough to prove that all the identity equivalence between any two > types have this property. > > * So, as Mike says above, most of the time we can work with type > equivalence rather than "type equality". And I do too. > > Something that is not well explained at all in the literature is > when and how the univalence axiom *actually makes a difference*. > > (I guess this is not well understood. I used to thing that the > univalence axioms makes a difference only for types that are not > sets. But actually, for example, the univalence axiom is needed (in > the absence of the K axiom) to prove that the type of ordinals is a > set.) > > * One example: object classifiers, subtype classifiers, ... > > * Sometimes the univalence axiom may be *convenient* but *not needed*. > > I guess that Kevin is, in particular, saying precisely that. In all > cases where he needs to transport constructions along isomorphisms, > he is confident that this can be done without univalence. And I > would agree with this assessment. > > Best, > Martin > > > > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84aTxLT0kwd5syASy31Aw%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 11645 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-26 19:53 ` Kevin Buzzard@ 2019-11-26 20:40 ` Martín Hötzel Escardó2019-11-26 22:18 ` Michael Shulman 1 sibling, 0 replies; 32+ messages in thread From: Martín Hötzel Escardó @ 2019-11-26 20:40 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1594 bytes --] On Tuesday, 26 November 2019 19:53:19 UTC, Kevin Buzzard wrote: > > What I meant by my earlier post was that the `=` I have run into in Lean's > type theory is too weak (canonically isomorphic things can't be proved to > be equal) but the one I have run into in HoTT seems too strong > (non-canonically isomorphic things are equal). > Given a *specific* isomorphism, in HoTT you get a *specific* element of the identity type. Let me say this explicitly: equality in HoTT is not truth-valued. It collects all the possible ways to identify things. In the case of equality of types, the identity type collects the equivalences between them (rather than being the truth value expressing whether they are equivalent). In fact, canonicity is at the heart of the univalence axiom: there is a canonical one-to-one correspondence between elements of the equality type (i.e. the identity type) and elements of the types of equivalences. So, the univalence axiom just says that the elements of the good, old identity type can be understood to be precisely the equivalences. You may wonder what the bonus of this is. This is the content of my last two bullet points in my message. Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/77829d67-ed64-43eb-aaf0-d673df419080%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 2231 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-26 19:53 ` Kevin Buzzard 2019-11-26 20:40 ` Martín Hötzel Escardó@ 2019-11-26 22:18 ` Michael Shulman2019-11-27 0:16 ` Joyal, André ` (2 more replies) 1 sibling, 3 replies; 32+ messages in thread From: Michael Shulman @ 2019-11-26 22:18 UTC (permalink / raw) To: Kevin Buzzard;+Cc:Martín Hötzel Escardó, Homotopy Type Theory Personally, I'm doubtful that one can ascribe any precise meaning to "canonical isomorphism", and therefore doubtful that one will be able to implement a computer proof assistant that can distinguish a "canonical isomorphism" from an arbitrary one. It's certainly worth thinking about, but my personal opinion is that instead of designing a proof assistant to match the way mathematicians think about "canonical isomorphisms", mathematicians are going to need to change the way they think. But it's just a question of going all the way down a road that they've already taken one step along. In formal systems like ZFC and Lean, almost no isomorphisms are equalities. Being willing to treat "canonical" isomorphisms as equalities is a first step into the brave new world of homotopy theory and higher category theory, but it's hard to find a place to stand when you've only taken that one step. In trying to make things precise, I think one feels inexorably pulled to the more consistent, and formalizable, position that *all* isomorphisms should be treated as equalities. It's not the same notion of equality, as Martin says, but it's a better replacement for it, which in particular can do everything that the old notion of equality could do when used "correctly" (e.g. equality of numbers and functions). On Tue, Nov 26, 2019 at 11:53 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > Nicolas originally asked > > "So, to put this into one concrete question, how (if at all) is HoTT-Coq > more practical than Mizar for the purpose of formalizing mathematics, > outside the specific realm of synthetic homotopy theory?" > > One issue with this question is that different people mean different things by "mathematics". As someone who was until recently an outsider to formalising but very much a "working mathematician", I think I've made it pretty clear on this forum and others that for the majority of people in e.g. my maths department, they would say that none of the systems have really got anywhere concerning modern day mathematics, which is the kind of mathematics that the majority of mathematicians working in maths departments are interested in. This is a dismal state of affairs and one which I would love to help change, but it needs a cultural change within mathematics departments. The Mizar stuff I've seen has mostly been undergraduate level mathematics. UniMath seems to be a massive amount of category theory and not much undergraduate level mathematics at all. On the other hand, "there is a lot more category theory in the HoTT systems than in Mizar, so maybe Hott-Coq is more practical than Mizar for category theory" might be an answer to the original question. > > I'm interested in algebraic geometry, and in algebraic geometry there is this convention (explicitly flagged in Milne's book on etale cohomology) that the notation for "canonical isomorphism" (whatever that means) is "=". One can call this "mathematical equality" and it comes with a warning that it is not well-defined. I think one reason it's a challenge to formalise modern algebraic geometry is that none of the systems seem to have this kind of equality (perhaps because all of the systems demand well-defined definitions!). What I meant by my earlier post was that the `=` I have run into in Lean's type theory is too weak (canonically isomorphic things can't be proved to be equal) but the one I have run into in HoTT seems too strong (non-canonically isomorphic things are equal). > > It would not surprise me if different areas of mathematics had different concepts of equality. Mathematicians seem to use the concept very fluidly. Maybe it is the case that the areas where "mathematical equality" is closer to e.g. Lean's `=` or Mizar's `=` or UniMath's `=` or Isabelle/HOL's `=` or whatever, will find that formalising goes more easily in Lean's type theory/Mizar/HoTT/HOL or whatever. The biggest problem with this conjecture is that equality is mostly a cut-and-dried thing at undergraduate level, and there is not enough harder maths formalised in any of these systems (obviously there are several monumental theorems but I'm dreaming about far greater things) for us to start to check. Note that people like Riemann had no idea about set theory but did a lot of complex analysis, and he really only needed to worry about equality of complex numbers and equality of functions from the complexes to the complexes, so I don't think it's a coincidence that a whole bunch of complex analysis is done in Isabelle/HOL, which seems to me to be the "simplest logic" of the lot. Probably all the systems model this equality well. > > Kevin > > > On Tue, 26 Nov 2019 at 19:14, Martín Hötzel Escardó <escardo.martin@gmail.com> wrote: >> >> >> >> On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: >>> >>> HoTT instead expands the notion of "equality" to >>> essentially mean "isomorphism" and requires transporting along it as a >>> nontrivial action. I doubt that that's what you have in mind, but >>> maybe you could explain what you do mean? >> >> >> I think terminology and notation alone cause a lot of confusion (and I >> have said this many times in this list in the past, before Kevin joined in). >> >> Much of the disagreement is not a real disagreement but a >> misunderstanding. >> >> * In HoTT, or in univalent mathematics, we use the terminology >> "equals" and the notation "=" for something that is not the same >> notion as in "traditional mathematics". >> >> * Before the univalence axiom, we had Martin-Loef's identity type. >> >> * It was *intended* to capture equality *as used by mathematicians* >> (constructive or not). >> >> * But it didn't. Hofmann and Streicher proved that. >> >> * The identity type captures something else. >> >> It certainly doesn't capture truth-valued equality by default. >> >> In particular, Voevosdky showed that it captures isomorphism of >> sets, and more generality equivalence of ∞-groupoids. >> >> But this is distorting history a bit. >> >> In the initial drafts of his "homotopy lambda calculus", he tried >> come up with a new construction in type theory to capture >> equivalence. >> >> It was only later that he found out that what he needed was >> precisely Martin-Loef's identity type. >> >> * So writing "x = y" for the identity type is a bit perverse. >> >> People may say, and they have said "but there is no other sensible >> notion of equality for such type theories. >> >> That may be so, but because, in any case, *it is not the same >> notion of equality*, we should not use the same symbol. >> >> * Similarly, writing "X ≃ Y" is a bit perverse, too. >> >> In truth-valued mathematics, "X ≃ Y" is most of the time intended >> to be truth-valued, not set-valued. >> >> (Exception: category theory. E.g. we write a long chain of >> isomorphisms to establish that two objects are isomorphic. Then we >> learn that the author of such a proof was not interested in the >> existence of an isomorphism, but instead to provide an >> example. Such a proof/construction is usually concluded by saying >> something like "by chasing the isomorphism, we see that we can take >> [...] as our desired isomorphism.) >> >> >> * With the above out of the way, we can consider the imprecise slogan >> "isomorphic types are equal". >> >> The one thing that the univalence axiom doesn't say is that >> isomorphic type are equal. >> >> What it does say is that the *identity type* Id X Y is in canonical >> bijection with the type X ≃ Y of equivalences. >> >> * What is the effect of this? >> >> - That the identity type behaves like isomorphism, rather than like >> equality. >> >> - And that isomorphism behaves a little bit like equality. >> >> The important thing above is "a little bit". >> >> In particular, we cannot *substitute* things by isomorphic >> things. We can only *transport* them (just like things work as >> usual with isomorphisms). >> >> * Usually, the univalence axioms is expressed as a relation between >> equality and isomorphism. >> >> Where by equality we don't mean equality but instead the identity >> type. >> >> A way to avoid these terminological problems is to formulate >> univalence as a property of isomorphisms, or more precisely >> equivalences. >> >> To show that all equivalences satisfy a given property, it is >> enough to prove that all the identity equivalence between any two >> types have this property. >> >> * So, as Mike says above, most of the time we can work with type >> equivalence rather than "type equality". And I do too. >> >> Something that is not well explained at all in the literature is >> when and how the univalence axiom *actually makes a difference*. >> >> (I guess this is not well understood. I used to thing that the >> univalence axioms makes a difference only for types that are not >> sets. But actually, for example, the univalence axiom is needed (in >> the absence of the K axiom) to prove that the type of ordinals is a >> set.) >> >> * One example: object classifiers, subtype classifiers, ... >> >> * Sometimes the univalence axiom may be *convenient* but *not needed*. >> >> I guess that Kevin is, in particular, saying precisely that. In all >> cases where he needs to transport constructions along isomorphisms, >> he is confident that this can be done without univalence. And I >> would agree with this assessment. >> >> Best, >> Martin >> >> >> >> >> -- >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com. > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84aTxLT0kwd5syASy31Aw%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQyAaJnLeJZHCMqWAu3f%2BOb72%2BMSSLmb8MjkBHoH05k_Rw%40mail.gmail.com. ^ permalink raw reply [flat|nested] 32+ messages in thread

*RE: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-26 22:18 ` Michael Shulman@ 2019-11-27 0:16 ` Joyal, André2019-11-27 2:28 ` Stefan Monnier 2019-11-27 1:41 ` Daniel R. Grayson 2019-11-27 8:22 ` N. Raghavendra 2 siblings, 1 reply; 32+ messages in thread From: Joyal, André @ 2019-11-27 0:16 UTC (permalink / raw) To: Michael Shulman, Kevin Buzzard Cc: Martín Hötzel Escardó, Homotopy Type Theory Dear Michael, You wrote: <<Personally, I'm doubtful that one can ascribe any precise meaning to "canonical isomorphism", and therefore doubtful that one will be able to implement a computer proof assistant that can distinguish a "canonical isomorphism" from an arbitrary one. >> The notion of canonical isomorphism depends obviously on the context. For example, the "canonical isomorphism" (AxB)xC = Ax(BxC) is likely to be the associativity isomorphism. Maybe AI (deep learning) could be trained to recognise the correct canonical isomorphism from the context (=the proof). It may automatise what is already automatic in our thinking. Best, André ________________________________________ From: homotopytypetheory@googlegroups.com [homotopytypetheory@googlegroups.com] on behalf of Michael Shulman [shulman@sandiego.edu] Sent: Tuesday, November 26, 2019 5:18 PM To: Kevin Buzzard Cc: Martín Hötzel Escardó; Homotopy Type Theory Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Personally, I'm doubtful that one can ascribe any precise meaning to "canonical isomorphism", and therefore doubtful that one will be able to implement a computer proof assistant that can distinguish a "canonical isomorphism" from an arbitrary one. It's certainly worth thinking about, but my personal opinion is that instead of designing a proof assistant to match the way mathematicians think about "canonical isomorphisms", mathematicians are going to need to change the way they think. But it's just a question of going all the way down a road that they've already taken one step along. In formal systems like ZFC and Lean, almost no isomorphisms are equalities. Being willing to treat "canonical" isomorphisms as equalities is a first step into the brave new world of homotopy theory and higher category theory, but it's hard to find a place to stand when you've only taken that one step. In trying to make things precise, I think one feels inexorably pulled to the more consistent, and formalizable, position that *all* isomorphisms should be treated as equalities. It's not the same notion of equality, as Martin says, but it's a better replacement for it, which in particular can do everything that the old notion of equality could do when used "correctly" (e.g. equality of numbers and functions). On Tue, Nov 26, 2019 at 11:53 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > Nicolas originally asked > > "So, to put this into one concrete question, how (if at all) is HoTT-Coq > more practical than Mizar for the purpose of formalizing mathematics, > outside the specific realm of synthetic homotopy theory?" > > One issue with this question is that different people mean different things by "mathematics". As someone who was until recently an outsider to formalising but very much a "working mathematician", I think I've made it pretty clear on this forum and others that for the majority of people in e.g. my maths department, they would say that none of the systems have really got anywhere concerning modern day mathematics, which is the kind of mathematics that the majority of mathematicians working in maths departments are interested in. This is a dismal state of affairs and one which I would love to help change, but it needs a cultural change within mathematics departments. The Mizar stuff I've seen has mostly been undergraduate level mathematics. UniMath seems to be a massive amount of category theory and not much undergraduate level mathematics at all. On the other hand, "there is a lot more category theory in the HoTT systems than in Mizar, so maybe Hott-Coq is more practical than Mizar for category theory" might be an answer to the original question. > > I'm interested in algebraic geometry, and in algebraic geometry there is this convention (explicitly flagged in Milne's book on etale cohomology) that the notation for "canonical isomorphism" (whatever that means) is "=". One can call this "mathematical equality" and it comes with a warning that it is not well-defined. I think one reason it's a challenge to formalise modern algebraic geometry is that none of the systems seem to have this kind of equality (perhaps because all of the systems demand well-defined definitions!). What I meant by my earlier post was that the `=` I have run into in Lean's type theory is too weak (canonically isomorphic things can't be proved to be equal) but the one I have run into in HoTT seems too strong (non-canonically isomorphic things are equal). > > It would not surprise me if different areas of mathematics had different concepts of equality. Mathematicians seem to use the concept very fluidly. Maybe it is the case that the areas where "mathematical equality" is closer to e.g. Lean's `=` or Mizar's `=` or UniMath's `=` or Isabelle/HOL's `=` or whatever, will find that formalising goes more easily in Lean's type theory/Mizar/HoTT/HOL or whatever. The biggest problem with this conjecture is that equality is mostly a cut-and-dried thing at undergraduate level, and there is not enough harder maths formalised in any of these systems (obviously there are several monumental theorems but I'm dreaming about far greater things) for us to start to check. Note that people like Riemann had no idea about set theory but did a lot of complex analysis, and he really only needed to worry about equality of complex numbers and equality of functions from the complexes to the complexes, so I don't think it's a coincidence that a whole bunch of complex analysis is done in Isabelle/HOL, which seems to me to be the "simplest logic" of the lot. Probably all the systems model this equality well. > > Kevin > > > On Tue, 26 Nov 2019 at 19:14, Martín Hötzel Escardó <escardo.martin@gmail.com> wrote: >> >> >> >> On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: >>> >>> HoTT instead expands the notion of "equality" to >>> essentially mean "isomorphism" and requires transporting along it as a >>> nontrivial action. I doubt that that's what you have in mind, but >>> maybe you could explain what you do mean? >> >> >> I think terminology and notation alone cause a lot of confusion (and I >> have said this many times in this list in the past, before Kevin joined in). >> >> Much of the disagreement is not a real disagreement but a >> misunderstanding. >> >> * In HoTT, or in univalent mathematics, we use the terminology >> "equals" and the notation "=" for something that is not the same >> notion as in "traditional mathematics". >> >> * Before the univalence axiom, we had Martin-Loef's identity type. >> >> * It was *intended* to capture equality *as used by mathematicians* >> (constructive or not). >> >> * But it didn't. Hofmann and Streicher proved that. >> >> * The identity type captures something else. >> >> It certainly doesn't capture truth-valued equality by default. >> >> In particular, Voevosdky showed that it captures isomorphism of >> sets, and more generality equivalence of ∞-groupoids. >> >> But this is distorting history a bit. >> >> In the initial drafts of his "homotopy lambda calculus", he tried >> come up with a new construction in type theory to capture >> equivalence. >> >> It was only later that he found out that what he needed was >> precisely Martin-Loef's identity type. >> >> * So writing "x = y" for the identity type is a bit perverse. >> >> People may say, and they have said "but there is no other sensible >> notion of equality for such type theories. >> >> That may be so, but because, in any case, *it is not the same >> notion of equality*, we should not use the same symbol. >> >> * Similarly, writing "X ≃ Y" is a bit perverse, too. >> >> In truth-valued mathematics, "X ≃ Y" is most of the time intended >> to be truth-valued, not set-valued. >> >> (Exception: category theory. E.g. we write a long chain of >> isomorphisms to establish that two objects are isomorphic. Then we >> learn that the author of such a proof was not interested in the >> existence of an isomorphism, but instead to provide an >> example. Such a proof/construction is usually concluded by saying >> something like "by chasing the isomorphism, we see that we can take >> [...] as our desired isomorphism.) >> >> >> * With the above out of the way, we can consider the imprecise slogan >> "isomorphic types are equal". >> >> The one thing that the univalence axiom doesn't say is that >> isomorphic type are equal. >> >> What it does say is that the *identity type* Id X Y is in canonical >> bijection with the type X ≃ Y of equivalences. >> >> * What is the effect of this? >> >> - That the identity type behaves like isomorphism, rather than like >> equality. >> >> - And that isomorphism behaves a little bit like equality. >> >> The important thing above is "a little bit". >> >> In particular, we cannot *substitute* things by isomorphic >> things. We can only *transport* them (just like things work as >> usual with isomorphisms). >> >> * Usually, the univalence axioms is expressed as a relation between >> equality and isomorphism. >> >> Where by equality we don't mean equality but instead the identity >> type. >> >> A way to avoid these terminological problems is to formulate >> univalence as a property of isomorphisms, or more precisely >> equivalences. >> >> To show that all equivalences satisfy a given property, it is >> enough to prove that all the identity equivalence between any two >> types have this property. >> >> * So, as Mike says above, most of the time we can work with type >> equivalence rather than "type equality". And I do too. >> >> Something that is not well explained at all in the literature is >> when and how the univalence axiom *actually makes a difference*. >> >> (I guess this is not well understood. I used to thing that the >> univalence axioms makes a difference only for types that are not >> sets. But actually, for example, the univalence axiom is needed (in >> the absence of the K axiom) to prove that the type of ordinals is a >> set.) >> >> * One example: object classifiers, subtype classifiers, ... >> >> * Sometimes the univalence axiom may be *convenient* but *not needed*. >> >> I guess that Kevin is, in particular, saying precisely that. In all >> cases where he needs to transport constructions along isomorphisms, >> he is confident that this can be done without univalence. And I >> would agree with this assessment. >> >> Best, >> Martin >> >> >> >> >> -- >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com. > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84aTxLT0kwd5syASy31Aw%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQyAaJnLeJZHCMqWAu3f%2BOb72%2BMSSLmb8MjkBHoH05k_Rw%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652BA70E%40Pli.gst.uqam.ca. ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-26 22:18 ` Michael Shulman 2019-11-27 0:16 ` Joyal, André@ 2019-11-27 1:41 ` Daniel R. Grayson2019-11-27 8:22 ` N. Raghavendra 2 siblings, 0 replies; 32+ messages in thread From: Daniel R. Grayson @ 2019-11-27 1:41 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 838 bytes --] On Tuesday, November 26, 2019 at 4:18:49 PM UTC-6, Michael Shulman wrote: > > Personally, I'm doubtful that one can ascribe any precise meaning to > "canonical isomorphism", > One standard example of a non-canonical isomorphism is that between a finite dimensional vector space V and its dual V', so perhaps one may define a non-canonical isomorphism to be one that one merely has, and a canonical isomorphism is one that one actually has. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/39769e9d-6de3-422b-b3f7-123dcc2f737f%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1336 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-27 0:16 ` Joyal, André@ 2019-11-27 2:28 ` Stefan Monnier0 siblings, 0 replies; 32+ messages in thread From: Stefan Monnier @ 2019-11-27 2:28 UTC (permalink / raw) To: Joyal, André Cc: Michael Shulman, Kevin Buzzard, Martín Hötzel Escardó, Homotopy Type Theory > Maybe AI (deep learning) could be trained to recognise the correct > canonical isomorphism from the context (=the proof). Can't we define it more formally as the isomorphism with the smallest proof? Stefan -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/jwvmuciqcnn.fsf-monnier%2Bdiro%40gnu.org. ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-26 22:18 ` Michael Shulman 2019-11-27 0:16 ` Joyal, André 2019-11-27 1:41 ` Daniel R. Grayson@ 2019-11-27 8:22 ` N. Raghavendra2 siblings, 0 replies; 32+ messages in thread From: N. Raghavendra @ 2019-11-27 8:22 UTC (permalink / raw) To: Homotopy Type Theory At 2019-11-26T14:18:34-08:00, Michael Shulman wrote: > Personally, I'm doubtful that one can ascribe any precise meaning to > "canonical isomorphism", and therefore doubtful that one will be able > to implement a computer proof assistant that can distinguish a > "canonical isomorphism" from an arbitrary one. I have usually assumed that canonical isomorphism meant functorial isomorphism, i.e., an isomorphism between an appropriate pair of functors (which are generally left unspecified). As has been mentioned, there is no functorial isomorphism from an arbitrary finite-dimensional vector space V to its dual, whereas the usual isomorphism from V to double dual is functorial, so the former is non-canonical, and the latter canonical. Another explanation I've often come across is that a canonical object is independent of the choices (if any) that were made in its definition. I guess the notion of independence depends on the context. Raghu. -- N. Raghavendra <raghu@hri.res.in>, http://www.retrotexts.net/ Harish-Chandra Research Institute, http://www.hri.res.in/ -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/87k17lafu9.fsf%40hri.res.in. ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-26 19:14 ` Martín Hötzel Escardó 2019-11-26 19:53 ` Kevin Buzzard@ 2019-11-27 10:12 ` Thorsten Altenkirch2019-11-27 16:37 ` Michael Shulman 1 sibling, 1 reply; 32+ messages in thread From: Thorsten Altenkirch @ 2019-11-27 10:12 UTC (permalink / raw) To: Martín Hötzel Escardó, Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 7827 bytes --] So writing "x = y" for the identity type is a bit perverse. People may say, and they have said "but there is no other sensible notion of equality for such type theories. That may be so, but because, in any case, *it is not the same notion of equality*, we should not use the same symbol. Two mathematical objects are equal if they have the same properties. This is exactly what equals means in HoTT and hence we should use the same symbol and call it equality. Everything else is confusing especially for the newcomer: “we have something in HoTT which is basically equality but we call it by a different name and we use a different symbol”??? Yes, it is different because equality of structures is not a proposition but a structure. But to insist that equality of structure is a proposition is just a confusion of conventional Mathematics. Independent of conventional Mathematics there is something like a naïve idea of equality which is preformal. And equality in HoTT is just a way to make this preformal notion precise. And why is it so strange to say there is more than one way to objects can be equal? As far is the notion of “canonical isomorphism”, Kevin is interested in, is concerned, I think this is an intensional aspect of an equality and hence not expressible within HoTT. E.g. 3+4 and 7 are the same natural number but 7 is canonical. Thorsten From: <homotopytypetheory@googlegroups.com> on behalf of Martín Hötzel Escardó <escardo.martin@gmail.com> Date: Tuesday, 26 November 2019 at 19:15 To: Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: HoTT instead expands the notion of "equality" to essentially mean "isomorphism" and requires transporting along it as a nontrivial action. I doubt that that's what you have in mind, but maybe you could explain what you do mean? I think terminology and notation alone cause a lot of confusion (and I have said this many times in this list in the past, before Kevin joined in). Much of the disagreement is not a real disagreement but a misunderstanding. * In HoTT, or in univalent mathematics, we use the terminology "equals" and the notation "=" for something that is not the same notion as in "traditional mathematics". * Before the univalence axiom, we had Martin-Loef's identity type. * It was *intended* to capture equality *as used by mathematicians* (constructive or not). * But it didn't. Hofmann and Streicher proved that. * The identity type captures something else. It certainly doesn't capture truth-valued equality by default. In particular, Voevosdky showed that it captures isomorphism of sets, and more generality equivalence of ∞-groupoids. But this is distorting history a bit. In the initial drafts of his "homotopy lambda calculus", he tried come up with a new construction in type theory to capture equivalence. It was only later that he found out that what he needed was precisely Martin-Loef's identity type. * So writing "x = y" for the identity type is a bit perverse. People may say, and they have said "but there is no other sensible notion of equality for such type theories. That may be so, but because, in any case, *it is not the same notion of equality*, we should not use the same symbol. * Similarly, writing "X ≃ Y" is a bit perverse, too. In truth-valued mathematics, "X ≃ Y" is most of the time intended to be truth-valued, not set-valued. (Exception: category theory. E.g. we write a long chain of isomorphisms to establish that two objects are isomorphic. Then we learn that the author of such a proof was not interested in the existence of an isomorphism, but instead to provide an example. Such a proof/construction is usually concluded by saying something like "by chasing the isomorphism, we see that we can take [...] as our desired isomorphism.) * With the above out of the way, we can consider the imprecise slogan "isomorphic types are equal". The one thing that the univalence axiom doesn't say is that isomorphic type are equal. What it does say is that the *identity type* Id X Y is in canonical bijection with the type X ≃ Y of equivalences. * What is the effect of this? - That the identity type behaves like isomorphism, rather than like equality. - And that isomorphism behaves a little bit like equality. The important thing above is "a little bit". In particular, we cannot *substitute* things by isomorphic things. We can only *transport* them (just like things work as usual with isomorphisms). * Usually, the univalence axioms is expressed as a relation between equality and isomorphism. Where by equality we don't mean equality but instead the identity type. A way to avoid these terminological problems is to formulate univalence as a property of isomorphisms, or more precisely equivalences. To show that all equivalences satisfy a given property, it is enough to prove that all the identity equivalence between any two types have this property. * So, as Mike says above, most of the time we can work with type equivalence rather than "type equality". And I do too. Something that is not well explained at all in the literature is when and how the univalence axiom *actually makes a difference*. (I guess this is not well understood. I used to thing that the univalence axioms makes a difference only for types that are not sets. But actually, for example, the univalence axiom is needed (in the absence of the K axiom) to prove that the type of ordinals is a set.) * One example: object classifiers, subtype classifiers, ... * Sometimes the univalence axiom may be *convenient* but *not needed*. I guess that Kevin is, in particular, saying precisely that. In all cases where he needs to transport constructions along isomorphisms, he is confident that this can be done without univalence. And I would agree with this assessment. Best, Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com?utm_medium=email&utm_source=footer>. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/F89C9786-6661-4F12-951D-3D58B1D71C6E%40nottingham.ac.uk. [-- Attachment #2: Type: text/html, Size: 20765 bytes --] ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-27 10:12 ` Thorsten Altenkirch@ 2019-11-27 16:37 ` Michael Shulman0 siblings, 0 replies; 32+ messages in thread From: Michael Shulman @ 2019-11-27 16:37 UTC (permalink / raw) To: Thorsten Altenkirch Cc: Martín Hötzel Escardó, Homotopy Type Theory I find the wide variety of opinions as to the meaning of "canonical" to be evidence for my contention that the notion is not formalizable. (-: Personally, I feel that the closest semiformal approximation to a "canonical" isomorphism is one that's declared as a coercion. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQzEF4sqoKtaRNVA_wN-vfEDV3UEzE0U1E%2B9i0jbjpHC_Q%40mail.gmail.com. ^ permalink raw reply [flat|nested] 32+ messages in thread

*Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?2019-11-24 18:11 ` Kevin Buzzard 2019-11-26 0:25 ` Michael Shulman@ 2019-11-27 20:21 ` Nicolas Alexander Schmidt1 sibling, 0 replies; 32+ messages in thread From: Nicolas Alexander Schmidt @ 2019-11-27 20:21 UTC (permalink / raw) To: Kevin Buzzard;+Cc:Homotopy Type Theory Thank you Kevin, for taking the time to write this very detailed response. After taking a look at your original approach and the improved one of your student, I am under the impression that the difficulties you encountered actually had little to do with the proof assistant you were working in. Perhaps this impression is just uninformed, and e.g. in a system based on cubical type theory these problems would disappear. Of course, the only way to tell is to go ahead and formalize this result in such a system. But to me it seems that the "commutative diagram hell" you faced really stems from an issue that already exists within mathematics, namely the two conflicting viewpoints on localization: viewing it as a property (the honest viewpoint) or viewing it as an operation (the convenient illusion). As far as I understood, in your original approach you proved the "standard affine covering lemma" (https://stacks.math.columbia.edu/tag/00EJ) under the operational viewpoint, making it nontrivial to apply this lemma to "nonstandard" localizations, whereas your student proved the lemma under the property viewpoint, i.e. for "all" localizations at the same time. To a "proper" mathematician this distinction must seem silly, and if he doesn't outright dismiss it as fruitless philosophical nonsense, he will most likely claim that one can safely pretend it doesn't exist due to "existence of canonical isomorphisms yada yada yada". And yet, even the (presumably "proper") author(s) of https://stacks.math.columbia.edu/tag/01HR somehow felt the need to justify the application of lemma 10.23.1 with a sentence like "[...] and hence we can rewrite this sequence as the sequence [...]", which seems to admit the issue. Thus instead of pathologies, one may view the difficulties arising in formalization as merely pointing out existing gaps in the proper mathematician's operational theory, that he can in principle fill out all the details in his proofs to arbitrary precision. This problem and its solution remind me of something I encountered a few years ago, when I tried to convince myself of the well-known fact that the abstract braid group B(W) := < T_w for w \in W | \ell(w) + \ell(w') = \ell(ww') \Rightarrow T_w T_{w'} = T_{ww'} > attached to a finite reflection group W can be viewed as the fundamental group of its complexified hyperplane complement X. My ambition was only to explicitly construct the map \rho: B(W) --> \pi_1(X,x_0), but even that turned out to be more difficult than expected. The first naive attempt---of writing down explicit representative paths in the classes \rho(T_w) and proving that these satisfy the "braid relations" up to homotopy---was completely impractical. In fact, even writing down representative paths seemed not merely difficult but hopeless. Eventually I realized that the solution is to attach to a generator T_w not a representative (operational viewpoint) but a canonical subspace of the path-space (property viewpoint), showing that the latter is contractible and that the collection of these subspaces satisfy the braid relations (in the obvious sense). After that realization, everything was completely straightforward. -- Nicolas Am 24.11.19 um 19:11 schrieb Kevin Buzzard: > > Kevin, I would like to second Michael's interest in seeing these 20 > commutative diagrams. Moreover, I'd also be very interested in seeing > your "spaghetti code" (quote from the slides of your Big Proof > talk): it > seems it should be informative to see where your initial approach went > wrong, and how much these problems and their solution had anything > to do > at all with the formal system you were working in. Are your original > files perhaps available somewhere? > > > Sorry for the delay. > > My original repo with a "bad" theorem is here: > > https://github.com/kbuzzard/lean-stacks-project > > The bad theorem is this: > > https://stacks.math.columbia.edu/tag/00EJ > > The problem is that the rings denoted R_{f_i} (localisations of rings) > are typically defined to mathematicians as "this explicit construction > here" as opposed to "the unique up to unique isomorphism ring having > some explicit property" and, as a mathematician, I formalised (or more > precisely got Imperial College maths undergraduates Chris Hughes and > Kenny Lau to formalise) the explicit construction of the localisation > and then the explicit theorem as stated in the stacks project, not > understanding at the time that this would lead to trouble. When I came > to apply it, I ran into the issue that on this page > > https://stacks.math.columbia.edu/tag/01HR > > we have the quote: "If f, g in R are such that D(f)=D(g), then by > Lemma 26.5.1 there are canonical maps M_f->M_g and M_g->M_f which are > mutually inverse. Hence [we can regard M_f and M_g as equal]". > > This is a typical mathematician's usage of the word "canonical" -- it > means "I give you my mathematician's guarantee that I will never do > anything to M_f which won't work in exactly the same way as M_g so you > can replace one by the other and I won't mind". > > As I explained earlier, by the time I noticed this subtlety it was too > late, and this led to this horrorshow: > > https://github.com/kbuzzard/lean-stacks-project/blob/7c2438e441547da6a5786a9a427fd78cbc407fa9/src/canonical_isomorphism_nonsense.lean#L268 > > plus the lines following, all of which is applied here > > https://github.com/kbuzzard/lean-stacks-project/blob/595aa1d6c5ce5a6fa0259c5a0a2226a91b07d96e/src/tag01HR.lean#L208 > > . That last link is justifying a whole bunch of rewrites along > canonical isomorphisms. These were the general lemmas I needed to > prove that if A -> B was a map, and if A was canonically isomorphic to > A' and if B was canonically isomorphic to B' and A' -> B' was the > corresponding map, then the image of A was canonically isomorphic to > the image of A' etc, all in some very specific situation where > "canonically isomorphic" was typically replaced by "unique isomorphism > satisfying this list of properties". Note that this is crappy old code > written by me when I had no idea what I was doing. One very > interesting twist was this: the universal property of localisation for > the localised ring R_f is a statement which says that under certain > circumstances there is a unique ring homomorphism from R_f; however in > https://stacks.math.columbia.edu/tag/00EJ the map beta in the > statement of the lemma is *not* a ring homomorphism and so a naive > application the universal property was actually *not enough*! One has > to reformulate the lemma in terms of equalisers of ring homomorphisms > and remove mention of beta. None of this is mentioned in the stacks > project website because we are covered by the fact that everything is > "canonical" so it's all bound to work -- and actually this is *true* > -- we are very good at using this black magic word. > > All of this is fixed in Ramon Mir's MSc project > > https://github.com/ramonfmir/lean-scheme > > and the explanations of how it was fixed are in his write-up here > > https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf > > Briefly, one crucial input was that the localisation map R -> R_f > could be characterised up to unique isomorphism in the category of > R-algebras by something far more concrete than the universal property, > and Ramon used this instead. > > In HoTT one might naively say that these problems would not arise > because isomorphic things are equal. However my *current* opinion is > that it is not as easy as this, because I believe that the correct > "axiom" is that "canonically" isomorphic objects are equal and that > the HoTT axiom is too strong. I developed some rather primitive tools > to rewrite certain statements along certain kinds of isomorphisms with > some naturality properties, and mathematicians would be happy with > these ideas. I can quite believe that if you stick to homotopy types > with the model in your mind as being topological spaces up to homotopy > then the HoTT axiom is perfect. However there are things other than > topological spaces in mathematics, for example commutative rings, and > in my mind the HoTT axiom just looks weird and wrong in ring theory, > and I expect it to backfire when HoTT people start doing some serious > ring theory. I might be wrong. Part of me hopes I'm wrong, in fact. > But this will remain my opinion until someone comes along and > formalises the definition of a scheme in one of the HoTT theories and > proves the "theorem" that an affine scheme is a scheme (I write > "theorem" in quotes because it is a construction, not a theorem). I > had the pleasure of meeting Thorsten Altenkirch earlier this week and > I asked him why this had not been done yet, and he told me that they > were just waiting for the right person to come along and do it. A year > or so ago I was of the opinion that more mathematicians should be > using Lean but now I have come to the conclusion that actually more > mathematicians should be engaging with *all* of the theorem provers, > so we can find out which provers are the most appropriate for which > areas. By "mathematicians" here I really mean my ugly phrase "proper > mathematicians", i.e. people doing algebra/number > theory/geometry/topology etc, people who have absolutely no idea what > a type is and would even struggle to list the axioms of set theory. > These people with their "canonical" constructions (a phrase which has > no meaning) are the problem, and they're very hard to reach because > currently these systems offer them nothing they need. I wrote a silly game > > http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ > > to help my 1st years revise for my exam (and the game takes things > much further than the contents of the course), and I'm writing a real > number game too, to help my 1st years revise analysis for their > January exam. It would not be hard to write analogous such games in > one of the HoTT theories, I would imagine. > > From what I have seen, it seems to me that Isabelle is a fabulous tool > for classical analysis, Coq is great for finite group theory, the > Kepler conjecture is proved in other HOL systems, and the HoTT systems > are great for the theory of topological spaces up to homotopy. But > number theory has been around for millennia and unfortunately uses > analysis, group theory and topological spaces, and I want one system > which can do all of them. I think that we can only find out the > limitations of these systems by doing a whole bunch of "proper > mathematics" in all of them. I think it's appalling that none of them > can even *state* the Hodge conjecture, for example. For me, that is a > very simple reason for a "proper mathematician" to immediately reject > all of them in 2019. But I digress. > > Kevin > > > > -- > > Nicolas > > > > > -- > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, > send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com > <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinity.xyz. > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/c25dfb49-6b6e-d926-f8c3-4c590ca6f507%40fromzerotoinfinity.xyz. ^ permalink raw reply [flat|nested] 32+ messages in thread

end of thread, other threads:[~2019-11-27 20:22 UTC | newest]Thread overview:32+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2019-10-27 14:41 [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Nicolas Alexander Schmidt 2019-10-27 17:22 ` Bas Spitters 2019-11-03 11:38 ` Bas Spitters 2019-11-03 11:52 ` David Roberts 2019-11-03 19:13 ` Michael Shulman 2019-11-03 19:45 ` Valery Isaev 2019-11-03 22:23 ` Martín Hötzel Escardó 2019-11-04 23:20 ` Nicolas Alexander Schmidt 2019-11-24 18:11 ` Kevin Buzzard 2019-11-26 0:25 ` Michael Shulman 2019-11-26 8:08 ` Ulrik Buchholtz 2019-11-26 19:14 ` Martín Hötzel Escardó 2019-11-26 19:53 ` Kevin Buzzard 2019-11-26 20:40 ` Martín Hötzel Escardó 2019-11-26 22:18 ` Michael Shulman 2019-11-27 0:16 ` Joyal, André 2019-11-27 2:28 ` Stefan Monnier 2019-11-27 1:41 ` Daniel R. Grayson 2019-11-27 8:22 ` N. Raghavendra 2019-11-27 10:12 ` Thorsten Altenkirch 2019-11-27 16:37 ` Michael Shulman 2019-11-27 20:21 ` Nicolas Alexander Schmidt 2019-11-04 18:42 ` Kevin Buzzard 2019-11-04 21:10 ` Michael Shulman 2019-11-04 23:26 ` David Roberts 2019-11-05 15:43 ` Daniel R. Grayson 2019-11-05 20:29 ` Yuhao Huang 2019-11-06 23:59 ` Daniel R. Grayson 2019-11-05 23:14 ` Martín Hötzel Escardó 2019-11-06 0:06 ` Stefan Monnier 2019-11-11 18:26 ` Licata, Dan 2019-11-03 7:29 ` Michael Shulman

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).