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-wr1-x43f.google.com (mail-wr1-x43f.google.com [IPv6:2a00:1450:4864:20::43f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 144d435c for ; Sun, 26 May 2019 11:41:36 +0000 (UTC) Received: by mail-wr1-x43f.google.com with SMTP id e14sf7340462wrx.7 for ; Sun, 26 May 2019 04:41:36 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558870895; cv=pass; d=google.com; s=arc-20160816; b=j/B6q+1Id79Ls3Q141+pnC/PYVrs4wxUGhs1OGL9/3TuqR4Y57fiYIpIePqUIsGNW8 j1brFc/9wly6u5ZR26wd0401IMgalZ2k8ghzydvEBLAPygjF4gCXs8vs+ZOX4Ai6nh0F B+yHz4s5OEGRS0SCdbZdRW2NhbdzOjMlNoJL2ILNtKNlHpT9g+gE80slc91JAzMtXH+v 2aD0ZK+icWLeBDZp+nvK9qRlI8pylESfBZyPOpgANUOuNLsVkILM5KmE8t+1eJgPp7uJ 90VvPWr5b9BhVLqsopN8zO9vBkeH0mmksoJhKtAJ2rD1cHHvKJZiLdsh/qMWXUYkYLqs MjMw== 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=SO7ivnsmpBjq8uOAVVW3THCLw76hL4yvohFyhmdBnY0=; b=fkqAHxOMUNOSGykT0qbL5D1UAsNhMcM7Z+lzw6GgbuNtOXNNK3dwAD2WpnGJTZFLSe F0WU41VE5bHomiBy1mZQZUGoCdoLqmkZBDTHGaim9g281EyAgzG4KpLhn1/38GLY2qQl bk68IeYrhJXcP6XiTiuhyhHgpQQOfG7I6VWucEswp2TA4bjq+Q8Q1IXZKP9/FrlmbLnj 5pAxtr9JMY92NzBp4aqXfhjRUnjZ9XLczh7/5XOAZsSdbFivhqcy4iz1LnIhgBfsZL0u eFZtHuW6IOPlcfGGXAWjaGHjU9FY+3m13UmqT9M8rVYkVq7YHcuNaYpDGjEIICSUbjE+ PSQw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ZCYV8o4N; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::12f as permitted sender) smtp.mailfrom=kevin.m.buzzard@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=SO7ivnsmpBjq8uOAVVW3THCLw76hL4yvohFyhmdBnY0=; b=LLOwzPkaGKjWAyWc1E91SUFauQuk0s7dAtsBitprX8uyDxO3tzOmfCacO7FvwlN4O9 Lb/dahFZpd6rHipuXJXunXBHK3hQuxYUx/3kqdjSvXgyjHfuDcX5xlUWJWPS/+Tdb3zG 95TwjGKZ5/IwP9fJqGKgYOYPHnppy3Q+8iP/zrKXRKajj44LdvY/F1nLt03r/mDNnvHz mneZFAxhqxQGaZCSAQtyKTKZXoZDP6hYlO2TFINE6MtYMiplCPolFsbIEwbkZVdfsV9m VtrV+RbW1mlA+qRwIcKLMcnMRpihGFs6F2t+4yoxBF7E9PA82/ZNohQEZL24r535CTO9 MO5Q== 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=SO7ivnsmpBjq8uOAVVW3THCLw76hL4yvohFyhmdBnY0=; b=s4//K6Xasg4OK9KFu5bTQlkC7gvCoVrR900Iwi5lm99TXH6JQvX8pieHXrkP/giPt1 Op5E8pERhtu3LlYoMIY5gDXhbtqLqmlxWG/VhIZT+nb3ecDJtGIxXtXjW9OL4cZZILP1 kJeatPaPxcmfeYyW2CP75dpJpwxq8MPTMgmoZBQ4EQmr+vQXoXXW1TTR15aLooqLtV/8 kIX/A7OuYc/9yNYn+vUPvnlXCDeRN1KkMTfID9gMzknxRLHZI1Lr15XI3G4sIuyWngU4 rUkz8UbXcAlTZd6Q9ByP06ixCDGq0mZZs0a95mrQsHuTh6W2MmH7q2q3DCJL7IbkVa3/ w0zw== 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=SO7ivnsmpBjq8uOAVVW3THCLw76hL4yvohFyhmdBnY0=; b=XTDYqw57JGsxmMFPa3hTnWI1qUJ05d5O4+q29dRauijqehifNYw3fLS6H2pnzZjhvA 7bTa55+9C+f8shjt/uMM/D8aeEvvzbWgjd4RXZWl+iYcLDaKbogeeSqO/WkU9NtIzGiv GNOgojPR2CkGCWypiIPG0wiyx4lCFcNoVC488c4mGfHSNqMl7Ytt9zofUqVpEAursjLm mm5bhEcrK/Tfd9GSeU3MQ1w1fJkVVkJ0reRfvBoAQRaySiKvmYlzDkEZtMVPsZla3MeJ /4hkGqR/LDrIjp0lAQe+RU6N8/hOBJjGUCIwu1POYNaM4jXwMbP/yt+R3LrWZmSAoRS/ +8Mw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVHieDyBjaW02XwMGnAYmzwlmeZMzBUJYTiS+5w12pH3AkwhWXX uh1CE5d0RnoovHORcEtfwqU= X-Google-Smtp-Source: APXvYqxrt3laUlpAmvzxDF/N8FRclblxIk0av8EAhaY7FHaV9GIXv4YIGPfxYo7M8ucgK5yXVfQcKA== X-Received: by 2002:a05:600c:2550:: with SMTP id e16mr9507080wma.90.1558870895568; Sun, 26 May 2019 04:41:35 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:4988:: with SMTP id r8ls190319wrq.1.gmail; Sun, 26 May 2019 04:41:34 -0700 (PDT) X-Received: by 2002:adf:fa88:: with SMTP id h8mr19954837wrr.32.1558870894916; Sun, 26 May 2019 04:41:34 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558870894; cv=none; d=google.com; s=arc-20160816; b=fWk81SFp8DAtT+1IOMk7lPcMgB8NrFwihLnZd1UczciRBf2a23xo2EPlonKwmlnTPA Q3C1YVd8fwyspo4XrR2Bq9QSJ05OepXXvDKtxsfQQvpbj21myfvKA124dVclFPwBvehX 4Yxg7bmdvvN/rlI6ymM+QHEOi7l/ybSWUd0CpZggAcKEQIU3yClNxnc2SOWtDw6OMggf ZvOKzh+1RAwjFIj/dS7b9SrKSrQfqPSkDrliuy67na2SfJlOp08Qr0zZDZyHC58ePZKz G5saCvYRwPXzZ/ZU0BbcVbYIVLdMeV2++GxSRVytUEW81KRowaMdmDTuveyedL/0Nnh/ h88A== 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=Cw8aw4JLTFshdhstccBjKlFGgPnNJ8sSZsYY2VbXeUU=; b=K/WNTIS0MHHVqqoHi61VrLh6Ne38lcWhL4NbsEwk+qZsFdBcn2H/HAQIuMquiXuREl V245WQKIpTutE7yK3dUkRg5jo5AO7ywVs7Z84z44H9PpPyngoc/EGUTyv1+rnR+bi2aG fwV85ifldo5hgybbR/n0cC1idqIN82dX4ELHzmu7hlmYiVnDXKLQ36CyJjy4/T3xDdYq l+Ig+sLRZj1+Kbv5QKVl34ggHgUUZz+dixTysByFuc4RI64wI2J7zldZQSFfanSEyGw7 uI/XC3Jbpihn1H0L7o7aV0DUnunM+K43pVUaBYtl69bdexY3PQjjyLQ78tQYD0KFSQBZ +ChA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ZCYV8o4N; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::12f as permitted sender) smtp.mailfrom=kevin.m.buzzard@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lf1-x12f.google.com (mail-lf1-x12f.google.com. [2a00:1450:4864:20::12f]) by gmr-mx.google.com with ESMTPS id x4si142408wmk.1.2019.05.26.04.41.34 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 26 May 2019 04:41:34 -0700 (PDT) Received-SPF: pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::12f as permitted sender) client-ip=2a00:1450:4864:20::12f; Received: by mail-lf1-x12f.google.com with SMTP id m15so9496510lfh.4 for ; Sun, 26 May 2019 04:41:34 -0700 (PDT) X-Received: by 2002:ac2:4430:: with SMTP id w16mr14018692lfl.35.1558870894245; Sun, 26 May 2019 04:41:34 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> In-Reply-To: From: Kevin Buzzard Date: Sun, 26 May 2019 12:41:17 +0100 Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Bas Spitters Cc: Noah Snyder , Homotopy Type Theory , Juan Ospina Content-Type: multipart/alternative; boundary="000000000000e6fd960589c8e913" X-Original-Sender: kevin.m.buzzard@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ZCYV8o4N; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::12f as permitted sender) smtp.mailfrom=kevin.m.buzzard@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: , --000000000000e6fd960589c8e913 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 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 connecti= on > 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 Co= q > 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-HoTT i= s of a >> category from =E2=80=9CCoq with the indices-matter option plus the HoTT = library." >> =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 comp= are >> 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 us= ing >> 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 o= ut >> the standard library and replaced it with a minimal core that is suffici= ent >> 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 homotopica= l >> 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 th= at >> 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, =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 s= ome >> 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 categori= es >> 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 >> 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, "UniM= ath". >>> >>> 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 ad= ds >>> 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 implementa= tion 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 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 th= eory >>>> 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 object. >>>> >>> >>> Yes. This is a pain point in Lean. It's a particularly nasty one too, a= s >>> far as mathematicians are concerned, because when you tell a mathematic= ian >>> "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 y= ou >>> 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 th= en 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 a= s >>> far as I can see this is a place where UniMath is a more natural fit fo= r >>> "the way mathematicians think". However now I've looked over what has >>> currently been formalised in UniMath I am wondering whether there are p= ain >>> points for it, which Lean manages to get over more easily. That is some= how >>> 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, we can as= sume both >>>> algebras are multimatrix algebras over division rings.=E2=80=9D Is th= at step >>>> something you=E2=80=99d be able to deal with easily in Lean? If not, = that=E2=80=99s >>>> 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 developm= ent) >>> 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 error i= n 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 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=E2=80=99s formali= zation 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 >>>>>> 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 ge= nerally >>>>>> about a project of formalising many of the statements of modern pure >>>>>> mathematics in an arbitrary system, such as HoTT. I know enough abou= t the >>>>>> formalisation process to know that whatever system one chooses, ther= e will >>>>>> be pain points, because some mathematical ideas fit more readily int= o some >>>>>> foundational systems than others. >>>>>> > >>>>>> > I have seen enough of Lean to become convinced that the pain point= s >>>>>> 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 depe= ndent >>>>>> types and it seems that one cannot use Isabelle's typeclass system t= o >>>>>> handle the rings showing up in a sheaf of rings. >>>>>> > >>>>>> > I have very little experience with HoTT. I have heard that the fac= t >>>>>> that "all constructions must be isomorphism-invariant" is both a ble= ssing >>>>>> and a curse. However I would like to know more details. I am speakin= g at >>>>>> the Big Proof conference in Edinburgh this coming Wednesday on the p= ain >>>>>> points involved with formalising mathematical objects in dependent t= ype >>>>>> 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 o= f this >>>>>> discussion, "modern pure mathematics" means the statements of the th= eorems >>>>>> publishsed by the Annals of Mathematics over the last few years, so = for >>>>>> example I am talking about formalising statements of theorems involv= ing >>>>>> L-functions of abelian varieties over number fields, Hodge theory, >>>>>> cohomology of algebraic varieties, Hecke algebras of symmetric group= s, >>>>>> 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 wo= rks, >>>>>> 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 minut= es >>>>>> failing to get onto ##hott on freenode ("you need to be identified w= ith >>>>>> 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 Ho= TT >>>>>> 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-4= 1a5-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, sen= d >>>>> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>>>> To view this discussion on the web visit >>>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42= eb-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/CAO0tDg4dyjZHueTP= QEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com >>>> >>>> . >>> >>> >>>> For more options, visit https://groups.google.com/d/optout. >>>> >>> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7LAv8A%2BoXR= LhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%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/CAH52Xb3k9b8D0oW8Ue8XGY-ZAJZHfmc1pTRTJO1Qg%3D3Dw0zwuA%40= mail.gmail.com. For more options, visit https://groups.google.com/d/optout. --000000000000e6fd960589c8e913 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
It seems to me, now I understand much better what is = going on (many thanks to all the people who replied) that dependent type th= eory + impredicative prop "got lucky", in that Coq has been aroun= d for a long time, and Lean 3 is an attempt to model basically the same typ= e theory but in a way more suited to mathematics, written by someone who kn= ows 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 to= p of a file and then not thinking about it any more. HoTT might be more app= ropriate for mathematics -- or at least for some kinds of mathematics -- bu= t 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 tac= tics"), 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 use= rs. 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 tact= ics 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 standar= d Lean documentation.

I am a working mathematician= who two years ago knew nothing about this way of doing mathematics on a co= mputer. Now I have seen what is possible I am becoming convinced that it ca= n 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 n= o immediate benefits in learning how this stuff works. In short, I think ty= pe 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 dep= artment? In the UK at least, the answer is "much less than 1", an= d I cannot see that changing any time soon. I would love to draw the mathem= atics and computer science communities closer together over ideas like this= , but it's hard work. I am wondering whether developing accessible data= bases 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 var= ious systems I do not see this occurring. This weekend I've learnt some= thing about UniMath, but whilst it might do bicategories very well (which a= re not on our undergraduate curriculum), where is the basic analysis? Where= is the stuff which draws mathematicians in? This by no means a criticism o= f 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 t= he derivative of sin is cos, and Isabelle/HOL might never have schemes. I k= now that Gonthier and his coauthors had to make a lot of undergraduate leve= l maths (Galois theory, algebraic number theory, group theory) when formali= sing the odd order theorem in Coq, but it turns out that the odd order theo= rem is perhaps not a good "selling point" for mathematics formali= sation when you're trying to sell to "normal research mathematicia= ns", and I don't know what is. I'm now wondering making formal= ised 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 f= antasy at this point.

One thing I have learnt = over the last two years is that a whole bunch of extremely smart people, bo= th mathematicians and computer scientists, have invested a lot of time in t= hinking about how to do mathematics with type theory. I find it very frustr= ating that mathematicians are not beginning to notice. Of course there are = exceptions. One day though -- will there simply be a gigantic wave which cr= ashes through mathematics and forces mathematicians to sit up and take noti= ce? I guess we simply do not know, but if there is, I hope I'm still ar= ound.

Kevin



On Su= n, 26 May 2019 at 06:50, Bas Spitters <b.a.w.spitters@gmail.com> wrote:
There has been pro= gress in making a cleaner interface with the standard Coq tactics. (Some ab= stractions were broken at the ocaml level)
I'm hopeful th= at 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 exi= sts in agda now.

IIUC, UniMath does not allow any = of the standard library or it's tactics, or even record types, since Vl= adimir wanted to have a very tight connection between type theory and it= 9;s semantics in simplicial sets. So, I don't expect them to connect to= other developments, but I could be wrong.

Abo= ut 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:

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:
UniM= ath 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 option plus the HoTT lib= rary." =C2=A0 =E2=80=9CCoq with the indices-matter option plus the HoT= T library" is of the same category as "Lean plus the math library= " and then it makes sense to compare how practically useful they are f= or math.

Here it's important to n= ote that most advanced things that you can do in Coq are broken by using th= e "indices-matter" option and relatedly not using the built-in ty= pe Prop.=C2=A0 Quoting from=C2=A0https://arxiv.org/abs/1610.04591 "This small = change makes the whole standard library unusable, and many tactics stop wor= king, too.=C2=A0 The solution was rather drastic: we ripped out the standar= d library and replaced it with a minimal core that is sufficient for the ba= sic tactics to work." =C2=A0

(In particular, = I was in error in my previous email, *some* tactics are available in Coq+in= dices-matter+HoTT, but not many of the more advanced ones, and to my knowle= dge, not tactics needed for complicated homotopical calculations.)

I should say I've never used Coq, just Agda. =C2=A0(Wh= en I was using Agda the situation was even worse, things like pattern match= ing 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.) =C2=A0S= o I'm likely wrong in some 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 Le= an) for doing ordinary mathematics.=C2=A0 However, if and when it does catc= h up some of the pain points involving transporting from my previous email = should go away automatically. =C2=A0(Side comment: once you start talking a= bout transporting stuff related to categories across equivalences of catego= ries it's only going to get more painful in ordinary type theory, but w= ill remain easy in HoTT approaches.)

Best,

Noah

p.s. Installed Lean last we= ek.=C2=A0 Looking forward to using it next year when Scott and I are both a= t MSRI.

On Sat, May 25,= 2019 at 11:36 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote:
<= blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-l= eft:1px solid rgb(204,204,204);padding-left:1ex">
Hi N= oah. Thank you for pointing out the category error. It seems to me that som= etimes when I say "HoTT" I should be saying, for example, "U= niMath".

Tactics in Lean are absolutely cruci= al for library development. Coq has some really powerful tactics, right? Un= iMath can use those tactics, presumably?

I underst= and that UniMath, as implemented in Coq, takes Coq and adds some "rule= s" of the form "you can't use this functionality" and al= so adds at least one new axiom (univalence).

On Sat, 25 May 2019 = at 15:50, Noah Snyder <nsnyder@gmail.com> wrote:
I=E2=80=99d also imagine that= a =E2=80=9Cpractical=E2=80=9D implementation would likely have some kind o= f =E2=80=9Ctwo-level=E2=80=9D type theory where you can use types that beha= ve classically when that=E2=80=99s better and HoTT types when that=E2=80=99= s better.

But plain Coq has suc= h types, right?

OK so this has all been extremely = informative. There are other provers being developed which will implement s= ome 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 const= ruction 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 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 tel= l 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 cr= azy system you are using which cannot deduce this immediately. As an intere= sting experiment, find your favourite mathematician, preferably one who doe= s not know what a Cohen-Macauley ring is, and ask them whether they think i= t 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 isomorph= ism-invariant. This is part of our code of conduct, in fact.
=
However in Lean I believe that the current plan is to try an= d 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 t= here are pain points for it, which Lean manages to get over more easily. Th= at is somehow where I'm coming from.
=C2=A0
=C2=A0For examp= le, say you have a theorem about bimodules over semisimple rings whose proo= f starts =E2=80=9Cwlog, by Artin-Wedderburn, we can assume both algebras ar= e multimatrix algebras over division rings.=E2=80=9D =C2=A0Is that step som= ething you=E2=80=99d be able to deal with easily in Lean?=C2=A0 If not, tha= t=E2=80=99s somewhere that down the line HoTT might make things more practi= cal.

This is a great example! To = be honest I am slightly confused about why we are not running into this sor= t 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=E2=80=99re making a category error in your question= .=C2=A0 HoTT is an abstract type theory, not a proof assistant.

Best,

Noah=C2=A0

<= div dir=3D"ltr" class=3D"gmail_attr">On Sat, May 25, 2019 at 9:34 AM Juan O= spina <jospina6= 5@gmail.com> wrote:
On page 117 of https://arxiv.org/pdf/1808.10690.pd= f appears the "additivity axiom".=C2=A0 Please let me know if= the following formulation of the such axiom is correct:

3D"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= =E2=80=99s formalization of=20
the Atiyah-Hirzebruch and Serre spectral sequences for cohomology=20
in HoTT using Lean:

=C2=A0https://arxiv.org/abs/1808.10690

Regards,

Steve

> On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> wrote:
>=20
> Hi from a Lean user.=20
>=20
> As many people here will know, Tom Hales' formal abstracts pro= ject https://formalabstracts.github.io/ wants to formalise many = of the statements of modern pure mathematics in Lean. One could ask more ge= nerally about a project of formalising many of the statements of modern pur= e 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.
>=20
> I have seen enough of Lean to become convinced that the pain point= s would be surmountable in Lean. I have seen enough of Isabelle/HOL to beco= me skeptical about the idea that it would be suitable for all of modern pur= e mathematics, although it is clearly suitable for some of it; however it s= eems that simple type theory struggles to handle things like tensor product= s of sheaves of modules on a scheme, because sheaves are dependent types an= d it seems that one cannot use Isabelle's typeclass system to handle th= e rings showing up in a sheaf of rings.
>=20
> I have very little experience with HoTT. I have heard that the fac= t that "all constructions must be isomorphism-invariant" is both = a blessing and a curse. However I would like to know more details. I am spe= aking at the Big Proof conference in Edinburgh this coming Wednesday on the= pain points involved with formalising mathematical objects in dependent ty= pe theory and during the preparation of my talk I began to wonder what the = analogous picture was with HoTT.
>=20
> 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 y= ears, 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, Ri= cci 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, a= nd what it is.
>=20
> If this is not the right forum for this question, I would be happi= ly directed to somewhere more suitable. After spending 10 minutes failing t= o get onto ##hott on freenode ("you need to be identified with service= s") I decided it was easier just to ask here. If people want to chat d= irectly I am usually around at https://leanprover.zulipchat.com/ = (registration required, full names are usually used, I'll start a HoTT = thread in #mathematics).
>=20
> Kevin Buzzard
>=20
> --=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 email to HomotopyTypeTheory+unsubscribe@googleg= roups.com.
> To view this discussion on the web visit https://groups.goog= le.com/d/msgid/HomotopyTypeTheory/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40go= oglegroups.com.
> For more options, visit https://groups.google.com/d/optout<= /a>.

--
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 ht= tps://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 &= 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.
<= /blockquote>

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://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg= 7LAv8A%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 &= 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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb3k9b8D0oW8Ue8XGY-ZAJZHfm= c1pTRTJO1Qg%3D3Dw0zwuA%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--000000000000e6fd960589c8e913--