From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-yb1-xb3c.google.com (mail-yb1-xb3c.google.com [IPv6:2607:f8b0:4864:20::b3c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c1cdcab2 for ; Sun, 2 Jun 2019 16:30:16 +0000 (UTC) Received: by mail-yb1-xb3c.google.com with SMTP id l3sf6934740ybm.18 for ; Sun, 02 Jun 2019 09:30:16 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1559493015; cv=pass; d=google.com; s=arc-20160816; b=WxlXEYbiH1utb8knSgJWcjF+FLSxT2629PNch/FbP97HSTfXJIQIaI5PqCXULJIaMi V4ESGIg8xGW9nf6AKYgFvvwhNJDZZwG9ePKT0NbjLYUeLtPv0gJvWl3XQw+fK5aIohSI 22vmkwn69xkaQq+XG/sF8ffYreF0rd9tHiD1BU4l8Y2BYmRQb0HuidrhM8a4FOUXDSzQ 5RqKg4D6gJfoYKcl3/iAB/A7crcpVowIG8/CeKEDceW+FBuXUUJdhq3DoVKXiwHQNW/g 5fdnywaoiVqhTL3h0cIhHMsjOoMGA9rWIrn6luW0qBzHZKVRiC2wK0MDEOC6G5wSI3GH wePA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=kYETy/90OT2X3ApyvMy3bigYMA6mtqT0Jk6wPhgHRJo=; b=YqI5kRPdAYBE9uHXGYFphWSVpS/wH3VIVIESVBVe4rfzYVZ2Qkm8vz3SJaqBYSbzWA oSapFslqhqrAiq2lHMaSNFij/+yIEq2V/z6e4fkSiLzPYh+PpYdCwTC6kbi1CP+7gewk xuuqlPPSBgZu2IF3dIQ08dZ0Wp2mO8OVVq1sJq+bP9YfDqCzZ13smG6S4SqmRMP9AoIi Uh2YRBqUm26gavwCHPKIGMx0N2jcyqpHfKla8xT4EaM4rjm92JFerNPMz8rgBbRMlfBs mcigq8XJbJkYhaUv4bIiI1BtZsXfPZuF88aFrizM+lXcwByL1Hsx/ApbiZQHxbX2KgHs aYkA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RRM2btJP; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=kYETy/90OT2X3ApyvMy3bigYMA6mtqT0Jk6wPhgHRJo=; b=QhByUp08e9J11AgpN8E7zAQ73YuFLISoHiGjDdIO69jqMMBzVJk3mEV4t30wL7P0zb 75q8ofMjZKjTRbGyHSmbEEZTJTw3gV4RiNxIso9xFEiFrpHUaSaQpj03BkX7WK8IbdT3 MqhzH1ILWsk6Q/3Z4tctsLO3GeJlEwsyW4ycJYjwyf3DxcKFYjGzqB78okcBsBeRnc11 mPmroJ6i3ID1N1QsUMnkZfFHPYr3Y964ynaJ92tTNC8QiX4GSH+gl3GR/gWqYX9ZQ9pf NOcLu3/ACpsiA4YCi0ilml8KyJ+xh3gW4AfJcRCcE6BQEF2/DWm9AvQTDL6lVLnmf5op Mo9Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=kYETy/90OT2X3ApyvMy3bigYMA6mtqT0Jk6wPhgHRJo=; b=sfrCby8OmixEPLrChm7m1Mc9GErxTpu3dMf3SQlFTKuOjluykq49Nnf7Nr4JrADbqx QnRGjvne335wBmlhh2a/wgxHOFl2OTfYS7O7u0TfF2WW59jl+XiBDNBxTVLHx8YL/E4j PKUc5IHcCn0In8rsXjjbwGFPFxjBZdN39rRh8emF9jQUNqyuO5FtT1BkDG4YJuxF45+b tiJTCeo3RlMFZzkUD9W9XXaEXGW8AEAxiLWKfKVkL9BeIvp7SYthSt2oX5eIEW1LRzTo uMR6LtEgIrSKBCfv8bHihiLYvSpcYs8/DRUBKWjP4i6JH4GfpCo7onOtZLiTy6mnz49v jRLQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=kYETy/90OT2X3ApyvMy3bigYMA6mtqT0Jk6wPhgHRJo=; b=U/kpwDKDQ2Rery5Hy/1ExtEahdHd6oKE2OcFFhOW+3kU5ukWAPo5P31PhF7NcOA8G4 I7rdQP/ftVo7Bl9YYehXBh8KdAcspcjGzD76/TylAKYNdKyqbhfPWPv8HPmfGCSpBtvH z5HL+8Knd7kR0y7BD747WV7CWr49zHj0q9bDCfiZQ2B5GxdHSY5QDFOUQSpiYStJfXxq 2eEHJ6Pern8/M5PHu4mtvo559dTOLVFY+hPjk8iTAAwKfTneW/DdvQ0hJioY3wqTlyTD bxNYNWi4KtQyIBcbc+DfHDe3IIyaMJm1CwOwz4mYKmQl1oaJY7xcot51i4K4E0zSXRwK jKPQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWgmkX41f9e7GhXMIW+ZqnEan7szpoUMcHto8R9qgFdpGpowru7 h70ec6uqhVxMovJMPB4Wxqo= X-Google-Smtp-Source: APXvYqxqnkX+yhsRyvdm3dwY85yUk2MywcHvw0Zhs6hbUTxuEk2Cia+/wj3ieqE8z7s1U4Sqz5sEww== X-Received: by 2002:a81:6bd5:: with SMTP id g204mr11708271ywc.217.1559493014767; Sun, 02 Jun 2019 09:30:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:98c6:: with SMTP id p189ls1680659ywg.7.gmail; Sun, 02 Jun 2019 09:30:14 -0700 (PDT) X-Received: by 2002:a81:2e46:: with SMTP id u67mr7307351ywu.179.1559493014172; Sun, 02 Jun 2019 09:30:14 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1559493014; cv=none; d=google.com; s=arc-20160816; b=Sg1rQsnpoRNJfCVd1KjPnSBojDyTHRPUQwk/f3G7xhi0jWBfBkJ/KmFCNd+Ro3AlOO iGGp4cmov3jSzJg6uTAlH292AMUQl0vShp8dScJcHYvGgvcZ48esT/muAnrMUmpzKobU ZD5ArFGU6udAAt9WBcUlQEQ7EZ1nEh2VRFAPjpTtpgu7JUGTUl+Uat2Ap4OXD0BwLJej IcTLFuE9dRm3lf/R/5EIPVMqYFUBlO2XC9Sg1vRLYR2EiPSGe8eHi3nBdb6CyVreKtSx SCHqKS386Nvi94fbvPInBrKK3N7V6yJUAVkyv10AjoEfcY2l8W9hQw5xbJwje9eUsnzq YtJA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=aBRDvlF6orpXx+ej3xj0UNyCqlUkUrv8fur32YCGfx8=; b=sZ8c6F26lxvBTJcBtf8b9i4ZX4vQtYE9xRNBZ1vrS4wc91KtVQ6Bd4MqoJQckdXzUg 9T8PIvexcyM9ZQleKFGshXz1YiQqUnUTlyf2SpJmJuiDa24uqIS9c/YINvoFOWcl7Ek/ 6azaSguWztH3GhR+6BqSmo/v6cvlQtFv3fPWmC+gw+hPxH0OEb2N75S++l90Cswm7g7L rm+yNFBQlKnjhA12UPp3luS6/Idd4oXnBh81+j7zIC6LXXxf5hB+q98B7iSZocyo9S+1 yTXGBRxJpLz0c4UhbrWQ+vP9ahVErziXG7hXDyxKuqh3pY9W2RxvHTGXTCc2OeyrPK5s /t6Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RRM2btJP; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yb1-xb2a.google.com (mail-yb1-xb2a.google.com. [2607:f8b0:4864:20::b2a]) by gmr-mx.google.com with ESMTPS id 66si363069ybe.5.2019.06.02.09.30.14 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Sun, 02 Jun 2019 09:30:14 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2a as permitted sender) client-ip=2607:f8b0:4864:20::b2a; Received: by mail-yb1-xb2a.google.com with SMTP id c7so4177611ybs.9 for ; Sun, 02 Jun 2019 09:30:14 -0700 (PDT) X-Received: by 2002:a25:7488:: with SMTP id p130mr10918854ybc.186.1559493013686; Sun, 02 Jun 2019 09:30:13 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> In-Reply-To: From: Bas Spitters Date: Sun, 2 Jun 2019 18:30:00 +0200 Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Kevin Buzzard Cc: Noah Snyder , Homotopy Type Theory , Juan Ospina Content-Type: multipart/alternative; boundary="0000000000001c4fa3058a59c30b" X-Original-Sender: b.a.w.spitters@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RRM2btJP; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --0000000000001c4fa3058a59c30b Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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-isom= orphism/ 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 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 > 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 > 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 bu= t > 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 f= or > 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 speaki= ng > 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 thi= s > 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 man= y > 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 a= ny > 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 a= m > wondering whether developing accessible databases of undergraduate level > mathematics would at least make mathematicians sit up and take notice, bu= t > 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 stuf= f > 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 Gonthi= er > 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 kn= ow > what is. I'm now wondering making formalised undergraduate mathematics mo= re > accessible to untrained mathematicians is a better approach, but who know= s. > 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 -- wi= ll > 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 > 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 futu= re. > > >> 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 bo= th > 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 > wrote: > > >>> > > >>> UniMath vs HoTT wasn=E2=80=99t exactly my point, UniMath =3D Book-H= oTT is of a > category from =E2=80=9CCoq with the indices-matter option plus the HoTT l= ibrary." > =E2=80=9CCoq 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 compa= re > 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 n= ot > 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 advanc= ed > 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 Agd= a > the situation was even worse, things like pattern matching secretly assum= ed > 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 som= e > places above. > > >>> > > >>> So I think from a practical point of view, =E2=80=9CCoq 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 sta= rt > talking about transporting stuff related to categories across equivalence= s > 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 t= o > me that sometimes when I say "HoTT" I should be saying, for example, > "UniMath". > > >>>> > > >>>> Tactics in Lean are absolutely crucial for library development. Co= q > 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 > wrote: > > >>>>> > > >>>>> I=E2=80=99d also imagine that a =E2=80=9Cpractical=E2=80=9D imple= mentation would likely > have some kind of =E2=80=9Ctwo-level=E2=80=9D type theory where you can u= se types that > behave classically when that=E2=80=99s better and HoTT types when that=E2= =80=99s 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=E2=80=99d have to do separately for each kind of mathematical ob= ject. > > >>>> > > >>>> > > >>>> 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 no= t > know what a Cohen-Macauley ring is, and ask them whether they think it wi= ll > 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 no= t > 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 a= s > 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 pai= n > points for it, which Lean manages to get over more easily. That is someho= w > where I'm coming from. > > >>>> > > >>>>> > > >>>>> For example, say you have a theorem about bimodules over > semisimple rings whose proof starts =E2=80=9Cwlog, by Artin-Wedderburn, w= e can > assume both algebras are multimatrix algebras over division rings.=E2=80= =9D Is > that step something you=E2=80=99d be able to deal with easily in Lean? I= f not, > that=E2=80=99s somewhere that down the line HoTT might make things more p= ractical. > > >>>> > > >>>> > > >>>> 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 s= ee > this would be a great test case for the (still very much under developmen= t) > 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=E2=80=99re making a category er= ror 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 > 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 t= he > 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=E2=80=99s > formalization of > > >>>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomolo= gy > > >>>>>>> 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 general= ly > 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 wil= l > be pain points, because some mathematical ideas fit more readily into som= e > 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 mode= rn > 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 th= e > 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 o= n > the pain points involved with formalising mathematical objects in depende= nt > 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 thi= s > discussion, "modern pure mathematics" means the statements of the theorem= s > 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 ch= at > 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-a= 3b7-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-b= 42b-b9a9f639d89e%40googlegroups.com > . > > >>>>>> For more options, visit https://groups.google.com/d/optout. > > >>>>> > > >>>>> -- > > >>>>> You received this message because you are subscribed to the Googl= e > 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/CAO0tDg4dyjZHueTPQEY= KQaojSw6SDKNUC8y49JHMoR9oTQOmMw%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%2BoXRL= hsN3O7uXCh3D%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. > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAOoPQuT4kJr4cr8rqS2kMjNkQyj6rj8CxChXx82rWcapXtRDxQ%40ma= il.gmail.com. For more options, visit https://groups.google.com/d/optout. --0000000000001c4fa3058a59c30b Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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.
This is explained in many places (e.g. the book).= Here's an early article explaining it for algebraic structures:
<= div>http://www.cse.chalmers.se/~nad/publicatio= ns/coquand-danielsson-isomorphism-is-equality.pdf

<= div>Have you looked at any of this? Does it provide what you are looking fo= r?

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 t= he 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<= br> 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&quo= t;
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 form= al 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&= quot;
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 (ma= ny thanks to all the people who replied) that dependent type theory + impre= dicative 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 the= y're doing (de Moura). Using nonconstructive maths e.g. LEM or AC etc i= n 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 implem= entation in an actual piece of software seems a bit more hacky at this poin= t ("use Coq, but don't use these commands or these tactics"),= which maybe raises the entry barrier for mathematicians a bit (and speakin= g 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 mathematici= ans -- 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 docum= entation.
> >
> > 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 possi= ble I am becoming convinced that it can really change mathematics. In my ex= perience 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 theor= ists are there in an average maths department? In the UK at least, the answ= er is "much less than 1", and I cannot see that changing any time= soon. I would love to draw the mathematics and computer science communitie= s closer together over ideas like this, but it's hard work. I am wonder= ing whether developing accessible databases of undergraduate level mathemat= ics would at least make mathematicians sit up and take notice, but when I l= ook at what has been done in these various systems I do not see this occurr= ing. This weekend I've learnt something about UniMath, but whilst it mi= ght do bicategories very well (which are not on our undergraduate curriculu= m), where is the basic analysis? Where is the stuff which draws mathematici= ans 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 Isab= elle/HOL might never have schemes. I know that Gonthier and his coauthors h= ad to make a lot of undergraduate level maths (Galois theory, algebraic num= ber theory, group theory) when formalising the odd order theorem in Coq, bu= t it turns out that the odd order theorem is perhaps not a good "selli= ng point" for mathematics formalisation when you're trying to sell= to "normal research mathematicians", and I don't know what i= s. I'm now wondering making formalised undergraduate mathematics more a= ccessible 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 b= unch 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 beginni= ng to notice. Of course there are exceptions. One day though -- will there = simply be a gigantic wave which crashes through mathematics and forces math= ematicians 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 th= e standard Coq tactics. (Some abstractions were broken at the ocaml level)<= br> > >> I'm hopeful that this can be lead to a clean connection b= etween the HoTT library and more of the Coq developments in the not too dis= tant future.
> >> As it exists in agda now.
> >>
> >> IIUC, UniMath does not allow any of the standard library or i= t'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 c= ould 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:
> >>=C2=A0 http://www.ii.uib.no/~b= ezem/abstracts/TYPES_2019_paper_51
> >>
> >> Coming back to Kevin's question, yes, HoTT (plus classica= l 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:<= br> > >>>
> >>> UniMath vs HoTT wasn=E2=80=99t exactly my point, UniMath = =3D Book-HoTT is of a category from =E2=80=9CCoq with the indices-matter op= tion plus the HoTT library."=C2=A0 =C2=A0=E2=80=9CCoq 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 pr= actically 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.=C2=A0 Quoting from <= a href=3D"https://arxiv.org/abs/1610.04591" rel=3D"noreferrer" target=3D"_b= lank">https://arxiv.org/abs/1610.04591 "This small change makes th= e whole standard library unusable, and many tactics stop working, too.=C2= =A0 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 t= o work."
> >>>
> >>> (In particular, I was in error in my previous email, *som= e* tactics are available in Coq+indices-matter+HoTT, but not many of the mo= re advanced ones, and to my knowledge, not tactics needed for complicated h= omotopical calculations.)
> >>>
> >>> I should say I've never used Coq, just Agda.=C2=A0 (W= hen I was using Agda the situation was even worse, things like pattern matc= hing secretly assumed k even if you used the without-k option, and HITs wer= e put in by a hack that wasn't totally clear if it worked, etc.)=C2=A0 = So I'm likely wrong in some places above.
> >>>
> >>> So I think from a practical point of view, =E2=80=9CCoq w= ith the indices-matter option plus the HoTT library" is well behind or= dinary Coq (and also Lean) for doing ordinary mathematics.=C2=A0 However, i= f and when it does catch up some of the pain points involving transporting = from my previous email should go away automatically.=C2=A0 (Side comment: o= nce you start talking about transporting stuff related to categories across= equivalences of categories it's only going to get more painful in ordi= nary type theory, but will remain easy in HoTT approaches.)
> >>>
> >>> Best,
> >>>
> >>> Noah
> >>>
> >>> p.s. Installed Lean last week.=C2=A0 Looking forward to u= sing 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@gm= ail.com> wrote:
> >>>>
> >>>> Hi Noah. Thank you for pointing out the category erro= r. It seems to me that sometimes when I say "HoTT" I should be sa= ying, for example, "UniMath".
> >>>>
> >>>> Tactics in Lean are absolutely crucial for library de= velopment. Coq has some really powerful tactics, right? UniMath can use tho= se tactics, presumably?
> >>>>
> >>>> I understand that UniMath, as implemented in Coq, tak= es 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> w= rote:
> >>>>>
> >>>>> I=E2=80=99d also imagine that a =E2=80=9Cpractica= l=E2=80=9D implementation would likely have some kind of =E2=80=9Ctwo-level= =E2=80=9D type theory where you can use types that behave classically when = that=E2=80=99s better and HoTT types when that=E2=80=99s 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 libra= ries in such provers.
> >>>>
> >>>>> For example, if G and H are isomorphic groups and= you want to translate a theorem or construction across the isomorphism.=C2= =A0 In ordinary type theory this is going to involve annoying book-keeping = which it seems like you=E2=80=99d have to do separately for each kind of ma= thematical object.
> >>>>
> >>>>
> >>>> Yes. This is a pain point in Lean. It's a particu= larly nasty one too, as far as mathematicians are concerned, because when y= ou tell a mathematician "well this ring R is Cohen-Macauley, and here&= #39;s a ring S which is isomorphic to R, but we cannot immediately deduce i= n 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 w= ho does not know what a Cohen-Macauley ring is, and ask them whether they t= hink it will be true that if R and S are isomorphic rings and R is Cohen-Ma= cauley then S is too. They will be very confident that this is true, even i= f they do not know the definition; standard mathematical definitions are is= omorphism-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 natu= ral fit for "the way mathematicians think". However now I've = looked over what has currently been formalised in UniMath I am wondering wh= ether there are pain points for it, which Lean manages to get over more eas= ily. That is somehow where I'm coming from.
> >>>>
> >>>>>
> >>>>>=C2=A0 For example, say you have a theorem about b= imodules over semisimple rings whose proof starts =E2=80=9Cwlog, by Artin-W= edderburn, we can assume both algebras are multimatrix algebras over divisi= on rings.=E2=80=9D=C2=A0 Is that step something you=E2=80=99d be able to de= al with easily in Lean?=C2=A0 If not, that=E2=80=99s somewhere that down th= e line HoTT might make things more practical.
> >>>>
> >>>>
> >>>> This is a great example! To be honest I am slightly c= onfused about why we are not running into this sort of thing already. As fa= r as I can see this would be a great test case for the (still very much und= er development) transport tactic. Maybe we don't have enough classifica= tion 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=E2=80=99re maki= ng a category error in your question.=C2=A0 HoTT is an abstract type theory= , not a proof assistant.
> >>>>>
> >>>>> Best,
> >>>>>
> >>>>> Noah
> >>>>>
> >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <<= a href=3D"mailto:jospina65@gmail.com" target=3D"_blank">jospina65@gmail.com= > wrote:
> >>>>>>
> >>>>>> On page 117 of https://arxiv.org/p= df/1808.10690.pdf appears the "additivity axiom".=C2=A0 Pleas= e 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=E2=80=99s formalization of
> >>>>>>> the Atiyah-Hirzebruch and Serre spectral = sequences for cohomology
> >>>>>>> in HoTT using Lean:
> >>>>>>>
> >>>>>>>=C2=A0 https://arxiv.org/abs/1808.1= 0690
> >>>>>>>
> >>>>>>> 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 H= ales' formal abstracts project https://formalabstracts.github.= io/ wants to formalise many of the statements of modern pure mathematic= s 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 whateve= r 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 suitabl= e for some of it; however it seems that simple type theory struggles to han= dle 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 H= oTT. I have heard that the fact that "all constructions must be isomor= phism-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 Edinburg= h this coming Wednesday on the pain points involved with formalising mathem= atical objects in dependent type theory and during the preparation of my ta= lk I began to wonder what the analogous picture was with HoTT.
> >>>>>>> >
> >>>>>>> > Everyone will have a different inter= pretation of "modern pure mathematics" so to fix our ideas, let m= e say that for the purposes of this discussion, "modern pure mathemati= cs" means the statements of the theorems publishsed by the Annals of M= athematics over the last few years, so for example I am talking about forma= lising statements of theorems involving L-functions of abelian varieties ov= er number fields, Hodge theory, cohomology of algebraic varieties, Hecke al= gebras 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 t= his 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 usua= lly used, I'll start a HoTT thread in #mathematics).
> >>>>>>> >
> >>>>>>> > Kevin Buzzard
> >>>>>>> >
> >>>>>>> > --
> >>>>>>> > You received this message because yo= u are subscribed to the Google Groups "Homotopy Type Theory" grou= p.
> >>>>>>> > To unsubscribe from this group and s= top receiving emails from it, send an email to HomotopyTypeTheo= ry+unsubscribe@googlegroups.com.
> >>>>>>> > To view this discussion on the web v= isit https://groups.google.com/d/msgid/HomotopyTypeTheory/a57315f6-= cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com.
> >>>>>>> > For more options, visit htt= ps://groups.google.com/d/optout.
> >>>>>>>
> >>>>>> --
> >>>>>> You received this message because you are sub= scribed to the Google Groups "Homotopy Type Theory" group.
> >>>>>> To unsubscribe from this group and stop recei= ving emails from it, send an email to HomotopyTypeTheory+unsubs= cribe@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://grou= ps.google.com/d/optout.
> >>>>>
> >>>>> --
> >>>>> You received this message because you are subscri= bed to the Google Groups "Homotopy Type Theory" group.
> >>>>> To unsubscribe from this group and stop receiving= emails from it, send an email to HomotopyTypeTheory+unsubscrib= e@googlegroups.com.
> >>>>>
> >>>>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4= dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com.
> >>>>>
> >>>>>
> >>>>> For more options, visit https://groups.g= oogle.com/d/optout.
> >>>
> >>> --
> >>> You received this message because you are subscribed to t= he Google Groups "Homotopy Type Theory" group.
> >>> To unsubscribe from this group and stop receiving emails = from it, send an email to HomotopyTypeTheory+unsubscribe@google= groups.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.co= m/d/optout.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuT4kJr4cr8rqS2kMjNkQyj6rj8C= xChXx82rWcapXtRDxQ%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--0000000000001c4fa3058a59c30b--