[-- Attachment #1.1: Type: text/plain, Size: 3305 bytes --] Hi from a Lean user. As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others. I have seen enough of Lean to become convinced that the pain points would be surmountable in Lean. I have seen enough of Isabelle/HOL to become skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings. I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a blessing and a curse. However I would like to know more details. I am speaking at the Big Proof conference in Edinburgh this coming Wednesday on the pain points involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT. Everyone will have a different interpretation of "modern pure mathematics" so to fix our ideas, let me say that for the purposes of this discussion, "modern pure mathematics" means the statements of the theorems publishsed by the Annals of Mathematics over the last few years, so for example I am talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the like; one can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is. If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics). Kevin Buzzard -- 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3866 bytes --]

A useful example for you might be Floris van Doorn’s formalization of the Atiyah-Hirzebruch and Serre spectral sequences for cohomology in HoTT using Lean: https://arxiv.org/abs/1808.10690 Regards, Steve > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > Hi from a Lean user. > > As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others. > > I have seen enough of Lean to become convinced that the pain points would be surmountable in Lean. I have seen enough of Isabelle/HOL to become skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings. > > I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a blessing and a curse. However I would like to know more details. I am speaking at the Big Proof conference in Edinburgh this coming Wednesday on the pain points involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT. > > Everyone will have a different interpretation of "modern pure mathematics" so to fix our ideas, let me say that for the purposes of this discussion, "modern pure mathematics" means the statements of the theorems publishsed by the Annals of Mathematics over the last few years, so for example I am talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the like; one can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is. > > If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics). > > Kevin Buzzard > > -- > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- 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/BFBE1A09-A246-4DAD-8AD2-25C3C517A7FE%40cmu.edu. For more options, visit https://groups.google.com/d/optout.

I am aware of Floris' work (which is in Lean 2, which used HoTT; Lean 3 has an impredicative Prop). My question is broader. It does not surprise me that doing homotopy theory is nice in homotopy type theory. What I am interested in is what happens when one tries to do other kinds of "normal mathematics" such as for example formalising parts of EGA. On Sat, 25 May 2019 at 11:22, Steve Awodey <awodey@cmu.edu> wrote: > > A useful example for you might be Floris van Doorn’s formalization of > the Atiyah-Hirzebruch and Serre spectral sequences for cohomology > in HoTT using Lean: > > https://arxiv.org/abs/1808.10690 > > Regards, > > Steve > > > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > > > Hi from a Lean user. > > > > As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others. > > > > I have seen enough of Lean to become convinced that the pain points would be surmountable in Lean. I have seen enough of Isabelle/HOL to become skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings. > > > > I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a blessing and a curse. However I would like to know more details. I am speaking at the Big Proof conference in Edinburgh this coming Wednesday on the pain points involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT. > > > > Everyone will have a different interpretation of "modern pure mathematics" so to fix our ideas, let me say that for the purposes of this discussion, "modern pure mathematics" means the statements of the theorems publishsed by the Annals of Mathematics over the last few years, so for example I am talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the like; one can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is. > > > > If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics). > > > > Kevin Buzzard > > > > -- > > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > -- 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/CAH52Xb3UieniG%3DvV%3DXCm8%2BEAn9%3D1Lsqq2EptRuJZXhy%2BC94pnA%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

On Sat, 25 May 2019 at 12:26, Thierry Coquand <Thierry.Coquand@cse.gu.se> wrote: > > > Some further references: > > - the UniMath library > > https://github.com/UniMath/UniMath/blob/master/UniMath/CONTENTS.md > (in particular representation of the notion of triangulated categories) Aah. So I think my question is this. The maths library for the Lean theorem prover has a bunch of MSc level algebra (localisations, completions, Noetherian rings), undergraduate level topology, but it is just beginning to develop a reasonable undergraduate level analysis library. Analysis has gone much more slowly than algebra because for some reason a bunch of complicated design decisions about partial functions had to be made, and e.g. people are still trying to figure out the best way to formalise manifolds. Lean also seems to find unbundled structures easier to work with than bundled structures, so whilst there is some category theory, it hasn't really yet found an application. I am hoping to integrate it into the work on schemes which is being done but somehow things keep being easier without it. So somehow currently the pain points seem to be getting category theory to work nicely (although this might be solvable if we try harder) and generally trying to work out how mathematicians use partial functions when talking about calculus and manifolds. I am unclear about whether these are issues intrinsic to the system or whether we are just not smart enough to know how to work the system. Conversely, in Isabelle/HOL doing real analysis is a dream, they have extensive real analysis libraries; the pain point that Lean has or might have simply isn't there, apparently. But doing schemes is painful in Isabelle/HOL, because sheaves of rings mean manipulating things which are rings, but without the typeclass system. Looking at UniMath I see a *huge* amount of category theory stuff. Then for algebra I see rings and modules, and there are things like the reals and the p-adics. What about schemes? Have people formalised schemes in UniMath? We ran into issues in Lean which needed solutions, but the pain points were just ignorance on our part (I'm a mathematician, and I needed to learn what type theory was). Real analysis seems to be easier to do in simple type theory than Lean's dependent type theory. How would this look in UniMath? This viewpoint that a type is a "space" rather than a "set" -- it's going to make some things easier, and some things harder. What does it make harder? Because propositions are subsingletons in Lean, and equality is a proposition, types have a much more set-ish feel to them. > > -Voevodsky’s paper > > https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0960129514000577 Voevodsky says in this paper "we come to the view that not only homotopy theory but the whole of Mathematics is the study of structures on homotopy types". On the other hand, if you talk to someone like Larry Paulson, he would tell you that simple type theory is enough to do all (pure) mathematics, and if you talk to one of the set theorists in Berkeley they would no doubt tell you that ZFC set theory is enough to do all mathematics, except for perhaps some bits where it's more convenient to have some large cardinals. All of these views are correct in some sense, but they are all hiding the fact that actually *some* mathematics is quite hard to do in the system preferred by one person, and turns out to be much easier if it's done in one of the other systems. For example schemes are relatively painless in Lean's dependent type theory, but would be painful in Isabelle/HOL. On the other hand real analysis is relatively painless in Isabelle/HOL and yet in Lean we still have not proved that the derivative of sin is cos. How does UniMath fit into all this? There are clearly things which could be done in UniMath but which have not been done. But why have they not been done? Is it just a matter of time, or are there things which are actually going to be *hard* to do in UniMath's foundations and doing in them in, say, ZFC or another kind of type theory would be much easier? Kevin > > - The paper https://lmcs.episciences.org/4814/pdf > contains a presentation of the categorical semantics of type theory using univalence; > Section 2.3 discusses some differences between the “classical” approach to representation of structures > and the approach in the univalent setting. > > The system is compatible with classical logic and choice (but this has not been needed in these examples). > > Best regards, > Thierry > > > > On 25 May 2019, at 12:22, Steve Awodey <awodey@cmu.edu> wrote: > > A useful example for you might be Floris van Doorn’s formalization of > the Atiyah-Hirzebruch and Serre spectral sequences for cohomology > in HoTT using Lean: > > https://arxiv.org/abs/1808.10690 > > Regards, > > Steve > > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > Hi from a Lean user. > > As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others. > > I have seen enough of Lean to become convinced that the pain points would be surmountable in Lean. I have seen enough of Isabelle/HOL to become skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings. > > I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a blessing and a curse. However I would like to know more details. I am speaking at the Big Proof conference in Edinburgh this coming Wednesday on the pain points involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT. > > Everyone will have a different interpretation of "modern pure mathematics" so to fix our ideas, let me say that for the purposes of this discussion, "modern pure mathematics" means the statements of the theorems publishsed by the Annals of Mathematics over the last few years, so for example I am talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the like; one can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is. > > If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics). > > Kevin Buzzard > > -- > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > > > -- > 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/BFBE1A09-A246-4DAD-8AD2-25C3C517A7FE%40cmu.edu. > For more options, visit https://groups.google.com/d/optout. > > -- 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/CAH52Xb0EK8xf1d6Oq9AgAcnjenu4Nhu7H7VcvDWToMpVKVtCog%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 4630 bytes --] On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the "additivity axiom". Please let me know if the following formulation of the such axiom is correct: [image: additivity.jpg] On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: > > A useful example for you might be Floris van Doorn’s formalization of > the Atiyah-Hirzebruch and Serre spectral sequences for cohomology > in HoTT using Lean: > > https://arxiv.org/abs/1808.10690 > > Regards, > > Steve > > > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com > <javascript:>> wrote: > > > > Hi from a Lean user. > > > > As many people here will know, Tom Hales' formal abstracts project > https://formalabstracts.github.io/ wants to formalise many of the > statements of modern pure mathematics in Lean. One could ask more generally > about a project of formalising many of the statements of modern pure > mathematics in an arbitrary system, such as HoTT. I know enough about the > formalisation process to know that whatever system one chooses, there will > be pain points, because some mathematical ideas fit more readily into some > foundational systems than others. > > > > I have seen enough of Lean to become convinced that the pain points > would be surmountable in Lean. I have seen enough of Isabelle/HOL to become > skeptical about the idea that it would be suitable for all of modern pure > mathematics, although it is clearly suitable for some of it; however it > seems that simple type theory struggles to handle things like tensor > products of sheaves of modules on a scheme, because sheaves are dependent > types and it seems that one cannot use Isabelle's typeclass system to > handle the rings showing up in a sheaf of rings. > > > > I have very little experience with HoTT. I have heard that the fact that > "all constructions must be isomorphism-invariant" is both a blessing and a > curse. However I would like to know more details. I am speaking at the Big > Proof conference in Edinburgh this coming Wednesday on the pain points > involved with formalising mathematical objects in dependent type theory and > during the preparation of my talk I began to wonder what the analogous > picture was with HoTT. > > > > Everyone will have a different interpretation of "modern pure > mathematics" so to fix our ideas, let me say that for the purposes of this > discussion, "modern pure mathematics" means the statements of the theorems > publishsed by the Annals of Mathematics over the last few years, so for > example I am talking about formalising statements of theorems involving > L-functions of abelian varieties over number fields, Hodge theory, > cohomology of algebraic varieties, Hecke algebras of symmetric groups, > Ricci flow and the like; one can see titles and more at > http://annals.math.princeton.edu/2019/189-3 . Classical logic and the > axiom of choice are absolutely essential -- I am only interested in the > hard-core "classical mathematician" stance of the way mathematics works, > and what it is. > > > > If this is not the right forum for this question, I would be happily > directed to somewhere more suitable. After spending 10 minutes failing to > get onto ##hott on freenode ("you need to be identified with services") I > decided it was easier just to ask here. If people want to chat directly I > am usually around at https://leanprover.zulipchat.com/ (registration > required, full names are usually used, I'll start a HoTT thread in > #mathematics). > > > > Kevin Buzzard > > > > -- > > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. > > > For more options, visit https://groups.google.com/d/optout. > > -- 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 8375 bytes --] [-- Attachment #2: additivity.jpg --] [-- Type: image/jpeg, Size: 18737 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 7350 bytes --] HoTT is NOT a specific proof assistant the way that Lean is. Instead it’s a different flavor of type theory which is well attuned to things that have a homotopical flavor. It can be implemented in various proof assistants (Coq, Agda, Lean 2) but none of them are really fully designed for HoTT. But the kind of practical question you’re asking depends on the implementation. I don’t think any of the implementations are practical in the way that you want. For example, I’m not aware of any kind of “tactics” for HoTT. The bookkeeping involved in saying that the two proofs of Eckman-Hilton for 3-loops agree (which I could explain in one hand gesture in person and where I understand all the relevant issues in HoTT) is very very intimidating practically. I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s better. HoTT is mostly better for math that’s explicitly homotopical. But there are situations in more ordinary math where you can see why it would be useful. For example, if G and H are isomorphic groups and you want to translate a theorem or construction across the isomorphism. In ordinary type theory this is going to involve annoying book-keeping which it seems like you’d have to do separately for each kind of mathematical object. In HoTT that happens automatically. For example, say you have a theorem about bimodules over semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.” Is that step something you’d be able to deal with easily in Lean? If not, that’s somewhere that down the line HoTT might make things more practical. But mostly I just want to say you’re making a category error in your question. HoTT is an abstract type theory, not a proof assistant. Best, Noah On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote: > On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the > "additivity axiom". Please let me know if the following formulation of the > such axiom is correct: > > [image: additivity.jpg] > > > > On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: >> >> A useful example for you might be Floris van Doorn’s formalization of >> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology >> in HoTT using Lean: >> >> https://arxiv.org/abs/1808.10690 >> >> Regards, >> >> Steve >> >> > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> >> wrote: >> > >> > Hi from a Lean user. >> > >> > As many people here will know, Tom Hales' formal abstracts project >> https://formalabstracts.github.io/ wants to formalise many of the >> statements of modern pure mathematics in Lean. One could ask more generally >> about a project of formalising many of the statements of modern pure >> mathematics in an arbitrary system, such as HoTT. I know enough about the >> formalisation process to know that whatever system one chooses, there will >> be pain points, because some mathematical ideas fit more readily into some >> foundational systems than others. >> > >> > I have seen enough of Lean to become convinced that the pain points >> would be surmountable in Lean. I have seen enough of Isabelle/HOL to become >> skeptical about the idea that it would be suitable for all of modern pure >> mathematics, although it is clearly suitable for some of it; however it >> seems that simple type theory struggles to handle things like tensor >> products of sheaves of modules on a scheme, because sheaves are dependent >> types and it seems that one cannot use Isabelle's typeclass system to >> handle the rings showing up in a sheaf of rings. >> > >> > I have very little experience with HoTT. I have heard that the fact >> that "all constructions must be isomorphism-invariant" is both a blessing >> and a curse. However I would like to know more details. I am speaking at >> the Big Proof conference in Edinburgh this coming Wednesday on the pain >> points involved with formalising mathematical objects in dependent type >> theory and during the preparation of my talk I began to wonder what the >> analogous picture was with HoTT. >> > >> > Everyone will have a different interpretation of "modern pure >> mathematics" so to fix our ideas, let me say that for the purposes of this >> discussion, "modern pure mathematics" means the statements of the theorems >> publishsed by the Annals of Mathematics over the last few years, so for >> example I am talking about formalising statements of theorems involving >> L-functions of abelian varieties over number fields, Hodge theory, >> cohomology of algebraic varieties, Hecke algebras of symmetric groups, >> Ricci flow and the like; one can see titles and more at >> http://annals.math.princeton.edu/2019/189-3 . Classical logic and the >> axiom of choice are absolutely essential -- I am only interested in the >> hard-core "classical mathematician" stance of the way mathematics works, >> and what it is. >> > >> > If this is not the right forum for this question, I would be happily >> directed to somewhere more suitable. After spending 10 minutes failing to >> get onto ##hott on freenode ("you need to be identified with services") I >> decided it was easier just to ask here. If people want to chat directly I >> am usually around at https://leanprover.zulipchat.com/ (registration >> required, full names are usually used, I'll start a HoTT thread in >> #mathematics). >> > >> > Kevin Buzzard >> > >> > -- >> > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. >> >> > For more options, visit https://groups.google.com/d/optout. >> >> -- > 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com?utm_medium=email&utm_source=footer> > . > For more options, visit https://groups.google.com/d/optout. > -- 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 9395 bytes --] [-- Attachment #2: additivity.jpg --] [-- Type: image/jpeg, Size: 18737 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 9733 bytes --] Hi Noah. Thank you for pointing out the category error. It seems to me that sometimes when I say "HoTT" I should be saying, for example, "UniMath". Tactics in Lean are absolutely crucial for library development. Coq has some really powerful tactics, right? UniMath can use those tactics, presumably? I understand that UniMath, as implemented in Coq, takes Coq and adds some "rules" of the form "you can't use this functionality" and also adds at least one new axiom (univalence). On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote: > I’d also imagine that a “practical” implementation would likely have some > kind of “two-level” type theory where you can use types that behave > classically when that’s better and HoTT types when that’s better. > But plain Coq has such types, right? OK so this has all been extremely informative. There are other provers being developed which will implement some flavour of HoTT more "faithfully", and it might be easier to develop maths libraries in such provers. For example, if G and H are isomorphic groups and you want to translate a > theorem or construction across the isomorphism. In ordinary type theory > this is going to involve annoying book-keeping which it seems like you’d > have to do separately for each kind of mathematical object. > Yes. This is a pain point in Lean. It's a particularly nasty one too, as far as mathematicians are concerned, because when you tell a mathematician "well this ring R is Cohen-Macauley, and here's a ring S which is isomorphic to R, but we cannot immediately deduce in Lean that S is Cohen-Macauley" then they begin to question what kind of crazy system you are using which cannot deduce this immediately. As an interesting experiment, find your favourite mathematician, preferably one who does not know what a Cohen-Macauley ring is, and ask them whether they think it will be true that if R and S are isomorphic rings and R is Cohen-Macauley then S is too. They will be very confident that this is true, even if they do not know the definition; standard mathematical definitions are isomorphism-invariant. This is part of our code of conduct, in fact. However in Lean I believe that the current plan is to try and make a tactic which will resolve this issue. This has not yet been done, and as far as I can see this is a place where UniMath is a more natural fit for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points for it, which Lean manages to get over more easily. That is somehow where I'm coming from. > For example, say you have a theorem about bimodules over semisimple rings > whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras > are multimatrix algebras over division rings.” Is that step something > you’d be able to deal with easily in Lean? If not, that’s somewhere that > down the line HoTT might make things more practical. > This is a great example! To be honest I am slightly confused about why we are not running into this sort of thing already. As far as I can see this would be a great test case for the (still very much under development) transport tactic. Maybe we don't have enough classification theorems. I think that our hope in general is that this sort of issue can be solved with automation. Kevin > But mostly I just want to say you’re making a category error in your > question. HoTT is an abstract type theory, not a proof assistant. > > Best, > > Noah > > On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote: > >> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the >> "additivity axiom". Please let me know if the following formulation of the >> such axiom is correct: >> >> [image: additivity.jpg] >> >> >> >> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: >>> >>> A useful example for you might be Floris van Doorn’s formalization of >>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology >>> in HoTT using Lean: >>> >>> https://arxiv.org/abs/1808.10690 >>> >>> Regards, >>> >>> Steve >>> >>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> >>> wrote: >>> > >>> > Hi from a Lean user. >>> > >>> > As many people here will know, Tom Hales' formal abstracts project >>> https://formalabstracts.github.io/ wants to formalise many of the >>> statements of modern pure mathematics in Lean. One could ask more generally >>> about a project of formalising many of the statements of modern pure >>> mathematics in an arbitrary system, such as HoTT. I know enough about the >>> formalisation process to know that whatever system one chooses, there will >>> be pain points, because some mathematical ideas fit more readily into some >>> foundational systems than others. >>> > >>> > I have seen enough of Lean to become convinced that the pain points >>> would be surmountable in Lean. I have seen enough of Isabelle/HOL to become >>> skeptical about the idea that it would be suitable for all of modern pure >>> mathematics, although it is clearly suitable for some of it; however it >>> seems that simple type theory struggles to handle things like tensor >>> products of sheaves of modules on a scheme, because sheaves are dependent >>> types and it seems that one cannot use Isabelle's typeclass system to >>> handle the rings showing up in a sheaf of rings. >>> > >>> > I have very little experience with HoTT. I have heard that the fact >>> that "all constructions must be isomorphism-invariant" is both a blessing >>> and a curse. However I would like to know more details. I am speaking at >>> the Big Proof conference in Edinburgh this coming Wednesday on the pain >>> points involved with formalising mathematical objects in dependent type >>> theory and during the preparation of my talk I began to wonder what the >>> analogous picture was with HoTT. >>> > >>> > Everyone will have a different interpretation of "modern pure >>> mathematics" so to fix our ideas, let me say that for the purposes of this >>> discussion, "modern pure mathematics" means the statements of the theorems >>> publishsed by the Annals of Mathematics over the last few years, so for >>> example I am talking about formalising statements of theorems involving >>> L-functions of abelian varieties over number fields, Hodge theory, >>> cohomology of algebraic varieties, Hecke algebras of symmetric groups, >>> Ricci flow and the like; one can see titles and more at >>> http://annals.math.princeton.edu/2019/189-3 . Classical logic and the >>> axiom of choice are absolutely essential -- I am only interested in the >>> hard-core "classical mathematician" stance of the way mathematics works, >>> and what it is. >>> > >>> > If this is not the right forum for this question, I would be happily >>> directed to somewhere more suitable. After spending 10 minutes failing to >>> get onto ##hott on freenode ("you need to be identified with services") I >>> decided it was easier just to ask here. If people want to chat directly I >>> am usually around at https://leanprover.zulipchat.com/ (registration >>> required, full names are usually used, I'll start a HoTT thread in >>> #mathematics). >>> > >>> > Kevin Buzzard >>> > >>> > -- >>> > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. >>> >>> > For more options, visit https://groups.google.com/d/optout. >>> >>> -- >> 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com >> <https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> For more options, visit https://groups.google.com/d/optout. >> > -- > 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > For more options, visit https://groups.google.com/d/optout. > -- 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/CAH52Xb3k4fmuPfpDSO%3DJmb3k19v3m6MjOLweQb_u8n0icdt0rQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 12940 bytes --] [-- Attachment #2: additivity.jpg --] [-- Type: image/jpeg, Size: 18737 bytes --]

[-- Attachment #1: Type: text/plain, Size: 12121 bytes --] UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library." “Coq with the indices-matter option plus the HoTT library" is of the same category as "Lean plus the math library" and then it makes sense to compare how practically useful they are for math. Here it's important to note that most advanced things that you can do in Coq are broken by using the "indices-matter" option and relatedly not using the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04591 "This small change makes the whole standard library unusable, and many tactics stop working, too. The solution was rather drastic: we ripped out the standard library and replaced it with a minimal core that is sufficient for the basic tactics to work." (In particular, I was in error in my previous email, *some* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical calculations.) I should say I've never used Coq, just Agda. (When I was using Agda the situation was even worse, things like pattern matching secretly assumed k even if you used the without-k option, and HITs were put in by a hack that wasn't totally clear if it worked, etc.) So I'm likely wrong in some places above. So I think from a practical point of view, “Coq with the indices-matter option plus the HoTT library" is well behind ordinary Coq (and also Lean) for doing ordinary mathematics. However, if and when it does catch up some of the pain points involving transporting from my previous email should go away automatically. (Side comment: once you start talking about transporting stuff related to categories across equivalences of categories it's only going to get more painful in ordinary type theory, but will remain easy in HoTT approaches.) Best, Noah p.s. Installed Lean last week. Looking forward to using it next year when Scott and I are both at MSRI. On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > Hi Noah. Thank you for pointing out the category error. It seems to me > that sometimes when I say "HoTT" I should be saying, for example, "UniMath". > > Tactics in Lean are absolutely crucial for library development. Coq has > some really powerful tactics, right? UniMath can use those tactics, > presumably? > > I understand that UniMath, as implemented in Coq, takes Coq and adds some > "rules" of the form "you can't use this functionality" and also adds at > least one new axiom (univalence). > > On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote: > >> I’d also imagine that a “practical” implementation would likely have some >> kind of “two-level” type theory where you can use types that behave >> classically when that’s better and HoTT types when that’s better. >> > > But plain Coq has such types, right? > > OK so this has all been extremely informative. There are other provers > being developed which will implement some flavour of HoTT more > "faithfully", and it might be easier to develop maths libraries in such > provers. > > For example, if G and H are isomorphic groups and you want to translate a >> theorem or construction across the isomorphism. In ordinary type theory >> this is going to involve annoying book-keeping which it seems like you’d >> have to do separately for each kind of mathematical object. >> > > Yes. This is a pain point in Lean. It's a particularly nasty one too, as > far as mathematicians are concerned, because when you tell a mathematician > "well this ring R is Cohen-Macauley, and here's a ring S which is > isomorphic to R, but we cannot immediately deduce in Lean that S is > Cohen-Macauley" then they begin to question what kind of crazy system you > are using which cannot deduce this immediately. As an interesting > experiment, find your favourite mathematician, preferably one who does not > know what a Cohen-Macauley ring is, and ask them whether they think it will > be true that if R and S are isomorphic rings and R is Cohen-Macauley then S > is too. They will be very confident that this is true, even if they do not > know the definition; standard mathematical definitions are > isomorphism-invariant. This is part of our code of conduct, in fact. > > However in Lean I believe that the current plan is to try and make a > tactic which will resolve this issue. This has not yet been done, and as > far as I can see this is a place where UniMath is a more natural fit for > "the way mathematicians think". However now I've looked over what has > currently been formalised in UniMath I am wondering whether there are pain > points for it, which Lean manages to get over more easily. That is somehow > where I'm coming from. > > >> For example, say you have a theorem about bimodules over semisimple >> rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both >> algebras are multimatrix algebras over division rings.” Is that step >> something you’d be able to deal with easily in Lean? If not, that’s >> somewhere that down the line HoTT might make things more practical. >> > > This is a great example! To be honest I am slightly confused about why we > are not running into this sort of thing already. As far as I can see this > would be a great test case for the (still very much under development) > transport tactic. Maybe we don't have enough classification theorems. I > think that our hope in general is that this sort of issue can be solved > with automation. > > Kevin > > > >> But mostly I just want to say you’re making a category error in your >> question. HoTT is an abstract type theory, not a proof assistant. >> >> Best, >> >> Noah >> >> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote: >> >>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the >>> "additivity axiom". Please let me know if the following formulation of the >>> such axiom is correct: >>> >>> [image: additivity.jpg] >>> >>> >>> >>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: >>>> >>>> A useful example for you might be Floris van Doorn’s formalization of >>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology >>>> in HoTT using Lean: >>>> >>>> https://arxiv.org/abs/1808.10690 >>>> >>>> Regards, >>>> >>>> Steve >>>> >>>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> >>>> wrote: >>>> > >>>> > Hi from a Lean user. >>>> > >>>> > As many people here will know, Tom Hales' formal abstracts project >>>> https://formalabstracts.github.io/ wants to formalise many of the >>>> statements of modern pure mathematics in Lean. One could ask more generally >>>> about a project of formalising many of the statements of modern pure >>>> mathematics in an arbitrary system, such as HoTT. I know enough about the >>>> formalisation process to know that whatever system one chooses, there will >>>> be pain points, because some mathematical ideas fit more readily into some >>>> foundational systems than others. >>>> > >>>> > I have seen enough of Lean to become convinced that the pain points >>>> would be surmountable in Lean. I have seen enough of Isabelle/HOL to become >>>> skeptical about the idea that it would be suitable for all of modern pure >>>> mathematics, although it is clearly suitable for some of it; however it >>>> seems that simple type theory struggles to handle things like tensor >>>> products of sheaves of modules on a scheme, because sheaves are dependent >>>> types and it seems that one cannot use Isabelle's typeclass system to >>>> handle the rings showing up in a sheaf of rings. >>>> > >>>> > I have very little experience with HoTT. I have heard that the fact >>>> that "all constructions must be isomorphism-invariant" is both a blessing >>>> and a curse. However I would like to know more details. I am speaking at >>>> the Big Proof conference in Edinburgh this coming Wednesday on the pain >>>> points involved with formalising mathematical objects in dependent type >>>> theory and during the preparation of my talk I began to wonder what the >>>> analogous picture was with HoTT. >>>> > >>>> > Everyone will have a different interpretation of "modern pure >>>> mathematics" so to fix our ideas, let me say that for the purposes of this >>>> discussion, "modern pure mathematics" means the statements of the theorems >>>> publishsed by the Annals of Mathematics over the last few years, so for >>>> example I am talking about formalising statements of theorems involving >>>> L-functions of abelian varieties over number fields, Hodge theory, >>>> cohomology of algebraic varieties, Hecke algebras of symmetric groups, >>>> Ricci flow and the like; one can see titles and more at >>>> http://annals.math.princeton.edu/2019/189-3 . Classical logic and the >>>> axiom of choice are absolutely essential -- I am only interested in the >>>> hard-core "classical mathematician" stance of the way mathematics works, >>>> and what it is. >>>> > >>>> > If this is not the right forum for this question, I would be happily >>>> directed to somewhere more suitable. After spending 10 minutes failing to >>>> get onto ##hott on freenode ("you need to be identified with services") I >>>> decided it was easier just to ask here. If people want to chat directly I >>>> am usually around at https://leanprover.zulipchat.com/ (registration >>>> required, full names are usually used, I'll start a HoTT thread in >>>> #mathematics). >>>> > >>>> > Kevin Buzzard >>>> > >>>> > -- >>>> > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. >>>> >>>> > For more options, visit https://groups.google.com/d/optout. >>>> >>>> -- >>> 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com >>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> For more options, visit https://groups.google.com/d/optout. >>> >> -- >> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com >> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . > > >> For more options, visit https://groups.google.com/d/optout. >> > -- 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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 16876 bytes --]

[-- Attachment #1: Type: text/plain, Size: 14134 bytes --] There has been progress in making a cleaner interface with the standard Coq tactics. (Some abstractions were broken at the ocaml level) I'm hopeful that this can be lead to a clean connection between the HoTT library and more of the Coq developments in the not too distant future. As it exists in agda now. IIUC, UniMath does not allow any of the standard library or it's tactics, or even record types, since Vladimir wanted to have a very tight connection between type theory and it's semantics in simplicial sets. So, I don't expect them to connect to other developments, but I could be wrong. About the bundled/unbundled issue, which also exists in Coq, there's some recent progress "frame type theory" which should be applicable to both Coq and lean: http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51 Coming back to Kevin's question, yes, HoTT (plus classical logic for sets), seems to be the most natural foundation for mathematics as is currently published in the Annals. On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote: > UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a > category from “Coq with the indices-matter option plus the HoTT library." > “Coq with the indices-matter option plus the HoTT library" is of the same > category as "Lean plus the math library" and then it makes sense to compare > how practically useful they are for math. > > Here it's important to note that most advanced things that you can do in > Coq are broken by using the "indices-matter" option and relatedly not using > the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04591 > "This small change makes the whole standard library unusable, and many > tactics stop working, too. The solution was rather drastic: we ripped out > the standard library and replaced it with a minimal core that is sufficient > for the basic tactics to work." > > (In particular, I was in error in my previous email, *some* tactics are > available in Coq+indices-matter+HoTT, but not many of the more advanced > ones, and to my knowledge, not tactics needed for complicated homotopical > calculations.) > > I should say I've never used Coq, just Agda. (When I was using Agda the > situation was even worse, things like pattern matching secretly assumed k > even if you used the without-k option, and HITs were put in by a hack that > wasn't totally clear if it worked, etc.) So I'm likely wrong in some > places above. > > So I think from a practical point of view, “Coq with the indices-matter > option plus the HoTT library" is well behind ordinary Coq (and also Lean) > for doing ordinary mathematics. However, if and when it does catch up some > of the pain points involving transporting from my previous email should go > away automatically. (Side comment: once you start talking about > transporting stuff related to categories across equivalences of categories > it's only going to get more painful in ordinary type theory, but will > remain easy in HoTT approaches.) > > Best, > > Noah > > p.s. Installed Lean last week. Looking forward to using it next year when > Scott and I are both at MSRI. > > On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> > wrote: > >> Hi Noah. Thank you for pointing out the category error. It seems to me >> that sometimes when I say "HoTT" I should be saying, for example, "UniMath". >> >> Tactics in Lean are absolutely crucial for library development. Coq has >> some really powerful tactics, right? UniMath can use those tactics, >> presumably? >> >> I understand that UniMath, as implemented in Coq, takes Coq and adds some >> "rules" of the form "you can't use this functionality" and also adds at >> least one new axiom (univalence). >> >> On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote: >> >>> I’d also imagine that a “practical” implementation would likely have >>> some kind of “two-level” type theory where you can use types that behave >>> classically when that’s better and HoTT types when that’s better. >>> >> >> But plain Coq has such types, right? >> >> OK so this has all been extremely informative. There are other provers >> being developed which will implement some flavour of HoTT more >> "faithfully", and it might be easier to develop maths libraries in such >> provers. >> >> For example, if G and H are isomorphic groups and you want to translate a >>> theorem or construction across the isomorphism. In ordinary type theory >>> this is going to involve annoying book-keeping which it seems like you’d >>> have to do separately for each kind of mathematical object. >>> >> >> Yes. This is a pain point in Lean. It's a particularly nasty one too, as >> far as mathematicians are concerned, because when you tell a mathematician >> "well this ring R is Cohen-Macauley, and here's a ring S which is >> isomorphic to R, but we cannot immediately deduce in Lean that S is >> Cohen-Macauley" then they begin to question what kind of crazy system you >> are using which cannot deduce this immediately. As an interesting >> experiment, find your favourite mathematician, preferably one who does not >> know what a Cohen-Macauley ring is, and ask them whether they think it will >> be true that if R and S are isomorphic rings and R is Cohen-Macauley then S >> is too. They will be very confident that this is true, even if they do not >> know the definition; standard mathematical definitions are >> isomorphism-invariant. This is part of our code of conduct, in fact. >> >> However in Lean I believe that the current plan is to try and make a >> tactic which will resolve this issue. This has not yet been done, and as >> far as I can see this is a place where UniMath is a more natural fit for >> "the way mathematicians think". However now I've looked over what has >> currently been formalised in UniMath I am wondering whether there are pain >> points for it, which Lean manages to get over more easily. That is somehow >> where I'm coming from. >> >> >>> For example, say you have a theorem about bimodules over semisimple >>> rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both >>> algebras are multimatrix algebras over division rings.” Is that step >>> something you’d be able to deal with easily in Lean? If not, that’s >>> somewhere that down the line HoTT might make things more practical. >>> >> >> This is a great example! To be honest I am slightly confused about why we >> are not running into this sort of thing already. As far as I can see this >> would be a great test case for the (still very much under development) >> transport tactic. Maybe we don't have enough classification theorems. I >> think that our hope in general is that this sort of issue can be solved >> with automation. >> >> Kevin >> >> >> >>> But mostly I just want to say you’re making a category error in your >>> question. HoTT is an abstract type theory, not a proof assistant. >>> >>> Best, >>> >>> Noah >>> >>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote: >>> >>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the >>>> "additivity axiom". Please let me know if the following formulation of the >>>> such axiom is correct: >>>> >>>> [image: additivity.jpg] >>>> >>>> >>>> >>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: >>>>> >>>>> A useful example for you might be Floris van Doorn’s formalization of >>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology >>>>> in HoTT using Lean: >>>>> >>>>> https://arxiv.org/abs/1808.10690 >>>>> >>>>> Regards, >>>>> >>>>> Steve >>>>> >>>>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> >>>>> wrote: >>>>> > >>>>> > Hi from a Lean user. >>>>> > >>>>> > As many people here will know, Tom Hales' formal abstracts project >>>>> https://formalabstracts.github.io/ wants to formalise many of the >>>>> statements of modern pure mathematics in Lean. One could ask more generally >>>>> about a project of formalising many of the statements of modern pure >>>>> mathematics in an arbitrary system, such as HoTT. I know enough about the >>>>> formalisation process to know that whatever system one chooses, there will >>>>> be pain points, because some mathematical ideas fit more readily into some >>>>> foundational systems than others. >>>>> > >>>>> > I have seen enough of Lean to become convinced that the pain points >>>>> would be surmountable in Lean. I have seen enough of Isabelle/HOL to become >>>>> skeptical about the idea that it would be suitable for all of modern pure >>>>> mathematics, although it is clearly suitable for some of it; however it >>>>> seems that simple type theory struggles to handle things like tensor >>>>> products of sheaves of modules on a scheme, because sheaves are dependent >>>>> types and it seems that one cannot use Isabelle's typeclass system to >>>>> handle the rings showing up in a sheaf of rings. >>>>> > >>>>> > I have very little experience with HoTT. I have heard that the fact >>>>> that "all constructions must be isomorphism-invariant" is both a blessing >>>>> and a curse. However I would like to know more details. I am speaking at >>>>> the Big Proof conference in Edinburgh this coming Wednesday on the pain >>>>> points involved with formalising mathematical objects in dependent type >>>>> theory and during the preparation of my talk I began to wonder what the >>>>> analogous picture was with HoTT. >>>>> > >>>>> > Everyone will have a different interpretation of "modern pure >>>>> mathematics" so to fix our ideas, let me say that for the purposes of this >>>>> discussion, "modern pure mathematics" means the statements of the theorems >>>>> publishsed by the Annals of Mathematics over the last few years, so for >>>>> example I am talking about formalising statements of theorems involving >>>>> L-functions of abelian varieties over number fields, Hodge theory, >>>>> cohomology of algebraic varieties, Hecke algebras of symmetric groups, >>>>> Ricci flow and the like; one can see titles and more at >>>>> http://annals.math.princeton.edu/2019/189-3 . Classical logic and the >>>>> axiom of choice are absolutely essential -- I am only interested in the >>>>> hard-core "classical mathematician" stance of the way mathematics works, >>>>> and what it is. >>>>> > >>>>> > If this is not the right forum for this question, I would be happily >>>>> directed to somewhere more suitable. After spending 10 minutes failing to >>>>> get onto ##hott on freenode ("you need to be identified with services") I >>>>> decided it was easier just to ask here. If people want to chat directly I >>>>> am usually around at https://leanprover.zulipchat.com/ (registration >>>>> required, full names are usually used, I'll start a HoTT thread in >>>>> #mathematics). >>>>> > >>>>> > Kevin Buzzard >>>>> > >>>>> > -- >>>>> > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. >>>>> >>>>> > For more options, visit https://groups.google.com/d/optout. >>>>> >>>>> -- >>>> 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com >>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com?utm_medium=email&utm_source=footer> >>>> . >>>> For more options, visit https://groups.google.com/d/optout. >>>> >>> -- >>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com >>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com?utm_medium=email&utm_source=footer> >>> . >> >> >>> For more options, visit https://groups.google.com/d/optout. >>> >> -- > 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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > For more options, visit https://groups.google.com/d/optout. > -- 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/CAOoPQuTNxVJ5%2B1Xotk3wzCgaW0C4wcxOdkpHANbOYdK5rCRkiA%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 18925 bytes --]

[-- Attachment #1: Type: text/plain, Size: 18691 bytes --] It seems to me, now I understand much better what is going on (many thanks to all the people who replied) that dependent type theory + impredicative prop "got lucky", in that Coq has been around for a long time, and Lean 3 is an attempt to model basically the same type theory but in a way more suited to mathematics, written by someone who knows what they're doing (de Moura). Using nonconstructive maths e.g. LEM or AC etc in Lean 3 is just a matter of writing some incantation at the top of a file and then not thinking about it any more. HoTT might be more appropriate for mathematics -- or at least for some kinds of mathematics -- but its implementation in an actual piece of software seems a bit more hacky at this point ("use Coq, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean documentation is not ideal for mathematicians -- mathematicians need very early on to be able to use tactics such as `ring` or `norm_num` to do calculations with real numbers or in commutative rings, and these tactics are not even mentioned in the standard Lean documentation. I am a working mathematician who two years ago knew nothing about this way of doing mathematics on a computer. Now I have seen what is possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians do not see the point of it, or what it has to offer a modern working mathematician; they can see no immediate benefits in learning how this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists are there in an average maths department? In the UK at least, the answer is "much less than 1", and I cannot see that changing any time soon. I would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least make mathematicians sit up and take notice, but when I look at what has been done in these various systems I do not see this occurring. This weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic analysis? Where is the stuff which draws mathematicians in? This by no means a criticism of unimath -- it is in fact a far more broad criticism of all of the systems out there. Lean 3 might have schemes but they still can't prove that the derivative of sin is cos, and Isabelle/HOL might never have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) when formalising the odd order theorem in Coq, but it turns out that the odd order theorem is perhaps not a good "selling point" for mathematics formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will work, but that looks to me like a complete fantasy at this point. One thing I have learnt over the last two years is that a whole bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians to sit up and take notice? I guess we simply do not know, but if there is, I hope I'm still around. Kevin On Sun, 26 May 2019 at 06:50, Bas Spitters <b.a.w.spitters@gmail.com> wrote: > There has been progress in making a cleaner interface with the standard > Coq tactics. (Some abstractions were broken at the ocaml level) > I'm hopeful that this can be lead to a clean connection between the HoTT > library and more of the Coq developments in the not too distant future. > As it exists in agda now. > > IIUC, UniMath does not allow any of the standard library or it's tactics, > or even record types, since Vladimir wanted to have a very tight connection > between type theory and it's semantics in simplicial sets. So, I don't > expect them to connect to other developments, but I could be wrong. > > About the bundled/unbundled issue, which also exists in Coq, there's some > recent progress "frame type theory" which should be applicable to both Coq > and lean: > http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51 > > Coming back to Kevin's question, yes, HoTT (plus classical logic for > sets), seems to be the most natural foundation for mathematics as is > currently published in the Annals. > > On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote: > >> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a >> category from “Coq with the indices-matter option plus the HoTT library." >> “Coq with the indices-matter option plus the HoTT library" is of the same >> category as "Lean plus the math library" and then it makes sense to compare >> how practically useful they are for math. >> >> Here it's important to note that most advanced things that you can do in >> Coq are broken by using the "indices-matter" option and relatedly not using >> the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04591 >> "This small change makes the whole standard library unusable, and many >> tactics stop working, too. The solution was rather drastic: we ripped out >> the standard library and replaced it with a minimal core that is sufficient >> for the basic tactics to work." >> >> (In particular, I was in error in my previous email, *some* tactics are >> available in Coq+indices-matter+HoTT, but not many of the more advanced >> ones, and to my knowledge, not tactics needed for complicated homotopical >> calculations.) >> >> I should say I've never used Coq, just Agda. (When I was using Agda the >> situation was even worse, things like pattern matching secretly assumed k >> even if you used the without-k option, and HITs were put in by a hack that >> wasn't totally clear if it worked, etc.) So I'm likely wrong in some >> places above. >> >> So I think from a practical point of view, “Coq with the indices-matter >> option plus the HoTT library" is well behind ordinary Coq (and also Lean) >> for doing ordinary mathematics. However, if and when it does catch up some >> of the pain points involving transporting from my previous email should go >> away automatically. (Side comment: once you start talking about >> transporting stuff related to categories across equivalences of categories >> it's only going to get more painful in ordinary type theory, but will >> remain easy in HoTT approaches.) >> >> Best, >> >> Noah >> >> p.s. Installed Lean last week. Looking forward to using it next year >> when Scott and I are both at MSRI. >> >> On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> >> wrote: >> >>> Hi Noah. Thank you for pointing out the category error. It seems to me >>> that sometimes when I say "HoTT" I should be saying, for example, "UniMath". >>> >>> Tactics in Lean are absolutely crucial for library development. Coq has >>> some really powerful tactics, right? UniMath can use those tactics, >>> presumably? >>> >>> I understand that UniMath, as implemented in Coq, takes Coq and adds >>> some "rules" of the form "you can't use this functionality" and also adds >>> at least one new axiom (univalence). >>> >>> On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote: >>> >>>> I’d also imagine that a “practical” implementation would likely have >>>> some kind of “two-level” type theory where you can use types that behave >>>> classically when that’s better and HoTT types when that’s better. >>>> >>> >>> But plain Coq has such types, right? >>> >>> OK so this has all been extremely informative. There are other provers >>> being developed which will implement some flavour of HoTT more >>> "faithfully", and it might be easier to develop maths libraries in such >>> provers. >>> >>> For example, if G and H are isomorphic groups and you want to translate >>>> a theorem or construction across the isomorphism. In ordinary type theory >>>> this is going to involve annoying book-keeping which it seems like you’d >>>> have to do separately for each kind of mathematical object. >>>> >>> >>> Yes. This is a pain point in Lean. It's a particularly nasty one too, as >>> far as mathematicians are concerned, because when you tell a mathematician >>> "well this ring R is Cohen-Macauley, and here's a ring S which is >>> isomorphic to R, but we cannot immediately deduce in Lean that S is >>> Cohen-Macauley" then they begin to question what kind of crazy system you >>> are using which cannot deduce this immediately. As an interesting >>> experiment, find your favourite mathematician, preferably one who does not >>> know what a Cohen-Macauley ring is, and ask them whether they think it will >>> be true that if R and S are isomorphic rings and R is Cohen-Macauley then S >>> is too. They will be very confident that this is true, even if they do not >>> know the definition; standard mathematical definitions are >>> isomorphism-invariant. This is part of our code of conduct, in fact. >>> >>> However in Lean I believe that the current plan is to try and make a >>> tactic which will resolve this issue. This has not yet been done, and as >>> far as I can see this is a place where UniMath is a more natural fit for >>> "the way mathematicians think". However now I've looked over what has >>> currently been formalised in UniMath I am wondering whether there are pain >>> points for it, which Lean manages to get over more easily. That is somehow >>> where I'm coming from. >>> >>> >>>> For example, say you have a theorem about bimodules over semisimple >>>> rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both >>>> algebras are multimatrix algebras over division rings.” Is that step >>>> something you’d be able to deal with easily in Lean? If not, that’s >>>> somewhere that down the line HoTT might make things more practical. >>>> >>> >>> This is a great example! To be honest I am slightly confused about why >>> we are not running into this sort of thing already. As far as I can see >>> this would be a great test case for the (still very much under development) >>> transport tactic. Maybe we don't have enough classification theorems. I >>> think that our hope in general is that this sort of issue can be solved >>> with automation. >>> >>> Kevin >>> >>> >>> >>>> But mostly I just want to say you’re making a category error in your >>>> question. HoTT is an abstract type theory, not a proof assistant. >>>> >>>> Best, >>>> >>>> Noah >>>> >>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> >>>> wrote: >>>> >>>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the >>>>> "additivity axiom". Please let me know if the following formulation of the >>>>> such axiom is correct: >>>>> >>>>> [image: additivity.jpg] >>>>> >>>>> >>>>> >>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: >>>>>> >>>>>> A useful example for you might be Floris van Doorn’s formalization of >>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology >>>>>> in HoTT using Lean: >>>>>> >>>>>> https://arxiv.org/abs/1808.10690 >>>>>> >>>>>> Regards, >>>>>> >>>>>> Steve >>>>>> >>>>>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> >>>>>> wrote: >>>>>> > >>>>>> > Hi from a Lean user. >>>>>> > >>>>>> > As many people here will know, Tom Hales' formal abstracts project >>>>>> https://formalabstracts.github.io/ wants to formalise many of the >>>>>> statements of modern pure mathematics in Lean. One could ask more generally >>>>>> about a project of formalising many of the statements of modern pure >>>>>> mathematics in an arbitrary system, such as HoTT. I know enough about the >>>>>> formalisation process to know that whatever system one chooses, there will >>>>>> be pain points, because some mathematical ideas fit more readily into some >>>>>> foundational systems than others. >>>>>> > >>>>>> > I have seen enough of Lean to become convinced that the pain points >>>>>> would be surmountable in Lean. I have seen enough of Isabelle/HOL to become >>>>>> skeptical about the idea that it would be suitable for all of modern pure >>>>>> mathematics, although it is clearly suitable for some of it; however it >>>>>> seems that simple type theory struggles to handle things like tensor >>>>>> products of sheaves of modules on a scheme, because sheaves are dependent >>>>>> types and it seems that one cannot use Isabelle's typeclass system to >>>>>> handle the rings showing up in a sheaf of rings. >>>>>> > >>>>>> > I have very little experience with HoTT. I have heard that the fact >>>>>> that "all constructions must be isomorphism-invariant" is both a blessing >>>>>> and a curse. However I would like to know more details. I am speaking at >>>>>> the Big Proof conference in Edinburgh this coming Wednesday on the pain >>>>>> points involved with formalising mathematical objects in dependent type >>>>>> theory and during the preparation of my talk I began to wonder what the >>>>>> analogous picture was with HoTT. >>>>>> > >>>>>> > Everyone will have a different interpretation of "modern pure >>>>>> mathematics" so to fix our ideas, let me say that for the purposes of this >>>>>> discussion, "modern pure mathematics" means the statements of the theorems >>>>>> publishsed by the Annals of Mathematics over the last few years, so for >>>>>> example I am talking about formalising statements of theorems involving >>>>>> L-functions of abelian varieties over number fields, Hodge theory, >>>>>> cohomology of algebraic varieties, Hecke algebras of symmetric groups, >>>>>> Ricci flow and the like; one can see titles and more at >>>>>> http://annals.math.princeton.edu/2019/189-3 . Classical logic and >>>>>> the axiom of choice are absolutely essential -- I am only interested in the >>>>>> hard-core "classical mathematician" stance of the way mathematics works, >>>>>> and what it is. >>>>>> > >>>>>> > If this is not the right forum for this question, I would be >>>>>> happily directed to somewhere more suitable. After spending 10 minutes >>>>>> failing to get onto ##hott on freenode ("you need to be identified with >>>>>> services") I decided it was easier just to ask here. If people want to chat >>>>>> directly I am usually around at https://leanprover.zulipchat.com/ >>>>>> (registration required, full names are usually used, I'll start a HoTT >>>>>> thread in #mathematics). >>>>>> > >>>>>> > Kevin Buzzard >>>>>> > >>>>>> > -- >>>>>> > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. >>>>>> >>>>>> > For more options, visit https://groups.google.com/d/optout. >>>>>> >>>>>> -- >>>>> 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com >>>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>> . >>>>> For more options, visit https://groups.google.com/d/optout. >>>>> >>>> -- >>>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com >>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com?utm_medium=email&utm_source=footer> >>>> . >>> >>> >>>> For more options, visit https://groups.google.com/d/optout. >>>> >>> -- >> 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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com >> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> For more options, visit https://groups.google.com/d/optout. >> > -- 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/CAH52Xb3k9b8D0oW8Ue8XGY-ZAJZHfmc1pTRTJO1Qg%3D3Dw0zwuA%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 23667 bytes --]

Dear Kevin, We've been working on making formalization accessible to mathematicians for a long time. E.g. in our formath project: http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath It's a slow process, but I believe we are making progress. You seem to be mixing at least two issues. - HoTT/UF as a foundation - Current implementations in proof assistants. If you want to restrict to classical maths. Then please have a careful look at how its done in mathematical components: https://math-comp.github.io/mcb/ and the analysis library that is currently under development. https://github.com/math-comp/analysis If you went to help connecting this to the HoTT library, it will be much appreciated. https://github.com/HoTT/HoTT Best wishes, Bas On Sun, May 26, 2019 at 1:41 PM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > It seems to me, now I understand much better what is going on (many thanks to all the people who replied) that dependent type theory + impredicative prop "got lucky", in that Coq has been around for a long time, and Lean 3 is an attempt to model basically the same type theory but in a way more suited to mathematics, written by someone who knows what they're doing (de Moura). Using nonconstructive maths e.g. LEM or AC etc in Lean 3 is just a matter of writing some incantation at the top of a file and then not thinking about it any more. HoTT might be more appropriate for mathematics -- or at least for some kinds of mathematics -- but its implementation in an actual piece of software seems a bit more hacky at this point ("use Coq, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean documentation is not ideal for mathematicians -- mathematicians need very early on to be able to use tactics such as `ring` or `norm_num` to do calculations with real numbers or in commutative rings, and these tactics are not even mentioned in the standard Lean documentation. > > I am a working mathematician who two years ago knew nothing about this way of doing mathematics on a computer. Now I have seen what is possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians do not see the point of it, or what it has to offer a modern working mathematician; they can see no immediate benefits in learning how this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists are there in an average maths department? In the UK at least, the answer is "much less than 1", and I cannot see that changing any time soon. I would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least make mathematicians sit up and take notice, but when I look at what has been done in these various systems I do not see this occurring. This weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic analysis? Where is the stuff which draws mathematicians in? This by no means a criticism of unimath -- it is in fact a far more broad criticism of all of the systems out there. Lean 3 might have schemes but they still can't prove that the derivative of sin is cos, and Isabelle/HOL might never have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) when formalising the odd order theorem in Coq, but it turns out that the odd order theorem is perhaps not a good "selling point" for mathematics formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will work, but that looks to me like a complete fantasy at this point. > > One thing I have learnt over the last two years is that a whole bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians to sit up and take notice? I guess we simply do not know, but if there is, I hope I'm still around. > > Kevin > > > > On Sun, 26 May 2019 at 06:50, Bas Spitters <b.a.w.spitters@gmail.com> wrote: >> >> There has been progress in making a cleaner interface with the standard Coq tactics. (Some abstractions were broken at the ocaml level) >> I'm hopeful that this can be lead to a clean connection between the HoTT library and more of the Coq developments in the not too distant future. >> As it exists in agda now. >> >> IIUC, UniMath does not allow any of the standard library or it's tactics, or even record types, since Vladimir wanted to have a very tight connection between type theory and it's semantics in simplicial sets. So, I don't expect them to connect to other developments, but I could be wrong. >> >> About the bundled/unbundled issue, which also exists in Coq, there's some recent progress "frame type theory" which should be applicable to both Coq and lean: >> http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51 >> >> Coming back to Kevin's question, yes, HoTT (plus classical logic for sets), seems to be the most natural foundation for mathematics as is currently published in the Annals. >> >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote: >>> >>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library." “Coq with the indices-matter option plus the HoTT library" is of the same category as "Lean plus the math library" and then it makes sense to compare how practically useful they are for math. >>> >>> Here it's important to note that most advanced things that you can do in Coq are broken by using the "indices-matter" option and relatedly not using the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04591 "This small change makes the whole standard library unusable, and many tactics stop working, too. The solution was rather drastic: we ripped out the standard library and replaced it with a minimal core that is sufficient for the basic tactics to work." >>> >>> (In particular, I was in error in my previous email, *some* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical calculations.) >>> >>> I should say I've never used Coq, just Agda. (When I was using Agda the situation was even worse, things like pattern matching secretly assumed k even if you used the without-k option, and HITs were put in by a hack that wasn't totally clear if it worked, etc.) So I'm likely wrong in some places above. >>> >>> So I think from a practical point of view, “Coq with the indices-matter option plus the HoTT library" is well behind ordinary Coq (and also Lean) for doing ordinary mathematics. However, if and when it does catch up some of the pain points involving transporting from my previous email should go away automatically. (Side comment: once you start talking about transporting stuff related to categories across equivalences of categories it's only going to get more painful in ordinary type theory, but will remain easy in HoTT approaches.) >>> >>> Best, >>> >>> Noah >>> >>> p.s. Installed Lean last week. Looking forward to using it next year when Scott and I are both at MSRI. >>> >>> On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: >>>> >>>> Hi Noah. Thank you for pointing out the category error. It seems to me that sometimes when I say "HoTT" I should be saying, for example, "UniMath". >>>> >>>> Tactics in Lean are absolutely crucial for library development. Coq has some really powerful tactics, right? UniMath can use those tactics, presumably? >>>> >>>> I understand that UniMath, as implemented in Coq, takes Coq and adds some "rules" of the form "you can't use this functionality" and also adds at least one new axiom (univalence). >>>> >>>> On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote: >>>>> >>>>> I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s better. >>>> >>>> >>>> But plain Coq has such types, right? >>>> >>>> OK so this has all been extremely informative. There are other provers being developed which will implement some flavour of HoTT more "faithfully", and it might be easier to develop maths libraries in such provers. >>>> >>>>> For example, if G and H are isomorphic groups and you want to translate a theorem or construction across the isomorphism. In ordinary type theory this is going to involve annoying book-keeping which it seems like you’d have to do separately for each kind of mathematical object. >>>> >>>> >>>> Yes. This is a pain point in Lean. It's a particularly nasty one too, as far as mathematicians are concerned, because when you tell a mathematician "well this ring R is Cohen-Macauley, and here's a ring S which is isomorphic to R, but we cannot immediately deduce in Lean that S is Cohen-Macauley" then they begin to question what kind of crazy system you are using which cannot deduce this immediately. As an interesting experiment, find your favourite mathematician, preferably one who does not know what a Cohen-Macauley ring is, and ask them whether they think it will be true that if R and S are isomorphic rings and R is Cohen-Macauley then S is too. They will be very confident that this is true, even if they do not know the definition; standard mathematical definitions are isomorphism-invariant. This is part of our code of conduct, in fact. >>>> >>>> However in Lean I believe that the current plan is to try and make a tactic which will resolve this issue. This has not yet been done, and as far as I can see this is a place where UniMath is a more natural fit for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points for it, which Lean manages to get over more easily. That is somehow where I'm coming from. >>>> >>>>> >>>>> For example, say you have a theorem about bimodules over semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.” Is that step something you’d be able to deal with easily in Lean? If not, that’s somewhere that down the line HoTT might make things more practical. >>>> >>>> >>>> This is a great example! To be honest I am slightly confused about why we are not running into this sort of thing already. As far as I can see this would be a great test case for the (still very much under development) transport tactic. Maybe we don't have enough classification theorems. I think that our hope in general is that this sort of issue can be solved with automation. >>>> >>>> Kevin >>>> >>>> >>>>> >>>>> But mostly I just want to say you’re making a category error in your question. HoTT is an abstract type theory, not a proof assistant. >>>>> >>>>> Best, >>>>> >>>>> Noah >>>>> >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote: >>>>>> >>>>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the "additivity axiom". Please let me know if the following formulation of the such axiom is correct: >>>>>> >>>>>> >>>>>> >>>>>> >>>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: >>>>>>> >>>>>>> A useful example for you might be Floris van Doorn’s formalization of >>>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology >>>>>>> in HoTT using Lean: >>>>>>> >>>>>>> https://arxiv.org/abs/1808.10690 >>>>>>> >>>>>>> Regards, >>>>>>> >>>>>>> Steve >>>>>>> >>>>>>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> wrote: >>>>>>> > >>>>>>> > Hi from a Lean user. >>>>>>> > >>>>>>> > As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others. >>>>>>> > >>>>>>> > I have seen enough of Lean to become convinced that the pain points would be surmountable in Lean. I have seen enough of Isabelle/HOL to become skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings. >>>>>>> > >>>>>>> > I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a blessing and a curse. However I would like to know more details. I am speaking at the Big Proof conference in Edinburgh this coming Wednesday on the pain points involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT. >>>>>>> > >>>>>>> > Everyone will have a different interpretation of "modern pure mathematics" so to fix our ideas, let me say that for the purposes of this discussion, "modern pure mathematics" means the statements of the theorems publishsed by the Annals of Mathematics over the last few years, so for example I am talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the like; one can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is. >>>>>>> > >>>>>>> > If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics). >>>>>>> > >>>>>>> > Kevin Buzzard >>>>>>> > >>>>>>> > -- >>>>>>> > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. >>>>>>> > For more options, visit https://groups.google.com/d/optout. >>>>>>> >>>>>> -- >>>>>> 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com. >>>>>> For more options, visit https://groups.google.com/d/optout. >>>>> >>>>> -- >>>>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com. >>>>> >>>>> >>>>> For more options, visit https://groups.google.com/d/optout. >>> >>> -- >>> 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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com. >>> For more options, visit https://groups.google.com/d/optout. -- 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/CAOoPQuTnM2F9a5VTGKjfxemPCizRyiAoM_VDYNgfTnF89gCBKg%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

I would like to again thank the people who have been responding to my posts this weekend with links and further reading. I know the Lean literature but I knew very little indeed about HoTT / UniMath at the start of this weekend; at least now I feel like I know where you guys are. On Sun, 26 May 2019 at 13:09, Bas Spitters <b.a.w.spitters@gmail.com> wrote: > It's a slow process, but I believe we are making progress. I agree that it's a slow process! I think that in any computer science department you can find people who know about these tools, indeed in the computer science department at my university there are people using things like Coq for program verification. I think that one measure of success would be when in most mathematics departments you can find someone who knows about this stuff. My personal experience is that we seem to be far from this, at this point. Bas points out the EU-funded project ForMath and I know that Paulson has an EU grant in Cambridge for Isabelle (my impression is that it is centred in the computer science department) and there is a Lean one based in Amsterdam which I know has mathematicians involved. For me the shock is that now I've seen what these things can do, I am kind of stunned that mathematicians don't know more about them. > You seem to be mixing at least two issues. > - HoTT/UF as a foundation > - Current implementations in proof assistants. Yes; when I started this thread I was very unclear about how everything fitted together. I asked a bit on the Lean chat but I guess many people are like me -- they know one system, and are not experts at all in what is going on with the other systems. I had forgotten about the mathcomp book! Someone pointed it out to me a while ago but I knew far less then about everything so it was a bit more intimidating. Thanks for reminding me. I think I have basically said all I had to say (and have managed to get my ideas un-muddled about several things). But here is a parting shot. Voevodsky was interested in formalising mathematics in a proof assistant. Before that, Voevodsky was a "traditional mathematician" and proved some great theorems and made some great constructions using mathematical objects called schemes. Theorems about schemes (his development of a homotopy theory for schemes) are what got him his Fields Medal. Schemes were clearly close to his heart. But looking at the things he formalised, he was doing things like the p-adic numbers, and lots and lots of category theory. I am surprised that he did not attempt to formalise the basic theory of schemes. Grothendieck's EGA is written in quite a "formal" way (although nowhere near as formal as what would be needed to formalise it easily in a proof assistant) and Johan de Jong's Stacks Project https://stacks.math.columbia.edu/ is another very solid attempt to lay down the foundations of the theory. I asked Johan whether he now considered his choice of "nice web pages" old-fashioned when it was now possible to formalise things in a proof assistant, and he said that he did not have time to learn how to use a proof assistant. But Voevodsky was surely aware of this work, and also how suitable it looks for formalisation. Thanks again to this community for all the comments and all the links and all the corrections. If anyone is going to Big Proof in Edinburgh this coming week I'd be happy to talk more. Kevin > > If you want to restrict to classical maths. Then please have a careful > look at how its done in mathematical components: > https://math-comp.github.io/mcb/ > and the analysis library that is currently under development. > https://github.com/math-comp/analysis > > If you went to help connecting this to the HoTT library, it will be > much appreciated. > https://github.com/HoTT/HoTT > > Best wishes, > > Bas > > On Sun, May 26, 2019 at 1:41 PM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > > > It seems to me, now I understand much better what is going on (many thanks to all the people who replied) that dependent type theory + impredicative prop "got lucky", in that Coq has been around for a long time, and Lean 3 is an attempt to model basically the same type theory but in a way more suited to mathematics, written by someone who knows what they're doing (de Moura). Using nonconstructive maths e.g. LEM or AC etc in Lean 3 is just a matter of writing some incantation at the top of a file and then not thinking about it any more. HoTT might be more appropriate for mathematics -- or at least for some kinds of mathematics -- but its implementation in an actual piece of software seems a bit more hacky at this point ("use Coq, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean documentation is not ideal for mathematicians -- mathematicians need very early on to be able to use tactics such as `ring` or `norm_num` to do calculations with real numbers or in commutative rings, and these tactics are not even mentioned in the standard Lean documentation. > > > > I am a working mathematician who two years ago knew nothing about this way of doing mathematics on a computer. Now I have seen what is possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians do not see the point of it, or what it has to offer a modern working mathematician; they can see no immediate benefits in learning how this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists are there in an average maths department? In the UK at least, the answer is "much less than 1", and I cannot see that changing any time soon. I would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least make mathematicians sit up and take notice, but when I look at what has been done in these various systems I do not see this occurring. This weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic analysis? Where is the stuff which draws mathematicians in? This by no means a criticism of unimath -- it is in fact a far more broad criticism of all of the systems out there. Lean 3 might have schemes but they still can't prove that the derivative of sin is cos, and Isabelle/HOL might never have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) when formalising the odd order theorem in Coq, but it turns out that the odd order theorem is perhaps not a good "selling point" for mathematics formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will work, but that looks to me like a complete fantasy at this point. > > > > One thing I have learnt over the last two years is that a whole bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians to sit up and take notice? I guess we simply do not know, but if there is, I hope I'm still around. > > > > Kevin > > > > > > > > On Sun, 26 May 2019 at 06:50, Bas Spitters <b.a.w.spitters@gmail.com> wrote: > >> > >> There has been progress in making a cleaner interface with the standard Coq tactics. (Some abstractions were broken at the ocaml level) > >> I'm hopeful that this can be lead to a clean connection between the HoTT library and more of the Coq developments in the not too distant future. > >> As it exists in agda now. > >> > >> IIUC, UniMath does not allow any of the standard library or it's tactics, or even record types, since Vladimir wanted to have a very tight connection between type theory and it's semantics in simplicial sets. So, I don't expect them to connect to other developments, but I could be wrong. > >> > >> About the bundled/unbundled issue, which also exists in Coq, there's some recent progress "frame type theory" which should be applicable to both Coq and lean: > >> http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51 > >> > >> Coming back to Kevin's question, yes, HoTT (plus classical logic for sets), seems to be the most natural foundation for mathematics as is currently published in the Annals. > >> > >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote: > >>> > >>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library." “Coq with the indices-matter option plus the HoTT library" is of the same category as "Lean plus the math library" and then it makes sense to compare how practically useful they are for math. > >>> > >>> Here it's important to note that most advanced things that you can do in Coq are broken by using the "indices-matter" option and relatedly not using the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04591 "This small change makes the whole standard library unusable, and many tactics stop working, too. The solution was rather drastic: we ripped out the standard library and replaced it with a minimal core that is sufficient for the basic tactics to work." > >>> > >>> (In particular, I was in error in my previous email, *some* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical calculations.) > >>> > >>> I should say I've never used Coq, just Agda. (When I was using Agda the situation was even worse, things like pattern matching secretly assumed k even if you used the without-k option, and HITs were put in by a hack that wasn't totally clear if it worked, etc.) So I'm likely wrong in some places above. > >>> > >>> So I think from a practical point of view, “Coq with the indices-matter option plus the HoTT library" is well behind ordinary Coq (and also Lean) for doing ordinary mathematics. However, if and when it does catch up some of the pain points involving transporting from my previous email should go away automatically. (Side comment: once you start talking about transporting stuff related to categories across equivalences of categories it's only going to get more painful in ordinary type theory, but will remain easy in HoTT approaches.) > >>> > >>> Best, > >>> > >>> Noah > >>> > >>> p.s. Installed Lean last week. Looking forward to using it next year when Scott and I are both at MSRI. > >>> > >>> On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > >>>> > >>>> Hi Noah. Thank you for pointing out the category error. It seems to me that sometimes when I say "HoTT" I should be saying, for example, "UniMath". > >>>> > >>>> Tactics in Lean are absolutely crucial for library development. Coq has some really powerful tactics, right? UniMath can use those tactics, presumably? > >>>> > >>>> I understand that UniMath, as implemented in Coq, takes Coq and adds some "rules" of the form "you can't use this functionality" and also adds at least one new axiom (univalence). > >>>> > >>>> On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote: > >>>>> > >>>>> I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s better. > >>>> > >>>> > >>>> But plain Coq has such types, right? > >>>> > >>>> OK so this has all been extremely informative. There are other provers being developed which will implement some flavour of HoTT more "faithfully", and it might be easier to develop maths libraries in such provers. > >>>> > >>>>> For example, if G and H are isomorphic groups and you want to translate a theorem or construction across the isomorphism. In ordinary type theory this is going to involve annoying book-keeping which it seems like you’d have to do separately for each kind of mathematical object. > >>>> > >>>> > >>>> Yes. This is a pain point in Lean. It's a particularly nasty one too, as far as mathematicians are concerned, because when you tell a mathematician "well this ring R is Cohen-Macauley, and here's a ring S which is isomorphic to R, but we cannot immediately deduce in Lean that S is Cohen-Macauley" then they begin to question what kind of crazy system you are using which cannot deduce this immediately. As an interesting experiment, find your favourite mathematician, preferably one who does not know what a Cohen-Macauley ring is, and ask them whether they think it will be true that if R and S are isomorphic rings and R is Cohen-Macauley then S is too. They will be very confident that this is true, even if they do not know the definition; standard mathematical definitions are isomorphism-invariant. This is part of our code of conduct, in fact. > >>>> > >>>> However in Lean I believe that the current plan is to try and make a tactic which will resolve this issue. This has not yet been done, and as far as I can see this is a place where UniMath is a more natural fit for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points for it, which Lean manages to get over more easily. That is somehow where I'm coming from. > >>>> > >>>>> > >>>>> For example, say you have a theorem about bimodules over semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.” Is that step something you’d be able to deal with easily in Lean? If not, that’s somewhere that down the line HoTT might make things more practical. > >>>> > >>>> > >>>> This is a great example! To be honest I am slightly confused about why we are not running into this sort of thing already. As far as I can see this would be a great test case for the (still very much under development) transport tactic. Maybe we don't have enough classification theorems. I think that our hope in general is that this sort of issue can be solved with automation. > >>>> > >>>> Kevin > >>>> > >>>> > >>>>> > >>>>> But mostly I just want to say you’re making a category error in your question. HoTT is an abstract type theory, not a proof assistant. > >>>>> > >>>>> Best, > >>>>> > >>>>> Noah > >>>>> > >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote: > >>>>>> > >>>>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the "additivity axiom". Please let me know if the following formulation of the such axiom is correct: > >>>>>> > >>>>>> > >>>>>> > >>>>>> > >>>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: > >>>>>>> > >>>>>>> A useful example for you might be Floris van Doorn’s formalization of > >>>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology > >>>>>>> in HoTT using Lean: > >>>>>>> > >>>>>>> https://arxiv.org/abs/1808.10690 > >>>>>>> > >>>>>>> Regards, > >>>>>>> > >>>>>>> Steve > >>>>>>> > >>>>>>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> wrote: > >>>>>>> > > >>>>>>> > Hi from a Lean user. > >>>>>>> > > >>>>>>> > As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others. > >>>>>>> > > >>>>>>> > I have seen enough of Lean to become convinced that the pain points would be surmountable in Lean. I have seen enough of Isabelle/HOL to become skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings. > >>>>>>> > > >>>>>>> > I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a blessing and a curse. However I would like to know more details. I am speaking at the Big Proof conference in Edinburgh this coming Wednesday on the pain points involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT. > >>>>>>> > > >>>>>>> > Everyone will have a different interpretation of "modern pure mathematics" so to fix our ideas, let me say that for the purposes of this discussion, "modern pure mathematics" means the statements of the theorems publishsed by the Annals of Mathematics over the last few years, so for example I am talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the like; one can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is. > >>>>>>> > > >>>>>>> > If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics). > >>>>>>> > > >>>>>>> > Kevin Buzzard > >>>>>>> > > >>>>>>> > -- > >>>>>>> > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. > >>>>>>> > For more options, visit https://groups.google.com/d/optout. > >>>>>>> > >>>>>> -- > >>>>>> 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com. > >>>>>> For more options, visit https://groups.google.com/d/optout. > >>>>> > >>>>> -- > >>>>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com. > >>>>> > >>>>> > >>>>> For more options, visit https://groups.google.com/d/optout. > >>> > >>> -- > >>> 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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com. > >>> For more options, visit https://groups.google.com/d/optout. -- 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/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3A%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 2967 bytes --] On Sunday, May 26, 2019 at 12:00:21 PM UTC-5, Kevin Buzzard wrote: > > ... But looking at > the things he formalised, he was doing things like the p-adic numbers, > and lots and lots of category theory. I am surprised that he did not > attempt to formalise the basic theory of schemes. > UniMath was formed from Voevodsky's Foundations (see https://github.com/UniMath/Foundations ) and some formalizations based on it by other people, starting with Benedikt Ahrens and me, and continuing with many others. In particular, the formalization of category theory began with Ahrens' formalization of the material in a joint paper of his with Kapulkin and Shulman, see https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/README.md , and has been continued by other people, not Voevodsky. Voevodsky was probably too busy writing his papers on the semantics of the system to turn to formalizing the basic theory of schemes. For a while he said he wasn't even interested in formalizing his proof of the Milnor conjecture, because he was confident it was correct. Then later he said, in a talk, that it would be important top find a constructive proof of the Milnor conjecture, and to formalize it, pinpointing a particular argument due to Merkurjev and Suslin as being non-constructive, see the remark under the entry at http://www.math.ias.edu/Voevodsky/voevodsky-publications_abstracts.html#UniMath-1 I also remember, perhaps in early 2014, that he told me he was thinking of formalizing the definition of scheme (or maybe variety) so he could talk about it at a forthcoming talk, but he never did that. Eventually UniMath should have the theory of schemes in it. By the way, to go back to your original question, I think there are no "pain points" in formalizing traditional mathematics in UniMath. The pain and challenge seem only to come when generalizing traditional facts about sets so they apply also to types that are not assumed to be sets. For an example of that, see Peter Lumsdaine's proof of transfinite induction into a family of types at https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/WellFoundedRelations.v#L208 or see our proof with Bezem and Buchholtz that the type of ℤ-torsors satisfies the induction principle into a family of types that the circle satisfies, at https://github.com/UniMath/SymmetryBook/blob/master/ZTors.tex -- 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/d57bb2de-ff98-484b-8bc0-9c3f31620a47%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 4318 bytes --]

On 25/05/2019 18.41, Noah Snyder wrote: > (When I was using Agda the situation was even worse, things like > pattern matching secretly assumed k even if you used the without-k > option, and HITs were put in by a hack that wasn't totally clear if it > worked, etc.) Things are a bit better now. Jesper Cockx and others have worked out a better story for --without-K, and Anders Mörtberg, Andrea Vezzosi and others have implemented --cubical, with direct support for HITs. -- /NAD -- 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/0e51ad31-29cb-d054-5e96-1544732f47eb%40cse.gu.se. For more options, visit https://groups.google.com/d/optout.

Dear Bas, dear all, thanks for the advertising this work. A small clarification: Le 26/05/2019 à 14:09, Bas Spitters a écrit : > > If you want to restrict to classical maths. Then please have a careful > look at how its done in mathematical components: > https://math-comp.github.io/mcb/ the mathematical components library is about constructive mathematics and is formalized in CIC (Gallina) without axiom ... > and the analysis library that is currently under development. > https://github.com/math-comp/analysis ... but the analysis one is indeed about classical mathematics. Best wishes, assia > If you went to help connecting this to the HoTT library, it will be > much appreciated. > https://github.com/HoTT/HoTT > > Best wishes, > > Bas > > On Sun, May 26, 2019 at 1:41 PM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: >> >> It seems to me, now I understand much better what is going on (many thanks to all the people who replied) that dependent type theory + impredicative prop "got lucky", in that Coq has been around for a long time, and Lean 3 is an attempt to model basically the same type theory but in a way more suited to mathematics, written by someone who knows what they're doing (de Moura). Using nonconstructive maths e.g. LEM or AC etc in Lean 3 is just a matter of writing some incantation at the top of a file and then not thinking about it any more. HoTT might be more appropriate for mathematics -- or at least for some kinds of mathematics -- but its implementation in an actual piece of software seems a bit more hacky at this point ("use Coq, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean documentation is not ideal for mathematicians -- mathematicians need very early on to be able to use tactics such as `ring` or `norm_num` to do calculations with real numbers or in commutative rings, and these tactics are not even mentioned in the standard Lean documentation. >> >> I am a working mathematician who two years ago knew nothing about this way of doing mathematics on a computer. Now I have seen what is possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians do not see the point of it, or what it has to offer a modern working mathematician; they can see no immediate benefits in learning how this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists are there in an average maths department? In the UK at least, the answer is "much less than 1", and I cannot see that changing any time soon. I would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least make mathematicians sit up and take notice, but when I look at what has been done in these various systems I do not see this occurring. This weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic analysis? Where is the stuff which draws mathematicians in? This by no means a criticism of unimath -- it is in fact a far more broad criticism of all of the systems out there. Lean 3 might have schemes but they still can't prove that the derivative of sin is cos, and Isabelle/HOL might never have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) when formalising the odd order theorem in Coq, but it turns out that the odd order theorem is perhaps not a good "selling point" for mathematics formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will work, but that looks to me like a complete fantasy at this point. >> >> One thing I have learnt over the last two years is that a whole bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians to sit up and take notice? I guess we simply do not know, but if there is, I hope I'm still around. >> >> Kevin >> >> >> >> On Sun, 26 May 2019 at 06:50, Bas Spitters <b.a.w.spitters@gmail.com> wrote: >>> >>> There has been progress in making a cleaner interface with the standard Coq tactics. (Some abstractions were broken at the ocaml level) >>> I'm hopeful that this can be lead to a clean connection between the HoTT library and more of the Coq developments in the not too distant future. >>> As it exists in agda now. >>> >>> IIUC, UniMath does not allow any of the standard library or it's tactics, or even record types, since Vladimir wanted to have a very tight connection between type theory and it's semantics in simplicial sets. So, I don't expect them to connect to other developments, but I could be wrong. >>> >>> About the bundled/unbundled issue, which also exists in Coq, there's some recent progress "frame type theory" which should be applicable to both Coq and lean: >>> http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51 >>> >>> Coming back to Kevin's question, yes, HoTT (plus classical logic for sets), seems to be the most natural foundation for mathematics as is currently published in the Annals. >>> >>> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote: >>>> >>>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library." “Coq with the indices-matter option plus the HoTT library" is of the same category as "Lean plus the math library" and then it makes sense to compare how practically useful they are for math. >>>> >>>> Here it's important to note that most advanced things that you can do in Coq are broken by using the "indices-matter" option and relatedly not using the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04591 "This small change makes the whole standard library unusable, and many tactics stop working, too. The solution was rather drastic: we ripped out the standard library and replaced it with a minimal core that is sufficient for the basic tactics to work." >>>> >>>> (In particular, I was in error in my previous email, *some* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical calculations.) >>>> >>>> I should say I've never used Coq, just Agda. (When I was using Agda the situation was even worse, things like pattern matching secretly assumed k even if you used the without-k option, and HITs were put in by a hack that wasn't totally clear if it worked, etc.) So I'm likely wrong in some places above. >>>> >>>> So I think from a practical point of view, “Coq with the indices-matter option plus the HoTT library" is well behind ordinary Coq (and also Lean) for doing ordinary mathematics. However, if and when it does catch up some of the pain points involving transporting from my previous email should go away automatically. (Side comment: once you start talking about transporting stuff related to categories across equivalences of categories it's only going to get more painful in ordinary type theory, but will remain easy in HoTT approaches.) >>>> >>>> Best, >>>> >>>> Noah >>>> >>>> p.s. Installed Lean last week. Looking forward to using it next year when Scott and I are both at MSRI. >>>> >>>> On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: >>>>> >>>>> Hi Noah. Thank you for pointing out the category error. It seems to me that sometimes when I say "HoTT" I should be saying, for example, "UniMath". >>>>> >>>>> Tactics in Lean are absolutely crucial for library development. Coq has some really powerful tactics, right? UniMath can use those tactics, presumably? >>>>> >>>>> I understand that UniMath, as implemented in Coq, takes Coq and adds some "rules" of the form "you can't use this functionality" and also adds at least one new axiom (univalence). >>>>> >>>>> On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote: >>>>>> >>>>>> I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s better. >>>>> >>>>> >>>>> But plain Coq has such types, right? >>>>> >>>>> OK so this has all been extremely informative. There are other provers being developed which will implement some flavour of HoTT more "faithfully", and it might be easier to develop maths libraries in such provers. >>>>> >>>>>> For example, if G and H are isomorphic groups and you want to translate a theorem or construction across the isomorphism. In ordinary type theory this is going to involve annoying book-keeping which it seems like you’d have to do separately for each kind of mathematical object. >>>>> >>>>> >>>>> Yes. This is a pain point in Lean. It's a particularly nasty one too, as far as mathematicians are concerned, because when you tell a mathematician "well this ring R is Cohen-Macauley, and here's a ring S which is isomorphic to R, but we cannot immediately deduce in Lean that S is Cohen-Macauley" then they begin to question what kind of crazy system you are using which cannot deduce this immediately. As an interesting experiment, find your favourite mathematician, preferably one who does not know what a Cohen-Macauley ring is, and ask them whether they think it will be true that if R and S are isomorphic rings and R is Cohen-Macauley then S is too. They will be very confident that this is true, even if they do not know the definition; standard mathematical definitions are isomorphism-invariant. This is part of our code of conduct, in fact. >>>>> >>>>> However in Lean I believe that the current plan is to try and make a tactic which will resolve this issue. This has not yet been done, and as far as I can see this is a place where UniMath is a more natural fit for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points for it, which Lean manages to get over more easily. That is somehow where I'm coming from. >>>>> >>>>>> >>>>>> For example, say you have a theorem about bimodules over semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.” Is that step something you’d be able to deal with easily in Lean? If not, that’s somewhere that down the line HoTT might make things more practical. >>>>> >>>>> >>>>> This is a great example! To be honest I am slightly confused about why we are not running into this sort of thing already. As far as I can see this would be a great test case for the (still very much under development) transport tactic. Maybe we don't have enough classification theorems. I think that our hope in general is that this sort of issue can be solved with automation. >>>>> >>>>> Kevin >>>>> >>>>> >>>>>> >>>>>> But mostly I just want to say you’re making a category error in your question. HoTT is an abstract type theory, not a proof assistant. >>>>>> >>>>>> Best, >>>>>> >>>>>> Noah >>>>>> >>>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote: >>>>>>> >>>>>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the "additivity axiom". Please let me know if the following formulation of the such axiom is correct: >>>>>>> >>>>>>> >>>>>>> >>>>>>> >>>>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: >>>>>>>> >>>>>>>> A useful example for you might be Floris van Doorn’s formalization of >>>>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology >>>>>>>> in HoTT using Lean: >>>>>>>> >>>>>>>> https://arxiv.org/abs/1808.10690 >>>>>>>> >>>>>>>> Regards, >>>>>>>> >>>>>>>> Steve >>>>>>>> >>>>>>>>> On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> wrote: >>>>>>>>> >>>>>>>>> Hi from a Lean user. >>>>>>>>> >>>>>>>>> As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others. >>>>>>>>> >>>>>>>>> I have seen enough of Lean to become convinced that the pain points would be surmountable in Lean. I have seen enough of Isabelle/HOL to become skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings. >>>>>>>>> >>>>>>>>> I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a blessing and a curse. However I would like to know more details. I am speaking at the Big Proof conference in Edinburgh this coming Wednesday on the pain points involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT. >>>>>>>>> >>>>>>>>> Everyone will have a different interpretation of "modern pure mathematics" so to fix our ideas, let me say that for the purposes of this discussion, "modern pure mathematics" means the statements of the theorems publishsed by the Annals of Mathematics over the last few years, so for example I am talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the like; one can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is. >>>>>>>>> >>>>>>>>> If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics). >>>>>>>>> >>>>>>>>> Kevin Buzzard >>>>>>>>> >>>>>>>>> -- >>>>>>>>> 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. >>>>>>>>> For more options, visit https://groups.google.com/d/optout. >>>>>>>> >>>>>>> -- >>>>>>> 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com. >>>>>>> For more options, visit https://groups.google.com/d/optout. >>>>>> >>>>>> -- >>>>>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com. >>>>>> >>>>>> >>>>>> For more options, visit https://groups.google.com/d/optout. >>>> >>>> -- >>>> 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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com. >>>> For more options, visit https://groups.google.com/d/optout. > -- 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/3f6331a7-688e-570b-01d8-d02a81eac96b%40inria.fr. For more options, visit https://groups.google.com/d/optout.

In my opinion there are several separate issues standing in the way of a wider use of proof assistants. One has to do with the design of the underlying formal systems. In this respect Book HoTT (the formal system of the homotopy type theory book, with univalence and higher inductive types added in an "ad hoc" way on top of intensional Martin-Lof type theory) is a step forward over systems such as CiC and MLTT on which Coq and Agda are based, due to various factors such as a nice treatment of quotients, automatic isomorphism-invariance, inductive and free constructions, etc. However, Book HoTT is also a step backwards, because the presence of non-computational "axioms" means that "execution" gets stuck whenever you try to use univalence. So you can prove automatically that anything true about a group G is true about an isomorphic group H, but if you then try to take some specific statement about some specific group G and transfer it to a specific statement about a specific group H along a specific isomorphism, what you'll get will be an unreadable statement littered with explicit transports across univalence-induced paths in the universe, rather than the "real" statement about H that should be obtained from actually *applying* that specific isomorphism. (To be fair, plenty of people using a system like Coq pre-HoTT had to add their own axioms, such as function extensionality and UIP, and when you want classical logic that's unavoidably an axiom. But at least the underlying type theory of Coq and Agda can "compute".) More modern homotopy type theories, which are generally based on cubical structures, allow univalence to be "executed" by the system. However, these systems lack (so far) all the intended categorical semantics (see below), and haven't yet been implemented in "real world" proof assistants (though there are prototypes now in use and development). In addition, as Noah mentioned, two-level theories with a stricter kind of equality (which do *not* exist in UniMath, HoTT/Coq, or HoTT/Agda -- this point is about having two different equalities on the same type, not two different classes of types with different equality behavior) are likely to make many things easier, but haven't been implemented in real-world proof assistants either (apart from some sneaky coding with typeclasses). So overall, I would say that the underlying design of homotopy type theories is not yet "in order" to achieve its hoped-for maximal benefit in a proof assistant by the working mathematician, though there are promising signs and progress is being made. All the issues discussed above are what I would call "mathematical", or perhaps more broadly "theoretical". But a separate issue standing in the way of wider use of proof assistants is what I would call "engineering". No matter how fancy we make the underlying formal system, I believe it will always remain true (for the foreseeable future) that a proof assistant needs a lot more detailed information than an ordinary mathematician would care to provide, or need to see, in writing and understanding a proof. This is where we need things like tactics, implicit arguments, elaboration, proof automation, etc. to fill in the gaps and make the system usable in practice. Here there's been a lot of progress over the past decades, but I think there's a long way to go too, and choosing a better underlying foundation (like any form of HoTT, cubical or otherwise) may improve things a bit but is not really a game-changer. However, there's something completely different that I do believe has the potential to be a game-changer. There's already a very different "gigantic wave crashing through mathematics": homotopy theory and higher category theory. Homotopy type theory gives type theory and formalization the potential to ride that wave. The real point here is that when something is formalized in type theory -- constructively -- it is automatically true internally in all models of type theory, and for homotopy type theory those models include higher categories. Note that the use of constructive logic has nothing to do with any philosophical belief; classical logic can still be "true" in the "real world", and yet constructive reasoning is valuable because it makes a theorem true internally in more categories. I think it's fairly hopeless to convince a classical mathematician that they should put in a lot of work to convince a computer of the truth of *something they already knew*. But I have much more hope of convincing them that they should tweak their proofs slightly, and perhaps use a computer to help verify the validity of the tweaks, in order that *essentially the same proof* will allow them to conclude a *vastly more general theorem*. Moreover, when working with higher categories the advantage is even more pronounced, because homotopy type theories introduce a totally new kind of proof that can be much simpler than all the previously available options -- and the immediate feedback involved in using a proof assistant is one of the best ways to *learn* that style of proof. In short, I think there's a huge public relations opportunity here for type theory and computer formalization, which sadly even Voevodsky missed out on. Rather than selling it as a way to be absolutely sure of proofs we already believe in (as important as that might be), we should sell it as a framework for *entirely new proofs* that bring the otherwise fiendishly complicated and technical world of higher category theory "down to earth". The experts in higher category theory are familiar with the fact that in many respects it is "more natural" and "better behaved" than ordinary category theory; but there are thick barriers to entry preventing many of us from getting to that point of expertise. With synthetic mathematics in homotopy type theory, we can envision one day teaching higher category theory to undergraduates. -- 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/CAOvivQx_b2QkEL-HqMXQNJ_QA83KjdAnFe7RmmiPRRQX6tYk-A%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

On 28/05/2019 11.50, Michael Shulman wrote: > More modern homotopy type theories, which are generally based on > cubical structures, allow univalence to be "executed" by the system. > However, these systems lack (so far) all the intended categorical > semantics (see below), and haven't yet been implemented in "real > world" proof assistants (though there are prototypes now in use and > development). The latest release of Agda can be used in cubical mode, and supports both univalence and higher inductive types. (As well as things like higher inductive-coinductive-recursive types that may not have a proper explanation.) -- /NAD -- 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/9232f85a-6d64-84dc-a2d0-290c0fc6e760%40cse.gu.se. For more options, visit https://groups.google.com/d/optout.

Of course Agda is a real-world proof assistant, but its cubical mode is still new and experimental, so I was counting it as a "prototype". But I suppose that's not really fair, since unlike a custom-developed prototype it presumably benefits from all the usability superstructure of Agda. Sorry! On Tue, May 28, 2019 at 3:13 AM Nils Anders Danielsson <nad@cse.gu.se> wrote: > > On 28/05/2019 11.50, Michael Shulman wrote: > > More modern homotopy type theories, which are generally based on > > cubical structures, allow univalence to be "executed" by the system. > > However, these systems lack (so far) all the intended categorical > > semantics (see below), and haven't yet been implemented in "real > > world" proof assistants (though there are prototypes now in use and > > development). > > The latest release of Agda can be used in cubical mode, and supports > both univalence and higher inductive types. (As well as things like > higher inductive-coinductive-recursive types that may not have a proper > explanation.) > > -- > /NAD > > -- > 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/9232f85a-6d64-84dc-a2d0-290c0fc6e760%40cse.gu.se. > For more options, visit https://groups.google.com/d/optout. -- 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/CAOvivQyPDzzjLEQfB%3DC5jQSH8wzFpr%3DgG8E_4BSWaBtb95mg3w%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

Dear Mike, I would like to add my grain of salt to the discussion. I think that mathematical research is more a communal activity than we think. What is considered a proof largely depends on a consensus developed within the mathematical community. Of course, the consensus relies on the opinions of experts and specialists. Publications and referees have an important role. But there is also a mathematical culture based on knowledge of abstract ideas and the mastery of symbolic computations. Homotopy type theory is contributing to the present mathematical culture by bringing a new formalism and new abstract ideas. It claims to be constructive and general (everything is a type). There is an old philosophical debate concerning constructive mathematics that was initiated by the work of Cantor, Kronecker, Hilbert, Brouwer and Bishop, to name a few. It is true that a constructive theorem is in a sense better and more general. In reality, constructive and non-constructive mathematics are the two faces of the same coin. The latter is feeding the former with results to be proved constructively! It seems obvious that the debate will endure for many generations to come. I believe that the contributions of homotopy type theory to the mathematical culture are important and real. It is worth developing abstractly and for the purpose of creating user-friendly powerful proof assistants. The language of type theory includes parametrised objects, sums, products, universes and univalence. It is not incompatible with the language of category theory and of homotopy theory. Hopefully, the three languages will be combined. Best, andré ________________________________________ From: homotopytypetheory@googlegroups.com [homotopytypetheory@googlegroups.com] on behalf of Michael Shulman [shulman@sandiego.edu] Sent: Tuesday, May 28, 2019 5:50 AM To: Kevin Buzzard Cc: Homotopy Type Theory Subject: Re: [HoTT] doing "all of pure mathematics" in type theory In my opinion there are several separate issues standing in the way of a wider use of proof assistants. One has to do with the design of the underlying formal systems. In this respect Book HoTT (the formal system of the homotopy type theory book, with univalence and higher inductive types added in an "ad hoc" way on top of intensional Martin-Lof type theory) is a step forward over systems such as CiC and MLTT on which Coq and Agda are based, due to various factors such as a nice treatment of quotients, automatic isomorphism-invariance, inductive and free constructions, etc. However, Book HoTT is also a step backwards, because the presence of non-computational "axioms" means that "execution" gets stuck whenever you try to use univalence. So you can prove automatically that anything true about a group G is true about an isomorphic group H, but if you then try to take some specific statement about some specific group G and transfer it to a specific statement about a specific group H along a specific isomorphism, what you'll get will be an unreadable statement littered with explicit transports across univalence-induced paths in the universe, rather than the "real" statement about H that should be obtained from actually *applying* that specific isomorphism. (To be fair, plenty of people using a system like Coq pre-HoTT had to add their own axioms, such as function extensionality and UIP, and when you want classical logic that's unavoidably an axiom. But at least the underlying type theory of Coq and Agda can "compute".) More modern homotopy type theories, which are generally based on cubical structures, allow univalence to be "executed" by the system. However, these systems lack (so far) all the intended categorical semantics (see below), and haven't yet been implemented in "real world" proof assistants (though there are prototypes now in use and development). In addition, as Noah mentioned, two-level theories with a stricter kind of equality (which do *not* exist in UniMath, HoTT/Coq, or HoTT/Agda -- this point is about having two different equalities on the same type, not two different classes of types with different equality behavior) are likely to make many things easier, but haven't been implemented in real-world proof assistants either (apart from some sneaky coding with typeclasses). So overall, I would say that the underlying design of homotopy type theories is not yet "in order" to achieve its hoped-for maximal benefit in a proof assistant by the working mathematician, though there are promising signs and progress is being made. All the issues discussed above are what I would call "mathematical", or perhaps more broadly "theoretical". But a separate issue standing in the way of wider use of proof assistants is what I would call "engineering". No matter how fancy we make the underlying formal system, I believe it will always remain true (for the foreseeable future) that a proof assistant needs a lot more detailed information than an ordinary mathematician would care to provide, or need to see, in writing and understanding a proof. This is where we need things like tactics, implicit arguments, elaboration, proof automation, etc. to fill in the gaps and make the system usable in practice. Here there's been a lot of progress over the past decades, but I think there's a long way to go too, and choosing a better underlying foundation (like any form of HoTT, cubical or otherwise) may improve things a bit but is not really a game-changer. However, there's something completely different that I do believe has the potential to be a game-changer. There's already a very different "gigantic wave crashing through mathematics": homotopy theory and higher category theory. Homotopy type theory gives type theory and formalization the potential to ride that wave. The real point here is that when something is formalized in type theory -- constructively -- it is automatically true internally in all models of type theory, and for homotopy type theory those models include higher categories. Note that the use of constructive logic has nothing to do with any philosophical belief; classical logic can still be "true" in the "real world", and yet constructive reasoning is valuable because it makes a theorem true internally in more categories. I think it's fairly hopeless to convince a classical mathematician that they should put in a lot of work to convince a computer of the truth of *something they already knew*. But I have much more hope of convincing them that they should tweak their proofs slightly, and perhaps use a computer to help verify the validity of the tweaks, in order that *essentially the same proof* will allow them to conclude a *vastly more general theorem*. Moreover, when working with higher categories the advantage is even more pronounced, because homotopy type theories introduce a totally new kind of proof that can be much simpler than all the previously available options -- and the immediate feedback involved in using a proof assistant is one of the best ways to *learn* that style of proof. In short, I think there's a huge public relations opportunity here for type theory and computer formalization, which sadly even Voevodsky missed out on. Rather than selling it as a way to be absolutely sure of proofs we already believe in (as important as that might be), we should sell it as a framework for *entirely new proofs* that bring the otherwise fiendishly complicated and technical world of higher category theory "down to earth". The experts in higher category theory are familiar with the fact that in many respects it is "more natural" and "better behaved" than ordinary category theory; but there are thick barriers to entry preventing many of us from getting to that point of expertise. With synthetic mathematics in homotopy type theory, we can envision one day teaching higher category theory to undergraduates. -- 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/CAOvivQx_b2QkEL-HqMXQNJ_QA83KjdAnFe7RmmiPRRQX6tYk-A%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. -- 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/8C57894C7413F04A98DDF5629FEC90B15872D76E%40Pli.gst.uqam.ca. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 2167 bytes --] Thanks for this discussion. I like it. Maybe I would like to argue with this point: On 28/05/2019 10:50, Michael Shulman wrote: > I think it's fairly hopeless to convince a classical mathematician > that they should put in a lot of work to convince a computer of the > truth of *something they already knew*. I am not sure why the person who started this thread, a mathematician, Kevin Buzzard, decided to put in such a lot of work, but did and he has (in Lean), with his students. But having interacted with a lot of students (from my institution, and from everywhere in the world, from maths, logic, computer science and philosophy departments (and once even a high school student in the UniMath School)), what I can say is that they are not trying to convince the computer. They are trying to convince themselves, using the computer to both check their understanding and record their understanding when the proof is complete. If I am allowed to speak for myself, I created a univalent library in Agda for the purpose of *doing something else*. However, it is nice to stare at the library and see everything developed from first principles. When presented with the mathematical literature, both as students and experienced mathematicians, we are never sure how far back one has to read until everything begins in a precise way. How much have we created, and how do all the different fields of mathematics interact with each other? When one records mathematics in the computer, this begins to become clear, or at least the asnwers to such questions become possible. We don't need to *convince* anybody. This will *happen*. And it is already happening. The students like it. This is my experience. M. -- 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/c7197bc2-7fc5-4027-bed6-24b2d350950f%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 2986 bytes --]

Thanks Martin! Of course you are right that there are people who don't need to be convinced and who derive benefit and pleasure from their formalization efforts, and in our community we probably encounter a lot of them. However, I still maintain that the *average* working mathematician is not yet going to find such work useful or rewarding for its own sake. If you go to, say, the U.S. Joint Mathematics Meetings and stop a hundred mathematicians at random in the lobby and ask whether they have ever formalized their work in a proof assistant, how many do you think will say yes? Perhaps I am too pessimistic. But let me in turn offer myself as an example: in addition to being a homotopy type theorist, I have another hat as a classical category theorist and homotopy theorist. When I prove things in HoTT, I often formalize them in a proof assistant. But when I prove things in classical mathematics, I very rarely consider formalizing them. Only once have I formalized a proof in classical category theory; the experience was more time-consuming and less enjoyable than I expected, and I have no plans to do it again. And I expect that as classical mathematicians go, I am (even when I have my classical mathematician hat on) pretty far on the sympathetic-to-formalization side of the spectrum. On Wed, May 29, 2019 at 12:05 PM Martín Hötzel Escardó <escardo.martin@gmail.com> wrote: > > Thanks for this discussion. I like it. > > Maybe I would like to argue with this point: > > On 28/05/2019 10:50, Michael Shulman wrote: > > I think it's fairly hopeless to convince a classical mathematician > > that they should put in a lot of work to convince a computer of the > > truth of *something they already knew*. > > I am not sure why the person who started this thread, a mathematician, > Kevin Buzzard, decided to put in such a lot of work, but did and he > has (in Lean), with his students. > > But having interacted with a lot of students (from my institution, and > from everywhere in the world, from maths, logic, computer science and > philosophy departments (and once even a high school student in the > UniMath School)), what I can say is that they are not trying to > convince the computer. > > They are trying to convince themselves, using the computer to both > check their understanding and record their understanding when > the proof is complete. > > If I am allowed to speak for myself, I created a univalent library in > Agda for the purpose of *doing something else*. However, it is nice to > stare at the library and see everything developed from first > principles. When presented with the mathematical literature, both as > students and experienced mathematicians, we are never sure how far > back one has to read until everything begins in a precise way. How > much have we created, and how do all the different fields of > mathematics interact with each other? When one records mathematics in > the computer, this begins to become clear, or at least the asnwers to such > questions become possible. > > We don't need to *convince* anybody. This will *happen*. And it is > already happening. The students like it. This is my experience. > > M. > > > -- > 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/c7197bc2-7fc5-4027-bed6-24b2d350950f%40googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- 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/CAOvivQxAZEXiCSS5%2BipOszo%3DJeymDXL3jyfuNFdY7AKxAZSS4g%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1: Type: text/plain, Size: 23912 bytes --] Dear Kevin, Looking at your slides from big proof, the transfer package you're asking for seems to be very close to what is provided by HoTT. https://xenaproject.wordpress.com/2019/06/02/equality-part-3-canonical-isomorphism/ This is explained in many places (e.g. the book). Here's an early article explaining it for algebraic structures: http://www.cse.chalmers.se/~nad/publications/coquand-danielsson-isomorphism-is-equality.pdf Have you looked at any of this? Does it provide what you are looking for? Best, Bas On Sun, May 26, 2019 at 7:00 PM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > I would like to again thank the people who have been responding to my > posts this weekend with links and further reading. I know the Lean > literature but I knew very little indeed about HoTT / UniMath at the > start of this weekend; at least now I feel like I know where you guys > are. > > On Sun, 26 May 2019 at 13:09, Bas Spitters <b.a.w.spitters@gmail.com> > wrote: > > > It's a slow process, but I believe we are making progress. > > I agree that it's a slow process! I think that in any computer science > department you can find people who know about these tools, indeed in > the computer science department at my university there are people > using things like Coq for program verification. I think that one > measure of success would be when in most mathematics departments you > can find someone who knows about this stuff. My personal experience is > that we seem to be far from this, at this point. Bas points out the > EU-funded project ForMath and I know that Paulson has an EU grant in > Cambridge for Isabelle (my impression is that it is centred in the > computer science department) and there is a Lean one based in > Amsterdam which I know has mathematicians involved. For me the shock > is that now I've seen what these things can do, I am kind of stunned > that mathematicians don't know more about them. > > > You seem to be mixing at least two issues. > > - HoTT/UF as a foundation > > - Current implementations in proof assistants. > > Yes; when I started this thread I was very unclear about how > everything fitted together. I asked a bit on the Lean chat but I guess > many people are like me -- they know one system, and are not experts > at all in what is going on with the other systems. > > I had forgotten about the mathcomp book! Someone pointed it out to me > a while ago but I knew far less then about everything so it was a bit > more intimidating. Thanks for reminding me. > > I think I have basically said all I had to say (and have managed to > get my ideas un-muddled about several things). But here is a parting > shot. Voevodsky was interested in formalising mathematics in a proof > assistant. Before that, Voevodsky was a "traditional mathematician" > and proved some great theorems and made some great constructions using > mathematical objects called schemes. Theorems about schemes (his > development of a homotopy theory for schemes) are what got him his > Fields Medal. Schemes were clearly close to his heart. But looking at > the things he formalised, he was doing things like the p-adic numbers, > and lots and lots of category theory. I am surprised that he did not > attempt to formalise the basic theory of schemes. Grothendieck's EGA > is written in quite a "formal" way (although nowhere near as formal as > what would be needed to formalise it easily in a proof assistant) and > Johan de Jong's Stacks Project https://stacks.math.columbia.edu/ is > another very solid attempt to lay down the foundations of the theory. > I asked Johan whether he now considered his choice of "nice web pages" > old-fashioned when it was now possible to formalise things in a proof > assistant, and he said that he did not have time to learn how to use a > proof assistant. But Voevodsky was surely aware of this work, and also > how suitable it looks for formalisation. > > Thanks again to this community for all the comments and all the links > and all the corrections. If anyone is going to Big Proof in Edinburgh > this coming week I'd be happy to talk more. > > Kevin > > > > > If you want to restrict to classical maths. Then please have a careful > > look at how its done in mathematical components: > > https://math-comp.github.io/mcb/ > > and the analysis library that is currently under development. > > https://github.com/math-comp/analysis > > > > If you went to help connecting this to the HoTT library, it will be > > much appreciated. > > https://github.com/HoTT/HoTT > > > > Best wishes, > > > > Bas > > > > On Sun, May 26, 2019 at 1:41 PM Kevin Buzzard <kevin.m.buzzard@gmail.com> > wrote: > > > > > > It seems to me, now I understand much better what is going on (many > thanks to all the people who replied) that dependent type theory + > impredicative prop "got lucky", in that Coq has been around for a long > time, and Lean 3 is an attempt to model basically the same type theory but > in a way more suited to mathematics, written by someone who knows what > they're doing (de Moura). Using nonconstructive maths e.g. LEM or AC etc in > Lean 3 is just a matter of writing some incantation at the top of a file > and then not thinking about it any more. HoTT might be more appropriate for > mathematics -- or at least for some kinds of mathematics -- but its > implementation in an actual piece of software seems a bit more hacky at > this point ("use Coq, but don't use these commands or these tactics"), > which maybe raises the entry barrier for mathematicians a bit (and speaking > from personal experience, already this entry barrier is quite high). High > level tactics are absolutely crucial for mathematical Lean users. This is > one of the reasons that the Lean documentation is not ideal for > mathematicians -- mathematicians need very early on to be able to use > tactics such as `ring` or `norm_num` to do calculations with real numbers > or in commutative rings, and these tactics are not even mentioned in the > standard Lean documentation. > > > > > > I am a working mathematician who two years ago knew nothing about this > way of doing mathematics on a computer. Now I have seen what is possible I > am becoming convinced that it can really change mathematics. In my > experience the biggest obstruction to it changing mathematics is simply > that mathematicians do not see the point of it, or what it has to offer a > modern working mathematician; they can see no immediate benefits in > learning how this stuff works. In short, I think type theory has an image > problem. Sure there are category theorists who know about it, but how many > category theorists are there in an average maths department? In the UK at > least, the answer is "much less than 1", and I cannot see that changing any > time soon. I would love to draw the mathematics and computer science > communities closer together over ideas like this, but it's hard work. I am > wondering whether developing accessible databases of undergraduate level > mathematics would at least make mathematicians sit up and take notice, but > when I look at what has been done in these various systems I do not see > this occurring. This weekend I've learnt something about UniMath, but > whilst it might do bicategories very well (which are not on our > undergraduate curriculum), where is the basic analysis? Where is the stuff > which draws mathematicians in? This by no means a criticism of unimath -- > it is in fact a far more broad criticism of all of the systems out there. > Lean 3 might have schemes but they still can't prove that the derivative of > sin is cos, and Isabelle/HOL might never have schemes. I know that Gonthier > and his coauthors had to make a lot of undergraduate level maths (Galois > theory, algebraic number theory, group theory) when formalising the odd > order theorem in Coq, but it turns out that the odd order theorem is > perhaps not a good "selling point" for mathematics formalisation when > you're trying to sell to "normal research mathematicians", and I don't know > what is. I'm now wondering making formalised undergraduate mathematics more > accessible to untrained mathematicians is a better approach, but who knows. > Obviously "AI which can solve the Riemann hypothesis" will work, but that > looks to me like a complete fantasy at this point. > > > > > > One thing I have learnt over the last two years is that a whole bunch > of extremely smart people, both mathematicians and computer scientists, > have invested a lot of time in thinking about how to do mathematics with > type theory. I find it very frustrating that mathematicians are not > beginning to notice. Of course there are exceptions. One day though -- will > there simply be a gigantic wave which crashes through mathematics and > forces mathematicians to sit up and take notice? I guess we simply do not > know, but if there is, I hope I'm still around. > > > > > > Kevin > > > > > > > > > > > > On Sun, 26 May 2019 at 06:50, Bas Spitters <b.a.w.spitters@gmail.com> > wrote: > > >> > > >> There has been progress in making a cleaner interface with the > standard Coq tactics. (Some abstractions were broken at the ocaml level) > > >> I'm hopeful that this can be lead to a clean connection between the > HoTT library and more of the Coq developments in the not too distant future. > > >> As it exists in agda now. > > >> > > >> IIUC, UniMath does not allow any of the standard library or it's > tactics, or even record types, since Vladimir wanted to have a very tight > connection between type theory and it's semantics in simplicial sets. So, I > don't expect them to connect to other developments, but I could be wrong. > > >> > > >> About the bundled/unbundled issue, which also exists in Coq, there's > some recent progress "frame type theory" which should be applicable to both > Coq and lean: > > >> http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51 > > >> > > >> Coming back to Kevin's question, yes, HoTT (plus classical logic for > sets), seems to be the most natural foundation for mathematics as is > currently published in the Annals. > > >> > > >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> > wrote: > > >>> > > >>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a > category from “Coq with the indices-matter option plus the HoTT library." > “Coq with the indices-matter option plus the HoTT library" is of the same > category as "Lean plus the math library" and then it makes sense to compare > how practically useful they are for math. > > >>> > > >>> Here it's important to note that most advanced things that you can > do in Coq are broken by using the "indices-matter" option and relatedly not > using the built-in type Prop. Quoting from > https://arxiv.org/abs/1610.04591 "This small change makes the whole > standard library unusable, and many tactics stop working, too. The > solution was rather drastic: we ripped out the standard library and > replaced it with a minimal core that is sufficient for the basic tactics to > work." > > >>> > > >>> (In particular, I was in error in my previous email, *some* tactics > are available in Coq+indices-matter+HoTT, but not many of the more advanced > ones, and to my knowledge, not tactics needed for complicated homotopical > calculations.) > > >>> > > >>> I should say I've never used Coq, just Agda. (When I was using Agda > the situation was even worse, things like pattern matching secretly assumed > k even if you used the without-k option, and HITs were put in by a hack > that wasn't totally clear if it worked, etc.) So I'm likely wrong in some > places above. > > >>> > > >>> So I think from a practical point of view, “Coq with the > indices-matter option plus the HoTT library" is well behind ordinary Coq > (and also Lean) for doing ordinary mathematics. However, if and when it > does catch up some of the pain points involving transporting from my > previous email should go away automatically. (Side comment: once you start > talking about transporting stuff related to categories across equivalences > of categories it's only going to get more painful in ordinary type theory, > but will remain easy in HoTT approaches.) > > >>> > > >>> Best, > > >>> > > >>> Noah > > >>> > > >>> p.s. Installed Lean last week. Looking forward to using it next > year when Scott and I are both at MSRI. > > >>> > > >>> On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard < > kevin.m.buzzard@gmail.com> wrote: > > >>>> > > >>>> Hi Noah. Thank you for pointing out the category error. It seems to > me that sometimes when I say "HoTT" I should be saying, for example, > "UniMath". > > >>>> > > >>>> Tactics in Lean are absolutely crucial for library development. Coq > has some really powerful tactics, right? UniMath can use those tactics, > presumably? > > >>>> > > >>>> I understand that UniMath, as implemented in Coq, takes Coq and > adds some "rules" of the form "you can't use this functionality" and also > adds at least one new axiom (univalence). > > >>>> > > >>>> On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> > wrote: > > >>>>> > > >>>>> I’d also imagine that a “practical” implementation would likely > have some kind of “two-level” type theory where you can use types that > behave classically when that’s better and HoTT types when that’s better. > > >>>> > > >>>> > > >>>> But plain Coq has such types, right? > > >>>> > > >>>> OK so this has all been extremely informative. There are other > provers being developed which will implement some flavour of HoTT more > "faithfully", and it might be easier to develop maths libraries in such > provers. > > >>>> > > >>>>> For example, if G and H are isomorphic groups and you want to > translate a theorem or construction across the isomorphism. In ordinary > type theory this is going to involve annoying book-keeping which it seems > like you’d have to do separately for each kind of mathematical object. > > >>>> > > >>>> > > >>>> Yes. This is a pain point in Lean. It's a particularly nasty one > too, as far as mathematicians are concerned, because when you tell a > mathematician "well this ring R is Cohen-Macauley, and here's a ring S > which is isomorphic to R, but we cannot immediately deduce in Lean that S > is Cohen-Macauley" then they begin to question what kind of crazy system > you are using which cannot deduce this immediately. As an interesting > experiment, find your favourite mathematician, preferably one who does not > know what a Cohen-Macauley ring is, and ask them whether they think it will > be true that if R and S are isomorphic rings and R is Cohen-Macauley then S > is too. They will be very confident that this is true, even if they do not > know the definition; standard mathematical definitions are > isomorphism-invariant. This is part of our code of conduct, in fact. > > >>>> > > >>>> However in Lean I believe that the current plan is to try and make > a tactic which will resolve this issue. This has not yet been done, and as > far as I can see this is a place where UniMath is a more natural fit for > "the way mathematicians think". However now I've looked over what has > currently been formalised in UniMath I am wondering whether there are pain > points for it, which Lean manages to get over more easily. That is somehow > where I'm coming from. > > >>>> > > >>>>> > > >>>>> For example, say you have a theorem about bimodules over > semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can > assume both algebras are multimatrix algebras over division rings.” Is > that step something you’d be able to deal with easily in Lean? If not, > that’s somewhere that down the line HoTT might make things more practical. > > >>>> > > >>>> > > >>>> This is a great example! To be honest I am slightly confused about > why we are not running into this sort of thing already. As far as I can see > this would be a great test case for the (still very much under development) > transport tactic. Maybe we don't have enough classification theorems. I > think that our hope in general is that this sort of issue can be solved > with automation. > > >>>> > > >>>> Kevin > > >>>> > > >>>> > > >>>>> > > >>>>> But mostly I just want to say you’re making a category error in > your question. HoTT is an abstract type theory, not a proof assistant. > > >>>>> > > >>>>> Best, > > >>>>> > > >>>>> Noah > > >>>>> > > >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> > wrote: > > >>>>>> > > >>>>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the > "additivity axiom". Please let me know if the following formulation of the > such axiom is correct: > > >>>>>> > > >>>>>> > > >>>>>> > > >>>>>> > > >>>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: > > >>>>>>> > > >>>>>>> A useful example for you might be Floris van Doorn’s > formalization of > > >>>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology > > >>>>>>> in HoTT using Lean: > > >>>>>>> > > >>>>>>> https://arxiv.org/abs/1808.10690 > > >>>>>>> > > >>>>>>> Regards, > > >>>>>>> > > >>>>>>> Steve > > >>>>>>> > > >>>>>>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard < > kevin....@gmail.com> wrote: > > >>>>>>> > > > >>>>>>> > Hi from a Lean user. > > >>>>>>> > > > >>>>>>> > As many people here will know, Tom Hales' formal abstracts > project https://formalabstracts.github.io/ wants to formalise many of the > statements of modern pure mathematics in Lean. One could ask more generally > about a project of formalising many of the statements of modern pure > mathematics in an arbitrary system, such as HoTT. I know enough about the > formalisation process to know that whatever system one chooses, there will > be pain points, because some mathematical ideas fit more readily into some > foundational systems than others. > > >>>>>>> > > > >>>>>>> > I have seen enough of Lean to become convinced that the pain > points would be surmountable in Lean. I have seen enough of Isabelle/HOL to > become skeptical about the idea that it would be suitable for all of modern > pure mathematics, although it is clearly suitable for some of it; however > it seems that simple type theory struggles to handle things like tensor > products of sheaves of modules on a scheme, because sheaves are dependent > types and it seems that one cannot use Isabelle's typeclass system to > handle the rings showing up in a sheaf of rings. > > >>>>>>> > > > >>>>>>> > I have very little experience with HoTT. I have heard that the > fact that "all constructions must be isomorphism-invariant" is both a > blessing and a curse. However I would like to know more details. I am > speaking at the Big Proof conference in Edinburgh this coming Wednesday on > the pain points involved with formalising mathematical objects in dependent > type theory and during the preparation of my talk I began to wonder what > the analogous picture was with HoTT. > > >>>>>>> > > > >>>>>>> > Everyone will have a different interpretation of "modern pure > mathematics" so to fix our ideas, let me say that for the purposes of this > discussion, "modern pure mathematics" means the statements of the theorems > publishsed by the Annals of Mathematics over the last few years, so for > example I am talking about formalising statements of theorems involving > L-functions of abelian varieties over number fields, Hodge theory, > cohomology of algebraic varieties, Hecke algebras of symmetric groups, > Ricci flow and the like; one can see titles and more at > http://annals.math.princeton.edu/2019/189-3 . Classical logic and the > axiom of choice are absolutely essential -- I am only interested in the > hard-core "classical mathematician" stance of the way mathematics works, > and what it is. > > >>>>>>> > > > >>>>>>> > If this is not the right forum for this question, I would be > happily directed to somewhere more suitable. After spending 10 minutes > failing to get onto ##hott on freenode ("you need to be identified with > services") I decided it was easier just to ask here. If people want to chat > directly I am usually around at https://leanprover.zulipchat.com/ > (registration required, full names are usually used, I'll start a HoTT > thread in #mathematics). > > >>>>>>> > > > >>>>>>> > Kevin Buzzard > > >>>>>>> > > > >>>>>>> > -- > > >>>>>>> > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com > . > > >>>>>>> > For more options, visit https://groups.google.com/d/optout. > > >>>>>>> > > >>>>>> -- > > >>>>>> 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com > . > > >>>>>> For more options, visit https://groups.google.com/d/optout. > > >>>>> > > >>>>> -- > > >>>>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com > . > > >>>>> > > >>>>> > > >>>>> For more options, visit https://groups.google.com/d/optout. > > >>> > > >>> -- > > >>> 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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com > . > > >>> For more options, visit https://groups.google.com/d/optout. > > -- > 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/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3A%40mail.gmail.com > . > For more options, visit https://groups.google.com/d/optout. > -- 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/CAOoPQuT4kJr4cr8rqS2kMjNkQyj6rj8CxChXx82rWcapXtRDxQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 30796 bytes --]

On Thu, 30 May 2019 at 18:14, Michael Shulman <shulman@sandiego.edu> wrote: > > Thanks Martin! Of course you are right that there are people who > don't need to be convinced and who derive benefit and pleasure from > their formalization efforts, and in our community we probably > encounter a lot of them. However, I still maintain that the *average* > working mathematician is not yet going to find such work useful or > rewarding for its own sake. If you go to, say, the U.S. Joint > Mathematics Meetings and stop a hundred mathematicians at random in > the lobby and ask whether they have ever formalized their work in a > proof assistant, how many do you think will say yes? I think this is absolutely right, and an important point. We can even go further: ask 100 mathematicians whether they have ever formalised *anything at all* in a proof assistant, and only epsilon will say yes. This is why I am focussing on the undergraduates. What we as a community can offer undergraduates is a guarantee that a proof is correct; one could regard this as "instant feedback". I think it is currently very difficult to answer the question I've been asked by several staff members -- "what is in it for me"? Some people might find this a negative approach, but if computer proof systems are introduced in undergraduate curricula, and the response to the question "what is the point of teaching these people type theory?" can be something like this: "what is the point of teaching them Banach spaces? Some will use it later on, many won't. Many students graduate, leave mathematics, and never really use these high-powered objects again. For those people, a course on type theory will teach them just as much as a course on Banach spaces -- it will just give them another domain where they can reason logically, learn some easy theorems, learn some deeper results, etc. Oh, and there's evidence that one day type theory will change the world in a way that Banach spaces probably will not". This is the line I am going to take in a couple of years' time when we are discussing changes to my university's curriculum. And then in a generation's time, one can hope that more than epsilon will say yes. Mathematical culture sometimes changes very slowly. We might be using different systems but I still believe that we are looking at the future, and if the current staff can't see it then we have to work on the future staff. The problem I find with this evil plan for world domination is that most senior people I talk to (across all of these systems) tend not to be employed by maths departments. This is a different issue, which needs different ideas, but those are really orthogonal to this conversation. The thing I know for sure is that there are modern maths undergraduates who grew up with computer games and who find the idea of turning their example sheet questions into levels of a computer game quite appealing. Kevin > > Perhaps I am too pessimistic. But let me in turn offer myself as an > example: in addition to being a homotopy type theorist, I have another > hat as a classical category theorist and homotopy theorist. When I > prove things in HoTT, I often formalize them in a proof assistant. > But when I prove things in classical mathematics, I very rarely > consider formalizing them. Only once have I formalized a proof in > classical category theory; the experience was more time-consuming and > less enjoyable than I expected, and I have no plans to do it again. > And I expect that as classical mathematicians go, I am (even when I > have my classical mathematician hat on) pretty far on the > sympathetic-to-formalization side of the spectrum. > > > > On Wed, May 29, 2019 at 12:05 PM Martín Hötzel Escardó > <escardo.martin@gmail.com> wrote: > > > > Thanks for this discussion. I like it. > > > > Maybe I would like to argue with this point: > > > > On 28/05/2019 10:50, Michael Shulman wrote: > > > I think it's fairly hopeless to convince a classical mathematician > > > that they should put in a lot of work to convince a computer of the > > > truth of *something they already knew*. > > > > I am not sure why the person who started this thread, a mathematician, > > Kevin Buzzard, decided to put in such a lot of work, but did and he > > has (in Lean), with his students. > > > > But having interacted with a lot of students (from my institution, and > > from everywhere in the world, from maths, logic, computer science and > > philosophy departments (and once even a high school student in the > > UniMath School)), what I can say is that they are not trying to > > convince the computer. > > > > They are trying to convince themselves, using the computer to both > > check their understanding and record their understanding when > > the proof is complete. > > > > If I am allowed to speak for myself, I created a univalent library in > > Agda for the purpose of *doing something else*. However, it is nice to > > stare at the library and see everything developed from first > > principles. When presented with the mathematical literature, both as > > students and experienced mathematicians, we are never sure how far > > back one has to read until everything begins in a precise way. How > > much have we created, and how do all the different fields of > > mathematics interact with each other? When one records mathematics in > > the computer, this begins to become clear, or at least the asnwers to such > > questions become possible. > > > > We don't need to *convince* anybody. This will *happen*. And it is > > already happening. The students like it. This is my experience. > > > > M. > > > > > > -- > > 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/c7197bc2-7fc5-4027-bed6-24b2d350950f%40googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > -- > 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/CAOvivQxAZEXiCSS5%2BipOszo%3DJeymDXL3jyfuNFdY7AKxAZSS4g%40mail.gmail.com. > For more options, visit https://groups.google.com/d/optout. -- 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/CAH52Xb0SKwTaKtkBdZgav3KPkrqGs-eYae11v103ErYU%3D2dCRQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

On Sun, 2 Jun 2019 at 17:30, Bas Spitters <b.a.w.spitters@gmail.com> wrote: > > Dear Kevin, > > Looking at your slides from big proof, the transfer package you're asking for seems to be very close to what is provided by HoTT. > https://xenaproject.wordpress.com/2019/06/02/equality-part-3-canonical-isomorphism/ > This is explained in many places (e.g. the book). Here's an early article explaining it for algebraic structures: > http://www.cse.chalmers.se/~nad/publications/coquand-danielsson-isomorphism-is-equality.pdf > > Have you looked at any of this? Does it provide what you are looking for? There is a subtle difference. HoTT transfers theorems and definitions across all isomorphisms. In the definition of a scheme, the stacks project transfers an exact sequence along a *canonical isomorphism*. Canonical isomorphism is denoted by "=" in some literature (e.g. see some recent tweets by David Roberts like https://twitter.com/HigherGeometer/status/1133993485034332161). This is some sort of weird half-way house, not as extreme as HoTT, not as weak as DTT, but some sort of weird half-way house where mathematicians claim to operate; this is an attitude which is beginning to scare me a little. Kevin > > Best, > > Bas > > On Sun, May 26, 2019 at 7:00 PM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: >> >> I would like to again thank the people who have been responding to my >> posts this weekend with links and further reading. I know the Lean >> literature but I knew very little indeed about HoTT / UniMath at the >> start of this weekend; at least now I feel like I know where you guys >> are. >> >> On Sun, 26 May 2019 at 13:09, Bas Spitters <b.a.w.spitters@gmail.com> wrote: >> >> > It's a slow process, but I believe we are making progress. >> >> I agree that it's a slow process! I think that in any computer science >> department you can find people who know about these tools, indeed in >> the computer science department at my university there are people >> using things like Coq for program verification. I think that one >> measure of success would be when in most mathematics departments you >> can find someone who knows about this stuff. My personal experience is >> that we seem to be far from this, at this point. Bas points out the >> EU-funded project ForMath and I know that Paulson has an EU grant in >> Cambridge for Isabelle (my impression is that it is centred in the >> computer science department) and there is a Lean one based in >> Amsterdam which I know has mathematicians involved. For me the shock >> is that now I've seen what these things can do, I am kind of stunned >> that mathematicians don't know more about them. >> >> > You seem to be mixing at least two issues. >> > - HoTT/UF as a foundation >> > - Current implementations in proof assistants. >> >> Yes; when I started this thread I was very unclear about how >> everything fitted together. I asked a bit on the Lean chat but I guess >> many people are like me -- they know one system, and are not experts >> at all in what is going on with the other systems. >> >> I had forgotten about the mathcomp book! Someone pointed it out to me >> a while ago but I knew far less then about everything so it was a bit >> more intimidating. Thanks for reminding me. >> >> I think I have basically said all I had to say (and have managed to >> get my ideas un-muddled about several things). But here is a parting >> shot. Voevodsky was interested in formalising mathematics in a proof >> assistant. Before that, Voevodsky was a "traditional mathematician" >> and proved some great theorems and made some great constructions using >> mathematical objects called schemes. Theorems about schemes (his >> development of a homotopy theory for schemes) are what got him his >> Fields Medal. Schemes were clearly close to his heart. But looking at >> the things he formalised, he was doing things like the p-adic numbers, >> and lots and lots of category theory. I am surprised that he did not >> attempt to formalise the basic theory of schemes. Grothendieck's EGA >> is written in quite a "formal" way (although nowhere near as formal as >> what would be needed to formalise it easily in a proof assistant) and >> Johan de Jong's Stacks Project https://stacks.math.columbia.edu/ is >> another very solid attempt to lay down the foundations of the theory. >> I asked Johan whether he now considered his choice of "nice web pages" >> old-fashioned when it was now possible to formalise things in a proof >> assistant, and he said that he did not have time to learn how to use a >> proof assistant. But Voevodsky was surely aware of this work, and also >> how suitable it looks for formalisation. >> >> Thanks again to this community for all the comments and all the links >> and all the corrections. If anyone is going to Big Proof in Edinburgh >> this coming week I'd be happy to talk more. >> >> Kevin >> >> > >> > If you want to restrict to classical maths. Then please have a careful >> > look at how its done in mathematical components: >> > https://math-comp.github.io/mcb/ >> > and the analysis library that is currently under development. >> > https://github.com/math-comp/analysis >> > >> > If you went to help connecting this to the HoTT library, it will be >> > much appreciated. >> > https://github.com/HoTT/HoTT >> > >> > Best wishes, >> > >> > Bas >> > >> > On Sun, May 26, 2019 at 1:41 PM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: >> > > >> > > It seems to me, now I understand much better what is going on (many thanks to all the people who replied) that dependent type theory + impredicative prop "got lucky", in that Coq has been around for a long time, and Lean 3 is an attempt to model basically the same type theory but in a way more suited to mathematics, written by someone who knows what they're doing (de Moura). Using nonconstructive maths e.g. LEM or AC etc in Lean 3 is just a matter of writing some incantation at the top of a file and then not thinking about it any more. HoTT might be more appropriate for mathematics -- or at least for some kinds of mathematics -- but its implementation in an actual piece of software seems a bit more hacky at this point ("use Coq, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean documentation is not ideal for mathematicians -- mathematicians need very early on to be able to use tactics such as `ring` or `norm_num` to do calculations with real numbers or in commutative rings, and these tactics are not even mentioned in the standard Lean documentation. >> > > >> > > I am a working mathematician who two years ago knew nothing about this way of doing mathematics on a computer. Now I have seen what is possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians do not see the point of it, or what it has to offer a modern working mathematician; they can see no immediate benefits in learning how this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists are there in an average maths department? In the UK at least, the answer is "much less than 1", and I cannot see that changing any time soon. I would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least make mathematicians sit up and take notice, but when I look at what has been done in these various systems I do not see this occurring. This weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic analysis? Where is the stuff which draws mathematicians in? This by no means a criticism of unimath -- it is in fact a far more broad criticism of all of the systems out there. Lean 3 might have schemes but they still can't prove that the derivative of sin is cos, and Isabelle/HOL might never have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) when formalising the odd order theorem in Coq, but it turns out that the odd order theorem is perhaps not a good "selling point" for mathematics formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will work, but that looks to me like a complete fantasy at this point. >> > > >> > > One thing I have learnt over the last two years is that a whole bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians to sit up and take notice? I guess we simply do not know, but if there is, I hope I'm still around. >> > > >> > > Kevin >> > > >> > > >> > > >> > > On Sun, 26 May 2019 at 06:50, Bas Spitters <b.a.w.spitters@gmail.com> wrote: >> > >> >> > >> There has been progress in making a cleaner interface with the standard Coq tactics. (Some abstractions were broken at the ocaml level) >> > >> I'm hopeful that this can be lead to a clean connection between the HoTT library and more of the Coq developments in the not too distant future. >> > >> As it exists in agda now. >> > >> >> > >> IIUC, UniMath does not allow any of the standard library or it's tactics, or even record types, since Vladimir wanted to have a very tight connection between type theory and it's semantics in simplicial sets. So, I don't expect them to connect to other developments, but I could be wrong. >> > >> >> > >> About the bundled/unbundled issue, which also exists in Coq, there's some recent progress "frame type theory" which should be applicable to both Coq and lean: >> > >> http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51 >> > >> >> > >> Coming back to Kevin's question, yes, HoTT (plus classical logic for sets), seems to be the most natural foundation for mathematics as is currently published in the Annals. >> > >> >> > >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote: >> > >>> >> > >>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library." “Coq with the indices-matter option plus the HoTT library" is of the same category as "Lean plus the math library" and then it makes sense to compare how practically useful they are for math. >> > >>> >> > >>> Here it's important to note that most advanced things that you can do in Coq are broken by using the "indices-matter" option and relatedly not using the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04591 "This small change makes the whole standard library unusable, and many tactics stop working, too. The solution was rather drastic: we ripped out the standard library and replaced it with a minimal core that is sufficient for the basic tactics to work." >> > >>> >> > >>> (In particular, I was in error in my previous email, *some* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical calculations.) >> > >>> >> > >>> I should say I've never used Coq, just Agda. (When I was using Agda the situation was even worse, things like pattern matching secretly assumed k even if you used the without-k option, and HITs were put in by a hack that wasn't totally clear if it worked, etc.) So I'm likely wrong in some places above. >> > >>> >> > >>> So I think from a practical point of view, “Coq with the indices-matter option plus the HoTT library" is well behind ordinary Coq (and also Lean) for doing ordinary mathematics. However, if and when it does catch up some of the pain points involving transporting from my previous email should go away automatically. (Side comment: once you start talking about transporting stuff related to categories across equivalences of categories it's only going to get more painful in ordinary type theory, but will remain easy in HoTT approaches.) >> > >>> >> > >>> Best, >> > >>> >> > >>> Noah >> > >>> >> > >>> p.s. Installed Lean last week. Looking forward to using it next year when Scott and I are both at MSRI. >> > >>> >> > >>> On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: >> > >>>> >> > >>>> Hi Noah. Thank you for pointing out the category error. It seems to me that sometimes when I say "HoTT" I should be saying, for example, "UniMath". >> > >>>> >> > >>>> Tactics in Lean are absolutely crucial for library development. Coq has some really powerful tactics, right? UniMath can use those tactics, presumably? >> > >>>> >> > >>>> I understand that UniMath, as implemented in Coq, takes Coq and adds some "rules" of the form "you can't use this functionality" and also adds at least one new axiom (univalence). >> > >>>> >> > >>>> On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote: >> > >>>>> >> > >>>>> I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s better. >> > >>>> >> > >>>> >> > >>>> But plain Coq has such types, right? >> > >>>> >> > >>>> OK so this has all been extremely informative. There are other provers being developed which will implement some flavour of HoTT more "faithfully", and it might be easier to develop maths libraries in such provers. >> > >>>> >> > >>>>> For example, if G and H are isomorphic groups and you want to translate a theorem or construction across the isomorphism. In ordinary type theory this is going to involve annoying book-keeping which it seems like you’d have to do separately for each kind of mathematical object. >> > >>>> >> > >>>> >> > >>>> Yes. This is a pain point in Lean. It's a particularly nasty one too, as far as mathematicians are concerned, because when you tell a mathematician "well this ring R is Cohen-Macauley, and here's a ring S which is isomorphic to R, but we cannot immediately deduce in Lean that S is Cohen-Macauley" then they begin to question what kind of crazy system you are using which cannot deduce this immediately. As an interesting experiment, find your favourite mathematician, preferably one who does not know what a Cohen-Macauley ring is, and ask them whether they think it will be true that if R and S are isomorphic rings and R is Cohen-Macauley then S is too. They will be very confident that this is true, even if they do not know the definition; standard mathematical definitions are isomorphism-invariant. This is part of our code of conduct, in fact. >> > >>>> >> > >>>> However in Lean I believe that the current plan is to try and make a tactic which will resolve this issue. This has not yet been done, and as far as I can see this is a place where UniMath is a more natural fit for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points for it, which Lean manages to get over more easily. That is somehow where I'm coming from. >> > >>>> >> > >>>>> >> > >>>>> For example, say you have a theorem about bimodules over semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.” Is that step something you’d be able to deal with easily in Lean? If not, that’s somewhere that down the line HoTT might make things more practical. >> > >>>> >> > >>>> >> > >>>> This is a great example! To be honest I am slightly confused about why we are not running into this sort of thing already. As far as I can see this would be a great test case for the (still very much under development) transport tactic. Maybe we don't have enough classification theorems. I think that our hope in general is that this sort of issue can be solved with automation. >> > >>>> >> > >>>> Kevin >> > >>>> >> > >>>> >> > >>>>> >> > >>>>> But mostly I just want to say you’re making a category error in your question. HoTT is an abstract type theory, not a proof assistant. >> > >>>>> >> > >>>>> Best, >> > >>>>> >> > >>>>> Noah >> > >>>>> >> > >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote: >> > >>>>>> >> > >>>>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the "additivity axiom". Please let me know if the following formulation of the such axiom is correct: >> > >>>>>> >> > >>>>>> >> > >>>>>> >> > >>>>>> >> > >>>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: >> > >>>>>>> >> > >>>>>>> A useful example for you might be Floris van Doorn’s formalization of >> > >>>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology >> > >>>>>>> in HoTT using Lean: >> > >>>>>>> >> > >>>>>>> https://arxiv.org/abs/1808.10690 >> > >>>>>>> >> > >>>>>>> Regards, >> > >>>>>>> >> > >>>>>>> Steve >> > >>>>>>> >> > >>>>>>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> wrote: >> > >>>>>>> > >> > >>>>>>> > Hi from a Lean user. >> > >>>>>>> > >> > >>>>>>> > As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others. >> > >>>>>>> > >> > >>>>>>> > I have seen enough of Lean to become convinced that the pain points would be surmountable in Lean. I have seen enough of Isabelle/HOL to become skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings. >> > >>>>>>> > >> > >>>>>>> > I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a blessing and a curse. However I would like to know more details. I am speaking at the Big Proof conference in Edinburgh this coming Wednesday on the pain points involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT. >> > >>>>>>> > >> > >>>>>>> > Everyone will have a different interpretation of "modern pure mathematics" so to fix our ideas, let me say that for the purposes of this discussion, "modern pure mathematics" means the statements of the theorems publishsed by the Annals of Mathematics over the last few years, so for example I am talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the like; one can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is. >> > >>>>>>> > >> > >>>>>>> > If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics). >> > >>>>>>> > >> > >>>>>>> > Kevin Buzzard >> > >>>>>>> > >> > >>>>>>> > -- >> > >>>>>>> > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. >> > >>>>>>> > For more options, visit https://groups.google.com/d/optout. >> > >>>>>>> >> > >>>>>> -- >> > >>>>>> 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com. >> > >>>>>> For more options, visit https://groups.google.com/d/optout. >> > >>>>> >> > >>>>> -- >> > >>>>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com. >> > >>>>> >> > >>>>> >> > >>>>> For more options, visit https://groups.google.com/d/optout. >> > >>> >> > >>> -- >> > >>> 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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com. >> > >>> For more options, visit https://groups.google.com/d/optout. >> >> -- >> 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/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3A%40mail.gmail.com. >> For more options, visit https://groups.google.com/d/optout. -- 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/CAH52Xb0XD3F9%3DXc2eHZDAyFHQ-3e%2BHUXc7kRTp_%2BvhzBPVx-8g%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

Hi, > On 2 Jun 2019, at 18:55, Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > There is a subtle difference. HoTT transfers theorems and definitions > across all isomorphisms. In the definition of a scheme, the stacks > project transfers an exact sequence along a *canonical isomorphism*. > Canonical isomorphism is denoted by "=" in some literature (e.g. see > some recent tweets by David Roberts like > https://twitter.com/HigherGeometer/status/1133993485034332161). This > is some sort of weird half-way house, not as extreme as HoTT, not as > weak as DTT, but some sort of weird half-way house where > mathematicians claim to operate; this is an attitude which is > beginning to scare me a little. I am under the impression that all isomorphisms that are definable within DTT/HoTT/UF are canonical isomorphisms, by which I informally mean that they are definable only by means of the universal properties characterizing the objects under consideration. This is based on the well-known observation that type theories often describe the free category with a certain kind of structure. Perhaps someone for whom it is not 21:45 on a Sunday can turn this impression into a theorem or correct it. If the impression is correct, then HoTT/UF is the half-way house (whose structural safety is supported by various models of univalence) and the mathematicians who work informally mixing equality and canonical isomorphisms are more extreme (and potentially inconsistent). With best wishes, Nicola -- 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/29FFF023-0DB7-4E09-8A77-B4F1C2730203%40leeds.ac.uk. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1: Type: text/plain, Size: 3100 bytes --] This brings an old question of what is a canonical isomorphism <https://mathoverflow.net/questions/19644/what-is-the-definition-of-canonical>. To give a simple example in the realm of HoTT, consider isomorphisms between S^1 and S^1. There is a "canonical" isomorphism, the identity, but there are many others. Are they less canonical? You can transport stuff along any of them, so they are not any less canonical from this perspective. Regards, Valery Isaev вс, 2 июн. 2019 г. в 23:47, Nicola Gambino <N.Gambino@leeds.ac.uk>: > Hi, > > > On 2 Jun 2019, at 18:55, Kevin Buzzard <kevin.m.buzzard@gmail.com> > wrote: > > > > There is a subtle difference. HoTT transfers theorems and definitions > > across all isomorphisms. In the definition of a scheme, the stacks > > project transfers an exact sequence along a *canonical isomorphism*. > > Canonical isomorphism is denoted by "=" in some literature (e.g. see > > some recent tweets by David Roberts like > > https://twitter.com/HigherGeometer/status/1133993485034332161). This > > is some sort of weird half-way house, not as extreme as HoTT, not as > > weak as DTT, but some sort of weird half-way house where > > mathematicians claim to operate; this is an attitude which is > > beginning to scare me a little. > > I am under the impression that all isomorphisms that are definable within > DTT/HoTT/UF are canonical isomorphisms, by which I informally mean that > they are definable only by means of the universal properties characterizing > the objects under consideration. > > This is based on the well-known observation that type theories often > describe the free category with a certain kind of structure. > > Perhaps someone for whom it is not 21:45 on a Sunday can turn this > impression into a theorem or correct it. > > If the impression is correct, then HoTT/UF is the half-way house (whose > structural safety is supported by various models of univalence) and the > mathematicians who work informally mixing equality and canonical > isomorphisms are more extreme (and potentially inconsistent). > > With best wishes, > Nicola > > -- > 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/29FFF023-0DB7-4E09-8A77-B4F1C2730203%40leeds.ac.uk > . > For more options, visit https://groups.google.com/d/optout. > -- 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/CAA520fs2MiSPAKkdyhOnqBSdqPw%2BhYCFL-6QRNAjobP-xKTkKA%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 4504 bytes --]

I think that often when mathematicians say that an isomorphism is "canonical" they mean that they've declared transport along it to be an implicit coercion. So although you can always transport across any isomorphism, the "canonical" ones are those that don't require notation. That is, the distinction between canonical and non-canonical does not reside in the formal system, but in the superstructure of implicit arguments, coercions, and elaboration built on top of it. On Sun, Jun 2, 2019 at 10:56 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > On Sun, 2 Jun 2019 at 17:30, Bas Spitters <b.a.w.spitters@gmail.com> wrote: > > > > Dear Kevin, > > > > Looking at your slides from big proof, the transfer package you're asking for seems to be very close to what is provided by HoTT. > > https://xenaproject.wordpress.com/2019/06/02/equality-part-3-canonical-isomorphism/ > > This is explained in many places (e.g. the book). Here's an early article explaining it for algebraic structures: > > http://www.cse.chalmers.se/~nad/publications/coquand-danielsson-isomorphism-is-equality.pdf > > > > Have you looked at any of this? Does it provide what you are looking for? > > There is a subtle difference. HoTT transfers theorems and definitions > across all isomorphisms. In the definition of a scheme, the stacks > project transfers an exact sequence along a *canonical isomorphism*. > Canonical isomorphism is denoted by "=" in some literature (e.g. see > some recent tweets by David Roberts like > https://twitter.com/HigherGeometer/status/1133993485034332161). This > is some sort of weird half-way house, not as extreme as HoTT, not as > weak as DTT, but some sort of weird half-way house where > mathematicians claim to operate; this is an attitude which is > beginning to scare me a little. > > Kevin > > > > Best, > > > > Bas > > > > On Sun, May 26, 2019 at 7:00 PM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > >> > >> I would like to again thank the people who have been responding to my > >> posts this weekend with links and further reading. I know the Lean > >> literature but I knew very little indeed about HoTT / UniMath at the > >> start of this weekend; at least now I feel like I know where you guys > >> are. > >> > >> On Sun, 26 May 2019 at 13:09, Bas Spitters <b.a.w.spitters@gmail.com> wrote: > >> > >> > It's a slow process, but I believe we are making progress. > >> > >> I agree that it's a slow process! I think that in any computer science > >> department you can find people who know about these tools, indeed in > >> the computer science department at my university there are people > >> using things like Coq for program verification. I think that one > >> measure of success would be when in most mathematics departments you > >> can find someone who knows about this stuff. My personal experience is > >> that we seem to be far from this, at this point. Bas points out the > >> EU-funded project ForMath and I know that Paulson has an EU grant in > >> Cambridge for Isabelle (my impression is that it is centred in the > >> computer science department) and there is a Lean one based in > >> Amsterdam which I know has mathematicians involved. For me the shock > >> is that now I've seen what these things can do, I am kind of stunned > >> that mathematicians don't know more about them. > >> > >> > You seem to be mixing at least two issues. > >> > - HoTT/UF as a foundation > >> > - Current implementations in proof assistants. > >> > >> Yes; when I started this thread I was very unclear about how > >> everything fitted together. I asked a bit on the Lean chat but I guess > >> many people are like me -- they know one system, and are not experts > >> at all in what is going on with the other systems. > >> > >> I had forgotten about the mathcomp book! Someone pointed it out to me > >> a while ago but I knew far less then about everything so it was a bit > >> more intimidating. Thanks for reminding me. > >> > >> I think I have basically said all I had to say (and have managed to > >> get my ideas un-muddled about several things). But here is a parting > >> shot. Voevodsky was interested in formalising mathematics in a proof > >> assistant. Before that, Voevodsky was a "traditional mathematician" > >> and proved some great theorems and made some great constructions using > >> mathematical objects called schemes. Theorems about schemes (his > >> development of a homotopy theory for schemes) are what got him his > >> Fields Medal. Schemes were clearly close to his heart. But looking at > >> the things he formalised, he was doing things like the p-adic numbers, > >> and lots and lots of category theory. I am surprised that he did not > >> attempt to formalise the basic theory of schemes. Grothendieck's EGA > >> is written in quite a "formal" way (although nowhere near as formal as > >> what would be needed to formalise it easily in a proof assistant) and > >> Johan de Jong's Stacks Project https://stacks.math.columbia.edu/ is > >> another very solid attempt to lay down the foundations of the theory. > >> I asked Johan whether he now considered his choice of "nice web pages" > >> old-fashioned when it was now possible to formalise things in a proof > >> assistant, and he said that he did not have time to learn how to use a > >> proof assistant. But Voevodsky was surely aware of this work, and also > >> how suitable it looks for formalisation. > >> > >> Thanks again to this community for all the comments and all the links > >> and all the corrections. If anyone is going to Big Proof in Edinburgh > >> this coming week I'd be happy to talk more. > >> > >> Kevin > >> > >> > > >> > If you want to restrict to classical maths. Then please have a careful > >> > look at how its done in mathematical components: > >> > https://math-comp.github.io/mcb/ > >> > and the analysis library that is currently under development. > >> > https://github.com/math-comp/analysis > >> > > >> > If you went to help connecting this to the HoTT library, it will be > >> > much appreciated. > >> > https://github.com/HoTT/HoTT > >> > > >> > Best wishes, > >> > > >> > Bas > >> > > >> > On Sun, May 26, 2019 at 1:41 PM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > >> > > > >> > > It seems to me, now I understand much better what is going on (many thanks to all the people who replied) that dependent type theory + impredicative prop "got lucky", in that Coq has been around for a long time, and Lean 3 is an attempt to model basically the same type theory but in a way more suited to mathematics, written by someone who knows what they're doing (de Moura). Using nonconstructive maths e.g. LEM or AC etc in Lean 3 is just a matter of writing some incantation at the top of a file and then not thinking about it any more. HoTT might be more appropriate for mathematics -- or at least for some kinds of mathematics -- but its implementation in an actual piece of software seems a bit more hacky at this point ("use Coq, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean documentation is not ideal for mathematicians -- mathematicians need very early on to be able to use tactics such as `ring` or `norm_num` to do calculations with real numbers or in commutative rings, and these tactics are not even mentioned in the standard Lean documentation. > >> > > > >> > > I am a working mathematician who two years ago knew nothing about this way of doing mathematics on a computer. Now I have seen what is possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians do not see the point of it, or what it has to offer a modern working mathematician; they can see no immediate benefits in learning how this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists are there in an average maths department? In the UK at least, the answer is "much less than 1", and I cannot see that changing any time soon. I would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least make mathematicians sit up and take notice, but when I look at what has been done in these various systems I do not see this occurring. This weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic analysis? Where is the stuff which draws mathematicians in? This by no means a criticism of unimath -- it is in fact a far more broad criticism of all of the systems out there. Lean 3 might have schemes but they still can't prove that the derivative of sin is cos, and Isabelle/HOL might never have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) when formalising the odd order theorem in Coq, but it turns out that the odd order theorem is perhaps not a good "selling point" for mathematics formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will work, but that looks to me like a complete fantasy at this point. > >> > > > >> > > One thing I have learnt over the last two years is that a whole bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians to sit up and take notice? I guess we simply do not know, but if there is, I hope I'm still around. > >> > > > >> > > Kevin > >> > > > >> > > > >> > > > >> > > On Sun, 26 May 2019 at 06:50, Bas Spitters <b.a.w.spitters@gmail.com> wrote: > >> > >> > >> > >> There has been progress in making a cleaner interface with the standard Coq tactics. (Some abstractions were broken at the ocaml level) > >> > >> I'm hopeful that this can be lead to a clean connection between the HoTT library and more of the Coq developments in the not too distant future. > >> > >> As it exists in agda now. > >> > >> > >> > >> IIUC, UniMath does not allow any of the standard library or it's tactics, or even record types, since Vladimir wanted to have a very tight connection between type theory and it's semantics in simplicial sets. So, I don't expect them to connect to other developments, but I could be wrong. > >> > >> > >> > >> About the bundled/unbundled issue, which also exists in Coq, there's some recent progress "frame type theory" which should be applicable to both Coq and lean: > >> > >> http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51 > >> > >> > >> > >> Coming back to Kevin's question, yes, HoTT (plus classical logic for sets), seems to be the most natural foundation for mathematics as is currently published in the Annals. > >> > >> > >> > >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote: > >> > >>> > >> > >>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library." “Coq with the indices-matter option plus the HoTT library" is of the same category as "Lean plus the math library" and then it makes sense to compare how practically useful they are for math. > >> > >>> > >> > >>> Here it's important to note that most advanced things that you can do in Coq are broken by using the "indices-matter" option and relatedly not using the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04591 "This small change makes the whole standard library unusable, and many tactics stop working, too. The solution was rather drastic: we ripped out the standard library and replaced it with a minimal core that is sufficient for the basic tactics to work." > >> > >>> > >> > >>> (In particular, I was in error in my previous email, *some* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical calculations.) > >> > >>> > >> > >>> I should say I've never used Coq, just Agda. (When I was using Agda the situation was even worse, things like pattern matching secretly assumed k even if you used the without-k option, and HITs were put in by a hack that wasn't totally clear if it worked, etc.) So I'm likely wrong in some places above. > >> > >>> > >> > >>> So I think from a practical point of view, “Coq with the indices-matter option plus the HoTT library" is well behind ordinary Coq (and also Lean) for doing ordinary mathematics. However, if and when it does catch up some of the pain points involving transporting from my previous email should go away automatically. (Side comment: once you start talking about transporting stuff related to categories across equivalences of categories it's only going to get more painful in ordinary type theory, but will remain easy in HoTT approaches.) > >> > >>> > >> > >>> Best, > >> > >>> > >> > >>> Noah > >> > >>> > >> > >>> p.s. Installed Lean last week. Looking forward to using it next year when Scott and I are both at MSRI. > >> > >>> > >> > >>> On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > >> > >>>> > >> > >>>> Hi Noah. Thank you for pointing out the category error. It seems to me that sometimes when I say "HoTT" I should be saying, for example, "UniMath". > >> > >>>> > >> > >>>> Tactics in Lean are absolutely crucial for library development. Coq has some really powerful tactics, right? UniMath can use those tactics, presumably? > >> > >>>> > >> > >>>> I understand that UniMath, as implemented in Coq, takes Coq and adds some "rules" of the form "you can't use this functionality" and also adds at least one new axiom (univalence). > >> > >>>> > >> > >>>> On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote: > >> > >>>>> > >> > >>>>> I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s better. > >> > >>>> > >> > >>>> > >> > >>>> But plain Coq has such types, right? > >> > >>>> > >> > >>>> OK so this has all been extremely informative. There are other provers being developed which will implement some flavour of HoTT more "faithfully", and it might be easier to develop maths libraries in such provers. > >> > >>>> > >> > >>>>> For example, if G and H are isomorphic groups and you want to translate a theorem or construction across the isomorphism. In ordinary type theory this is going to involve annoying book-keeping which it seems like you’d have to do separately for each kind of mathematical object. > >> > >>>> > >> > >>>> > >> > >>>> Yes. This is a pain point in Lean. It's a particularly nasty one too, as far as mathematicians are concerned, because when you tell a mathematician "well this ring R is Cohen-Macauley, and here's a ring S which is isomorphic to R, but we cannot immediately deduce in Lean that S is Cohen-Macauley" then they begin to question what kind of crazy system you are using which cannot deduce this immediately. As an interesting experiment, find your favourite mathematician, preferably one who does not know what a Cohen-Macauley ring is, and ask them whether they think it will be true that if R and S are isomorphic rings and R is Cohen-Macauley then S is too. They will be very confident that this is true, even if they do not know the definition; standard mathematical definitions are isomorphism-invariant. This is part of our code of conduct, in fact. > >> > >>>> > >> > >>>> However in Lean I believe that the current plan is to try and make a tactic which will resolve this issue. This has not yet been done, and as far as I can see this is a place where UniMath is a more natural fit for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points for it, which Lean manages to get over more easily. That is somehow where I'm coming from. > >> > >>>> > >> > >>>>> > >> > >>>>> For example, say you have a theorem about bimodules over semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.” Is that step something you’d be able to deal with easily in Lean? If not, that’s somewhere that down the line HoTT might make things more practical. > >> > >>>> > >> > >>>> > >> > >>>> This is a great example! To be honest I am slightly confused about why we are not running into this sort of thing already. As far as I can see this would be a great test case for the (still very much under development) transport tactic. Maybe we don't have enough classification theorems. I think that our hope in general is that this sort of issue can be solved with automation. > >> > >>>> > >> > >>>> Kevin > >> > >>>> > >> > >>>> > >> > >>>>> > >> > >>>>> But mostly I just want to say you’re making a category error in your question. HoTT is an abstract type theory, not a proof assistant. > >> > >>>>> > >> > >>>>> Best, > >> > >>>>> > >> > >>>>> Noah > >> > >>>>> > >> > >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote: > >> > >>>>>> > >> > >>>>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the "additivity axiom". Please let me know if the following formulation of the such axiom is correct: > >> > >>>>>> > >> > >>>>>> > >> > >>>>>> > >> > >>>>>> > >> > >>>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: > >> > >>>>>>> > >> > >>>>>>> A useful example for you might be Floris van Doorn’s formalization of > >> > >>>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology > >> > >>>>>>> in HoTT using Lean: > >> > >>>>>>> > >> > >>>>>>> https://arxiv.org/abs/1808.10690 > >> > >>>>>>> > >> > >>>>>>> Regards, > >> > >>>>>>> > >> > >>>>>>> Steve > >> > >>>>>>> > >> > >>>>>>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> wrote: > >> > >>>>>>> > > >> > >>>>>>> > Hi from a Lean user. > >> > >>>>>>> > > >> > >>>>>>> > As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others. > >> > >>>>>>> > > >> > >>>>>>> > I have seen enough of Lean to become convinced that the pain points would be surmountable in Lean. I have seen enough of Isabelle/HOL to become skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings. > >> > >>>>>>> > > >> > >>>>>>> > I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a blessing and a curse. However I would like to know more details. I am speaking at the Big Proof conference in Edinburgh this coming Wednesday on the pain points involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT. > >> > >>>>>>> > > >> > >>>>>>> > Everyone will have a different interpretation of "modern pure mathematics" so to fix our ideas, let me say that for the purposes of this discussion, "modern pure mathematics" means the statements of the theorems publishsed by the Annals of Mathematics over the last few years, so for example I am talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the like; one can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is. > >> > >>>>>>> > > >> > >>>>>>> > If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics). > >> > >>>>>>> > > >> > >>>>>>> > Kevin Buzzard > >> > >>>>>>> > > >> > >>>>>>> > -- > >> > >>>>>>> > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. > >> > >>>>>>> > For more options, visit https://groups.google.com/d/optout. > >> > >>>>>>> > >> > >>>>>> -- > >> > >>>>>> 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com. > >> > >>>>>> For more options, visit https://groups.google.com/d/optout. > >> > >>>>> > >> > >>>>> -- > >> > >>>>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com. > >> > >>>>> > >> > >>>>> > >> > >>>>> For more options, visit https://groups.google.com/d/optout. > >> > >>> > >> > >>> -- > >> > >>> 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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com. > >> > >>> For more options, visit https://groups.google.com/d/optout. > >> > >> -- > >> 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/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3A%40mail.gmail.com. > >> For more options, visit https://groups.google.com/d/optout. > > -- > 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/CAH52Xb0XD3F9%3DXc2eHZDAyFHQ-3e%2BHUXc7kRTp_%2BvhzBPVx-8g%40mail.gmail.com. > For more options, visit https://groups.google.com/d/optout. -- 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/CAOvivQzFBjtA33McF1nAerfcnFRbnWLAw73-F3GPBumbVqetag%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 1025 bytes --] On Sunday, 2 June 2019 18:49:30 UTC+1, Kevin Buzzard wrote: > > The thing I know for sure is > that there are modern maths undergraduates who grew up with computer > games and who find the idea of turning their example sheet questions > into levels of a computer game quite appealing. > > I am surprised that Thorsten Altenkirch didn't manifest himself at this point. He uses to say that you can't teach old dogs new tricks. I am not sure it is the computer games (it could be, and if not they could anyway help, perhaps). I think it is their open minds. 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/209e2262-cb8a-4b31-9b6b-44a5df0185a5%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 1617 bytes --]

The Langlandsy folk (of whom I am one, I guess) sometimes use "canonical" in a completely different way :-/ Randomly googling led me to https://mathoverflow.net/questions/127691/reconciling-lusztigs-results-with-the-langlands-philosophy (and I'm sure there are other examples -- I've even used it in my own work) where "canonical" is being used to describe a bijection between two sets. This is the thing I've referred to as "mission creep". Everyone thinking about functors and natural transformations etc -- all of these thoughts come to nothing when faced with the assertion that the Langlands correspondence is "canonical". What I believe the word means in that context is "this bijection of sets satisfies a whole bunch of cool properties, and I reserve the right to add to this list of cool properties in the future". This usage of the word has bothered me for years. When Gee and I were trying to write down a precise statement of local Langlands functoriality we ran into this; different experts seemed to have slightly different lists. When we were doing calculations we ran into a property which wasn't on any of the lists we'd seen, but which we wanted to be true, and we asked about whether this property was expected to be true in general, and/or was proved in any of the cases where the local Langlands conjectures were theorems. David Vogan said that indeed it should be on the list and even sketched a proof that it was true in the case of real and complex groups for us; other experts had not seen it before. At that time it really did feel like "canonical" was the same as "magical"; the more questions you asked, the more beautiful it got. The notion was completely unformalisable. One day someone might discover some elusive Tannakian category structure on some set of automorphic representations and all of a sudden the word might acquire some formal meaning, but until then this usage of the word remains a complete mystery to me -- I guess it may as well simply be replaced with the word "mysterious" or "beautiful" or something which is clearly not meant to be definable. As for the other issue, it would be easier to discuss if there were some formalisation of the proof that the structure presheaf on the spectrum of a commutative ring was a sheaf, in one of these HoTT systems. As far as I know this has not yet been done. Part of me wants to encourage the HoTT community to try formalising this statement ("an affine scheme is a scheme", if you like) in some HoTT proof verification system. Of course I could try doing it myself in Lean HoTT but I know I'll never get round to it. There is some subtlety here, which I am still perhaps doing a poor job of explaining. It all boils down to this very sneaky use of "=" in EGA. Kevin On Tue, 4 Jun 2019 at 21:32, Michael Shulman <shulman@sandiego.edu> wrote: > > I think that often when mathematicians say that an isomorphism is > "canonical" they mean that they've declared transport along it to be > an implicit coercion. So although you can always transport across any > isomorphism, the "canonical" ones are those that don't require > notation. That is, the distinction between canonical and > non-canonical does not reside in the formal system, but in the > superstructure of implicit arguments, coercions, and elaboration built > on top of it. > > > On Sun, Jun 2, 2019 at 10:56 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > > > On Sun, 2 Jun 2019 at 17:30, Bas Spitters <b.a.w.spitters@gmail.com> wrote: > > > > > > Dear Kevin, > > > > > > Looking at your slides from big proof, the transfer package you're asking for seems to be very close to what is provided by HoTT. > > > https://xenaproject.wordpress.com/2019/06/02/equality-part-3-canonical-isomorphism/ > > > This is explained in many places (e.g. the book). Here's an early article explaining it for algebraic structures: > > > http://www.cse.chalmers.se/~nad/publications/coquand-danielsson-isomorphism-is-equality.pdf > > > > > > Have you looked at any of this? Does it provide what you are looking for? > > > > There is a subtle difference. HoTT transfers theorems and definitions > > across all isomorphisms. In the definition of a scheme, the stacks > > project transfers an exact sequence along a *canonical isomorphism*. > > Canonical isomorphism is denoted by "=" in some literature (e.g. see > > some recent tweets by David Roberts like > > https://twitter.com/HigherGeometer/status/1133993485034332161). This > > is some sort of weird half-way house, not as extreme as HoTT, not as > > weak as DTT, but some sort of weird half-way house where > > mathematicians claim to operate; this is an attitude which is > > beginning to scare me a little. > > > > Kevin > > > > > > Best, > > > > > > Bas > > > > > > On Sun, May 26, 2019 at 7:00 PM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > >> > > >> I would like to again thank the people who have been responding to my > > >> posts this weekend with links and further reading. I know the Lean > > >> literature but I knew very little indeed about HoTT / UniMath at the > > >> start of this weekend; at least now I feel like I know where you guys > > >> are. > > >> > > >> On Sun, 26 May 2019 at 13:09, Bas Spitters <b.a.w.spitters@gmail.com> wrote: > > >> > > >> > It's a slow process, but I believe we are making progress. > > >> > > >> I agree that it's a slow process! I think that in any computer science > > >> department you can find people who know about these tools, indeed in > > >> the computer science department at my university there are people > > >> using things like Coq for program verification. I think that one > > >> measure of success would be when in most mathematics departments you > > >> can find someone who knows about this stuff. My personal experience is > > >> that we seem to be far from this, at this point. Bas points out the > > >> EU-funded project ForMath and I know that Paulson has an EU grant in > > >> Cambridge for Isabelle (my impression is that it is centred in the > > >> computer science department) and there is a Lean one based in > > >> Amsterdam which I know has mathematicians involved. For me the shock > > >> is that now I've seen what these things can do, I am kind of stunned > > >> that mathematicians don't know more about them. > > >> > > >> > You seem to be mixing at least two issues. > > >> > - HoTT/UF as a foundation > > >> > - Current implementations in proof assistants. > > >> > > >> Yes; when I started this thread I was very unclear about how > > >> everything fitted together. I asked a bit on the Lean chat but I guess > > >> many people are like me -- they know one system, and are not experts > > >> at all in what is going on with the other systems. > > >> > > >> I had forgotten about the mathcomp book! Someone pointed it out to me > > >> a while ago but I knew far less then about everything so it was a bit > > >> more intimidating. Thanks for reminding me. > > >> > > >> I think I have basically said all I had to say (and have managed to > > >> get my ideas un-muddled about several things). But here is a parting > > >> shot. Voevodsky was interested in formalising mathematics in a proof > > >> assistant. Before that, Voevodsky was a "traditional mathematician" > > >> and proved some great theorems and made some great constructions using > > >> mathematical objects called schemes. Theorems about schemes (his > > >> development of a homotopy theory for schemes) are what got him his > > >> Fields Medal. Schemes were clearly close to his heart. But looking at > > >> the things he formalised, he was doing things like the p-adic numbers, > > >> and lots and lots of category theory. I am surprised that he did not > > >> attempt to formalise the basic theory of schemes. Grothendieck's EGA > > >> is written in quite a "formal" way (although nowhere near as formal as > > >> what would be needed to formalise it easily in a proof assistant) and > > >> Johan de Jong's Stacks Project https://stacks.math.columbia.edu/ is > > >> another very solid attempt to lay down the foundations of the theory. > > >> I asked Johan whether he now considered his choice of "nice web pages" > > >> old-fashioned when it was now possible to formalise things in a proof > > >> assistant, and he said that he did not have time to learn how to use a > > >> proof assistant. But Voevodsky was surely aware of this work, and also > > >> how suitable it looks for formalisation. > > >> > > >> Thanks again to this community for all the comments and all the links > > >> and all the corrections. If anyone is going to Big Proof in Edinburgh > > >> this coming week I'd be happy to talk more. > > >> > > >> Kevin > > >> > > >> > > > >> > If you want to restrict to classical maths. Then please have a careful > > >> > look at how its done in mathematical components: > > >> > https://math-comp.github.io/mcb/ > > >> > and the analysis library that is currently under development. > > >> > https://github.com/math-comp/analysis > > >> > > > >> > If you went to help connecting this to the HoTT library, it will be > > >> > much appreciated. > > >> > https://github.com/HoTT/HoTT > > >> > > > >> > Best wishes, > > >> > > > >> > Bas > > >> > > > >> > On Sun, May 26, 2019 at 1:41 PM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > >> > > > > >> > > It seems to me, now I understand much better what is going on (many thanks to all the people who replied) that dependent type theory + impredicative prop "got lucky", in that Coq has been around for a long time, and Lean 3 is an attempt to model basically the same type theory but in a way more suited to mathematics, written by someone who knows what they're doing (de Moura). Using nonconstructive maths e.g. LEM or AC etc in Lean 3 is just a matter of writing some incantation at the top of a file and then not thinking about it any more. HoTT might be more appropriate for mathematics -- or at least for some kinds of mathematics -- but its implementation in an actual piece of software seems a bit more hacky at this point ("use Coq, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean documentation is not ideal for mathematicians -- mathematicians need very early on to be able to use tactics such as `ring` or `norm_num` to do calculations with real numbers or in commutative rings, and these tactics are not even mentioned in the standard Lean documentation. > > >> > > > > >> > > I am a working mathematician who two years ago knew nothing about this way of doing mathematics on a computer. Now I have seen what is possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians do not see the point of it, or what it has to offer a modern working mathematician; they can see no immediate benefits in learning how this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists are there in an average maths department? In the UK at least, the answer is "much less than 1", and I cannot see that changing any time soon. I would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least make mathematicians sit up and take notice, but when I look at what has been done in these various systems I do not see this occurring. This weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic analysis? Where is the stuff which draws mathematicians in? This by no means a criticism of unimath -- it is in fact a far more broad criticism of all of the systems out there. Lean 3 might have schemes but they still can't prove that the derivative of sin is cos, and Isabelle/HOL might never have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) when formalising the odd order theorem in Coq, but it turns out that the odd order theorem is perhaps not a good "selling point" for mathematics formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will work, but that looks to me like a complete fantasy at this point. > > >> > > > > >> > > One thing I have learnt over the last two years is that a whole bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians to sit up and take notice? I guess we simply do not know, but if there is, I hope I'm still around. > > >> > > > > >> > > Kevin > > >> > > > > >> > > > > >> > > > > >> > > On Sun, 26 May 2019 at 06:50, Bas Spitters <b.a.w.spitters@gmail.com> wrote: > > >> > >> > > >> > >> There has been progress in making a cleaner interface with the standard Coq tactics. (Some abstractions were broken at the ocaml level) > > >> > >> I'm hopeful that this can be lead to a clean connection between the HoTT library and more of the Coq developments in the not too distant future. > > >> > >> As it exists in agda now. > > >> > >> > > >> > >> IIUC, UniMath does not allow any of the standard library or it's tactics, or even record types, since Vladimir wanted to have a very tight connection between type theory and it's semantics in simplicial sets. So, I don't expect them to connect to other developments, but I could be wrong. > > >> > >> > > >> > >> About the bundled/unbundled issue, which also exists in Coq, there's some recent progress "frame type theory" which should be applicable to both Coq and lean: > > >> > >> http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51 > > >> > >> > > >> > >> Coming back to Kevin's question, yes, HoTT (plus classical logic for sets), seems to be the most natural foundation for mathematics as is currently published in the Annals. > > >> > >> > > >> > >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote: > > >> > >>> > > >> > >>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library." “Coq with the indices-matter option plus the HoTT library" is of the same category as "Lean plus the math library" and then it makes sense to compare how practically useful they are for math. > > >> > >>> > > >> > >>> Here it's important to note that most advanced things that you can do in Coq are broken by using the "indices-matter" option and relatedly not using the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04591 "This small change makes the whole standard library unusable, and many tactics stop working, too. The solution was rather drastic: we ripped out the standard library and replaced it with a minimal core that is sufficient for the basic tactics to work." > > >> > >>> > > >> > >>> (In particular, I was in error in my previous email, *some* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical calculations.) > > >> > >>> > > >> > >>> I should say I've never used Coq, just Agda. (When I was using Agda the situation was even worse, things like pattern matching secretly assumed k even if you used the without-k option, and HITs were put in by a hack that wasn't totally clear if it worked, etc.) So I'm likely wrong in some places above. > > >> > >>> > > >> > >>> So I think from a practical point of view, “Coq with the indices-matter option plus the HoTT library" is well behind ordinary Coq (and also Lean) for doing ordinary mathematics. However, if and when it does catch up some of the pain points involving transporting from my previous email should go away automatically. (Side comment: once you start talking about transporting stuff related to categories across equivalences of categories it's only going to get more painful in ordinary type theory, but will remain easy in HoTT approaches.) > > >> > >>> > > >> > >>> Best, > > >> > >>> > > >> > >>> Noah > > >> > >>> > > >> > >>> p.s. Installed Lean last week. Looking forward to using it next year when Scott and I are both at MSRI. > > >> > >>> > > >> > >>> On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > >> > >>>> > > >> > >>>> Hi Noah. Thank you for pointing out the category error. It seems to me that sometimes when I say "HoTT" I should be saying, for example, "UniMath". > > >> > >>>> > > >> > >>>> Tactics in Lean are absolutely crucial for library development. Coq has some really powerful tactics, right? UniMath can use those tactics, presumably? > > >> > >>>> > > >> > >>>> I understand that UniMath, as implemented in Coq, takes Coq and adds some "rules" of the form "you can't use this functionality" and also adds at least one new axiom (univalence). > > >> > >>>> > > >> > >>>> On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote: > > >> > >>>>> > > >> > >>>>> I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s better. > > >> > >>>> > > >> > >>>> > > >> > >>>> But plain Coq has such types, right? > > >> > >>>> > > >> > >>>> OK so this has all been extremely informative. There are other provers being developed which will implement some flavour of HoTT more "faithfully", and it might be easier to develop maths libraries in such provers. > > >> > >>>> > > >> > >>>>> For example, if G and H are isomorphic groups and you want to translate a theorem or construction across the isomorphism. In ordinary type theory this is going to involve annoying book-keeping which it seems like you’d have to do separately for each kind of mathematical object. > > >> > >>>> > > >> > >>>> > > >> > >>>> Yes. This is a pain point in Lean. It's a particularly nasty one too, as far as mathematicians are concerned, because when you tell a mathematician "well this ring R is Cohen-Macauley, and here's a ring S which is isomorphic to R, but we cannot immediately deduce in Lean that S is Cohen-Macauley" then they begin to question what kind of crazy system you are using which cannot deduce this immediately. As an interesting experiment, find your favourite mathematician, preferably one who does not know what a Cohen-Macauley ring is, and ask them whether they think it will be true that if R and S are isomorphic rings and R is Cohen-Macauley then S is too. They will be very confident that this is true, even if they do not know the definition; standard mathematical definitions are isomorphism-invariant. This is part of our code of conduct, in fact. > > >> > >>>> > > >> > >>>> However in Lean I believe that the current plan is to try and make a tactic which will resolve this issue. This has not yet been done, and as far as I can see this is a place where UniMath is a more natural fit for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points for it, which Lean manages to get over more easily. That is somehow where I'm coming from. > > >> > >>>> > > >> > >>>>> > > >> > >>>>> For example, say you have a theorem about bimodules over semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.” Is that step something you’d be able to deal with easily in Lean? If not, that’s somewhere that down the line HoTT might make things more practical. > > >> > >>>> > > >> > >>>> > > >> > >>>> This is a great example! To be honest I am slightly confused about why we are not running into this sort of thing already. As far as I can see this would be a great test case for the (still very much under development) transport tactic. Maybe we don't have enough classification theorems. I think that our hope in general is that this sort of issue can be solved with automation. > > >> > >>>> > > >> > >>>> Kevin > > >> > >>>> > > >> > >>>> > > >> > >>>>> > > >> > >>>>> But mostly I just want to say you’re making a category error in your question. HoTT is an abstract type theory, not a proof assistant. > > >> > >>>>> > > >> > >>>>> Best, > > >> > >>>>> > > >> > >>>>> Noah > > >> > >>>>> > > >> > >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote: > > >> > >>>>>> > > >> > >>>>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the "additivity axiom". Please let me know if the following formulation of the such axiom is correct: > > >> > >>>>>> > > >> > >>>>>> > > >> > >>>>>> > > >> > >>>>>> > > >> > >>>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: > > >> > >>>>>>> > > >> > >>>>>>> A useful example for you might be Floris van Doorn’s formalization of > > >> > >>>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology > > >> > >>>>>>> in HoTT using Lean: > > >> > >>>>>>> > > >> > >>>>>>> https://arxiv.org/abs/1808.10690 > > >> > >>>>>>> > > >> > >>>>>>> Regards, > > >> > >>>>>>> > > >> > >>>>>>> Steve > > >> > >>>>>>> > > >> > >>>>>>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> wrote: > > >> > >>>>>>> > > > >> > >>>>>>> > Hi from a Lean user. > > >> > >>>>>>> > > > >> > >>>>>>> > As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others. > > >> > >>>>>>> > > > >> > >>>>>>> > I have seen enough of Lean to become convinced that the pain points would be surmountable in Lean. I have seen enough of Isabelle/HOL to become skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings. > > >> > >>>>>>> > > > >> > >>>>>>> > I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a blessing and a curse. However I would like to know more details. I am speaking at the Big Proof conference in Edinburgh this coming Wednesday on the pain points involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT. > > >> > >>>>>>> > > > >> > >>>>>>> > Everyone will have a different interpretation of "modern pure mathematics" so to fix our ideas, let me say that for the purposes of this discussion, "modern pure mathematics" means the statements of the theorems publishsed by the Annals of Mathematics over the last few years, so for example I am talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the like; one can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is. > > >> > >>>>>>> > > > >> > >>>>>>> > If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics). > > >> > >>>>>>> > > > >> > >>>>>>> > Kevin Buzzard > > >> > >>>>>>> > > > >> > >>>>>>> > -- > > >> > >>>>>>> > 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. > > >> > >>>>>>> > For more options, visit https://groups.google.com/d/optout. > > >> > >>>>>>> > > >> > >>>>>> -- > > >> > >>>>>> 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com. > > >> > >>>>>> For more options, visit https://groups.google.com/d/optout. > > >> > >>>>> > > >> > >>>>> -- > > >> > >>>>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com. > > >> > >>>>> > > >> > >>>>> > > >> > >>>>> For more options, visit https://groups.google.com/d/optout. > > >> > >>> > > >> > >>> -- > > >> > >>> 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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com. > > >> > >>> For more options, visit https://groups.google.com/d/optout. > > >> > > >> -- > > >> 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/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3A%40mail.gmail.com. > > >> For more options, visit https://groups.google.com/d/optout. > > > > -- > > 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/CAH52Xb0XD3F9%3DXc2eHZDAyFHQ-3e%2BHUXc7kRTp_%2BvhzBPVx-8g%40mail.gmail.com. > > For more options, visit https://groups.google.com/d/optout. -- 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/CAH52Xb0v2jbutOG7bfgroYn%2B3HdD_rWtz9BC505fH1NdpnLzrQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1: Type: text/plain, Size: 2975 bytes --] Sees my name was mentioned (says the devil). Computer games are the perfect analogy. You are fighting a proof and once you have done it you reach the next level. But then there is still the boss lemma to be defeated. When I started using Type Theory using Randy Pollack’s LEGO system ages ago, I was playing nethack at the same time. The similarity of the two activities was intriguing (also both were entirely ASCII based). Also you can still to formal proofs when tired and or drunk. But you can’t do paper maths. Thorsten From: <homotopytypetheory@googlegroups.com> on behalf of Martín Hötzel Escardó <escardo.martin@gmail.com> Date: Tuesday, 4 June 2019 at 21:51 To: Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: Re: [HoTT] doing "all of pure mathematics" in type theory On Sunday, 2 June 2019 18:49:30 UTC+1, Kevin Buzzard wrote: The thing I know for sure is that there are modern maths undergraduates who grew up with computer games and who find the idea of turning their example sheet questions into levels of a computer game quite appealing. I am surprised that Thorsten Altenkirch didn't manifest himself at this point. He uses to say that you can't teach old dogs new tricks. I am not sure it is the computer games (it could be, and if not they could anyway help, perhaps). I think it is their open minds. 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/209e2262-cb8a-4b31-9b6b-44a5df0185a5%40googlegroups.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/209e2262-cb8a-4b31-9b6b-44a5df0185a5%40googlegroups.com?utm_medium=email&utm_source=footer>. For more options, visit https://groups.google.com/d/optout. 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/38C01A88-302F-4DA0-91CB-8411B4F595A0%40nottingham.ac.uk. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 6738 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1812 bytes --] I don't think implicit coercions fully handle the problem Kevin's talking about with the way "canonical isomorphisms" are used. It sounds like canonical isomorphisms are supposed to have a ton of coherences which are "obvious", so you can treat canonically isomorphic structures as if they are strictly equal. With implicit coercions, (in e.g. Coq) the transport isn't written, but it can still mess things up if you don't have the coherences you expected. And even if you do have the coherences you need, implicit coercions does not arrange to apply them automatically. I'm reminded of Guillaume's thought from his HoTTEST talk, to have some kind of proof automation that makes it look as if a path is a judgmental equality, by automatically using the necessary coherences. On Tuesday, June 4, 2019 at 4:32:31 PM UTC-4, Michael Shulman wrote: > > I think that often when mathematicians say that an isomorphism is > "canonical" they mean that they've declared transport along it to be > an implicit coercion. So although you can always transport across any > isomorphism, the "canonical" ones are those that don't require > notation. That is, the distinction between canonical and > non-canonical does not reside in the formal system, but in the > superstructure of implicit arguments, coercions, and elaboration built > on top of it. > > -- 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/1b8a8efe-ac71-44e1-9131-96dc2c445768%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 2389 bytes --]