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.2 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-vk1-xa38.google.com (mail-vk1-xa38.google.com [IPv6:2607:f8b0:4864:20::a38]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 7823ec8a for ; Sat, 25 May 2019 16:42:03 +0000 (UTC) Received: by mail-vk1-xa38.google.com with SMTP id z6sf5201357vkd.12 for ; Sat, 25 May 2019 09:42:03 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558802522; cv=pass; d=google.com; s=arc-20160816; b=Ou8b9wbV+rbCf7oUtjaXW1yCDP2uJq2j2iDinb7MriBZvd8vBA7GCITsV4EImy8e/u Mj6uKWyHYwNjAwmByTRv6vWZUcsg7egthZ2zOfpKA3YfIbcOFSisj6As6AkevO+B1wW+ MiBOcEupt8Hj0xAT8zYfPiX/lK7XELcN/l8vauxXW/ss63pBjRNfoTlJM/O63gvCEgxQ CdEwSTqq9mKVWcE3CN7nrbnTqN4c/75y9VoUQqP8O2jqnVRYdoIkpgZ/8TtxFfRrs1Rm zDpKhHrhZWjG9kzvfMU3r+FQ2eNQrpBXNCv3j5w6DvnpJRHQg7P/lBndTQg4ejKoX81/ QYqQ== 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=bUMK04TqIiSJjamZpCzJ7fi98r6f/qICxeJ4b6/6RlU=; b=tiNV7qVFDoQOWqVKEhOXgISADMOisGLmiE5yvJ/ptycSXo+dzueC+iNwaBckhZP3WQ EwF+feyLY6E6eDOk+ak/G6LiVHAMzEfbJ3MbklgUfPuozJDUWs9ylLD9kXqR5uhSivMj 56Np4/ZGnrTCYo9a9Nrrwsmrx/3n0ABJK+QEtqBgUMIN3pHLpyTFYBhs6rmFXF3OmAu6 PgV4AJI6qORn8ou+xAMs5Cna27u1fALP5Q1By8ueTo9ImFgThcTiqrb9uWM0J2Xt5JLr WUEJmF0VqZmPkiDuvQ0o7CY+FHEccK8fhN+gBXX/g5dNiI5AWM5mbD1WoHzdiI4utAzZ 8ZrQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=cHvkc9V6; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::232 as permitted sender) smtp.mailfrom=nsnyder@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=bUMK04TqIiSJjamZpCzJ7fi98r6f/qICxeJ4b6/6RlU=; b=B7zGv3n09bHL2fE8N9bJOGMXN/nSmvY0HixgJ1zc/pycEGDVIAE1U5raHMOXbYu+Gs CmoxPo6YvxeFYt6IR/x3O8gsnfV99nOwER2DVoHbbA+6vxeOG0UnOWsXJDHEkIfePuUh zJ8kFUxYPB2N/kdVHbjGKtaCPe7zaqSzKqx8cLnAB+AG60Ls048N/1PXBpWJMuOyG9Tb hBvOosnl/jsxcEq+6U/JOgXiALviZxE8shU0/5ePhV1SZMoLJjQ6s6Nlyk7aum7YaQBn rskuaOQg/g3cyMqM1HesxMPbvztf+trGi7OSjuU+ckTqBhmwmoFMUmTCrPQpJ0X+KBml 9sqg== 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=bUMK04TqIiSJjamZpCzJ7fi98r6f/qICxeJ4b6/6RlU=; b=EMz1XL6fWI5yHQHPE8y37UwvyoveqzQmvPvbjAbd1sz+di2NbJZXBntl9mTcxr7Bog D/QfNL+0aband3lL+yeRD7mO1nXu9eHnaBGv2LLLRx6KIJobCcxQTSSNHkTRixy72k7A 4jYYDVYNuOMPAME52Pa2Cm2joZe2lsRrW81LI/Pl5CUKSxmR8g4JkqFc8R+OL0GhvKnU bSKuHls9z541MniaCDa9cQDn3ry/fAYzbJHSQKxnkA0wdzuTcHZQ4MchW8C5MNCzOCMj vP9W+nAWEsGRlkUb/mnY1g79qGvs+o+lyUXVHJva/dyFnnketUQ4R9ROdNHfoec/LF8s 6bYA== 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=bUMK04TqIiSJjamZpCzJ7fi98r6f/qICxeJ4b6/6RlU=; b=hXHbJXaPAZsh3grppS+z+hoSnctxi5m/m8/Rwcj0gWAOllt41AzW+bFhh19C+vIQkG nxremS4poAV8IF6qjghrzyptua41lrMWG/cA1Zfy5+lAHV1TI5ZT3XFuZqBxZ/nuRWDb reFSEIG8aWbRgHq2sLIqlx+UGGccvugzgwjPDh8c+ZCq4MxdPbF8uhrs97eD/9ZfeDtx vz5bdDCQY+8Tm9IyXnXGUmc2Bg1hca82iO0yHnSGUGR8NdEkZMzHbTw9nicJUT5/Zd7y Rw3WoJVfdzuFXJAoCKGRGwSaOK0jHpaCLRyRofllSy86IZi4DvaZEU26vpuCMYqeHJaO 3ZSQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUYq3i2BL1bp/E8YPX7OofgjUP81BoaS/bIA0iiJHahrsdZmy3m fxULzM05+Kef4bXmomMl5R0= X-Google-Smtp-Source: APXvYqxDmoAzkKZsOEMHa5RhE6FGtsgC5i6RnIg09fmWZZzltH1QVinCAFw0/GpumgdwbjvW6Caqrw== X-Received: by 2002:a67:d71d:: with SMTP id p29mr62566031vsj.223.1558802522435; Sat, 25 May 2019 09:42:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a67:72c6:: with SMTP id n189ls1699890vsc.2.gmail; Sat, 25 May 2019 09:42:02 -0700 (PDT) X-Received: by 2002:a67:3052:: with SMTP id w79mr40596114vsw.68.1558802522005; Sat, 25 May 2019 09:42:02 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558802522; cv=none; d=google.com; s=arc-20160816; b=fPurG5GcqH3AshpxR4ZHkH+b95nRdaTAiXNhODdXD61OSwLU/vGCZPqNvnnK1/ef1O qDTbzB26DqqGHw6ljhh1FoUUcUZbBGHM7vFuSl+y8obRqA1Atw9axzXWKBZh2O5njOCL U1a0rktdW4rGCOIbAyUQsEKxQuKzJP7uWag05+9OGuUPFgg8BbVEI0FvMxpb/TFLziUe BjP3oRYD2ZDEzdNiL6BMZD1/mlyHKVlLMLSTT5mvRCHPPjMRR6cQMssMfYkm0ExuV4/p sZZZQ1ZNsScnyMvP5FZtAbe5qB8t6jaOpyDcXhQ5Py0Vk+/itxhmfpxuTcGA6wbUKIMO tonA== 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=fiwVWr4UBBwFBdCY/0iCBxk6CCdpEk/TpQNrrx1QRvU=; b=PL/fCUr/6AiElJYoGQ67MLKCLwGZHt2mdvQ0nPhWnixO/aMGxVbubysBUYVr16Ko/R 37lhxZqErmRHHNzqPywg61BmEmjhZT19YWC20hoxmrX5bEHE4H0rjAJAYt4l4eJJ5w4l iidklrZ+i/cXmFZyHVYVjJb+bmu6Y7PajPplo5o+gELoetZjTMhlVPxkkgFYbyNOgSiL Iz/FO3O/qBai/2ZtQcGzh/y8+HU3NsQ5DKp4qmILOTu/FoSBCdi4EysK3w8gxTlot4M/ JbROa5o2SbM9Vdm8p74OjcXQhKMJxySqUDF7uwyzQlI723BpV/HClJTf5MuHbPrOveCS xl1A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=cHvkc9V6; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::232 as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-oi1-x232.google.com (mail-oi1-x232.google.com. [2607:f8b0:4864:20::232]) by gmr-mx.google.com with ESMTPS id m21si173836vsj.0.2019.05.25.09.42.01 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 25 May 2019 09:42:01 -0700 (PDT) Received-SPF: pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::232 as permitted sender) client-ip=2607:f8b0:4864:20::232; Received: by mail-oi1-x232.google.com with SMTP id w144so9202886oie.12 for ; Sat, 25 May 2019 09:42:01 -0700 (PDT) X-Received: by 2002:aca:558c:: with SMTP id j134mr9644134oib.3.1558802521131; Sat, 25 May 2019 09:42:01 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> In-Reply-To: From: Noah Snyder Date: Sat, 25 May 2019 12:41:49 -0400 Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Kevin Buzzard Cc: Homotopy Type Theory , Juan Ospina Content-Type: multipart/alternative; boundary="0000000000008c0fae0589b8feeb" X-Original-Sender: nsnyder@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=cHvkc9V6; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::232 as permitted sender) smtp.mailfrom=nsnyder@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: , --0000000000008c0fae0589b8feeb Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable UniMath vs HoTT wasn=E2=80=99t exactly my point, UniMath =3D Book-HoTT is o= f a category from =E2=80=9CCoq with the indices-matter option plus the HoTT lib= rary." =E2=80=9CCoq with the indices-matter option plus the HoTT library" is of th= e same category as "Lean plus the math library" and then it makes sense to compare how practically useful they are for math. Here it's important to note that most advanced things that you can do in Coq are broken by using the "indices-matter" option and relatedly not using the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04591 "This small change makes the whole standard library unusable, and many tactics stop working, too. The solution was rather drastic: we ripped out the standard library and replaced it with a minimal core that is sufficient for the basic tactics to work." (In particular, I was in error in my previous email, *some* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical calculations.) I should say I've never used Coq, just Agda. (When I was using Agda the situation was even worse, things like pattern matching secretly assumed k even if you used the without-k option, and HITs were put in by a hack that wasn't totally clear if it worked, etc.) So I'm likely wrong in some places above. So I think from a practical point of view, =E2=80=9CCoq with the indices-ma= tter option plus the HoTT library" is well behind ordinary Coq (and also Lean) for doing ordinary mathematics. However, if and when it does catch up some of the pain points involving transporting from my previous email should go away automatically. (Side comment: once you start talking about transporting stuff related to categories across equivalences of categories it's only going to get more painful in ordinary type theory, but will remain easy in HoTT approaches.) Best, Noah p.s. Installed Lean last week. Looking forward to using it next year when Scott and I are both at MSRI. On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard 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, "UniMat= h". > > Tactics in Lean are absolutely crucial for library development. Coq has > some really powerful tactics, right? UniMath can use those tactics, > presumably? > > I understand that UniMath, as implemented in Coq, takes Coq and adds some > "rules" of the form "you can't use this functionality" and also adds at > least one new axiom (univalence). > > On Sat, 25 May 2019 at 15:50, Noah Snyder wrote: > >> I=E2=80=99d also imagine that a =E2=80=9Cpractical=E2=80=9D implementati= on 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=99= s better. >> > > But plain Coq has such types, right? > > OK so this has all been extremely informative. There are other provers > being developed which will implement some flavour of HoTT more > "faithfully", and it might be easier to develop maths libraries in such > provers. > > For example, if G and H are isomorphic groups and you want to translate a >> theorem or construction across the isomorphism. In ordinary type theory >> this is going to involve annoying book-keeping which it seems like you= =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 tell a mathematicia= n > "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 as > far as I can see this is a place where UniMath is a more natural fit for > "the way mathematicians think". However now I've looked over what has > currently been formalised in UniMath I am wondering whether there are 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, we can assu= me 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? If not, th= at=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 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. 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 formaliza= tion 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 gene= rally >>>> about a project of formalising many of the statements of modern pure >>>> mathematics in an arbitrary system, such as HoTT. I know enough about = the >>>> formalisation process to know that whatever system one chooses, there = will >>>> be pain points, because some mathematical ideas fit more readily into = some >>>> foundational systems than others. >>>> > >>>> > I have seen enough of Lean to become convinced that the pain points >>>> would be surmountable in Lean. I have seen enough of Isabelle/HOL to b= ecome >>>> skeptical about the idea that it would be suitable for all of modern p= ure >>>> mathematics, although it is clearly suitable for some of it; however i= t >>>> seems that simple type theory struggles to handle things like tensor >>>> products of sheaves of modules on a scheme, because sheaves are depend= ent >>>> types and it seems that one cannot use Isabelle's typeclass system to >>>> handle the rings showing up in a sheaf of rings. >>>> > >>>> > I have very little experience with HoTT. I have heard that the fact >>>> that "all constructions must be isomorphism-invariant" is both a bless= ing >>>> and a curse. However I would like to know more details. I am speaking = at >>>> the Big Proof conference in Edinburgh this coming Wednesday on the pai= n >>>> points involved with formalising mathematical objects in dependent typ= e >>>> theory and during the preparation of my talk I began to wonder what th= e >>>> analogous picture was with HoTT. >>>> > >>>> > Everyone will have a different interpretation of "modern pure >>>> mathematics" so to fix our ideas, let me say that for the purposes of = this >>>> discussion, "modern pure mathematics" means the statements of the theo= rems >>>> publishsed by the Annals of Mathematics over the last few years, so fo= r >>>> example I am talking about formalising statements of theorems involvin= g >>>> 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 th= e >>>> hard-core "classical mathematician" stance of the way mathematics work= s, >>>> and what it is. >>>> > >>>> > If this is not the right forum for this question, I would be happily >>>> directed to somewhere more suitable. After spending 10 minutes failing= to >>>> get onto ##hott on freenode ("you need to be identified with services"= ) I >>>> decided it was easier just to ask here. If people want to chat directl= y 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-41a= 5-a3b7-b585e33375d4%40googlegroups.com. >>>> >>>> > For more options, visit https://groups.google.com/d/optout. >>>> >>>> -- >>> You received this message because you are subscribed to the Google >>> Groups "Homotopy Type Theory" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb= -b42b-b9a9f639d89e%40googlegroups.com >>> >>> . >>> For more options, visit https://groups.google.com/d/optout. >>> >> -- >> You received this message because you are subscribed to the Google 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/CAO0tDg4dyjZHueTPQE= YKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%= 40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. --0000000000008c0fae0589b8feeb Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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 option plus the = HoTT library." =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 practically useful th= ey are for math.

Here it's import= ant 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 bui= lt-in type Prop.=C2=A0 Quoting from=C2=A0https://arxiv.org/abs/1610.04591 "This small change mak= es the 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 tactic= s to work." =C2=A0

(In particular, I was in e= rror in my previous email, *some* tactics are available in Coq+indices-matt= er+HoTT, but not many of the more advanced ones, and to my knowledge, not t= actics needed for complicated homotopical calculations.)

I should say I've never used Coq, just Agda. =C2=A0(When I was u= sing Agda the situation was even worse, things like pattern matching secret= ly 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=A0So 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 plu= s the HoTT library" is well behind ordinary Coq (and also Lean) for do= ing ordinary mathematics.=C2=A0 However, if 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: once you start talking about trans= porting stuff related to categories across equivalences of categories it= 9;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.=C2=A0 = Looking forward to using it next year when Scott and I are both at MSRI.

On Sat, May 25, 2019 at 1= 1:36 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote:
Hi Noah. Thank you for pointing out the categor= y error. It seems to me that sometimes when I say "HoTT" I should= be saying, for example, "UniMath".

Tact= ics in Lean are absolutely crucial for library development. Coq has some re= ally powerful tactics, right? UniMath can use those tactics, presumably?

I understand that UniMath, as implemented in Coq, ta= kes Coq and adds some "rules" of the form "you can't use= this functionality" and also adds at least one new axiom (univalence)= .

On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote:
<= /div>
I=E2=80=99d also imagine that = a =E2=80=9Cpractical=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 behav= e 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 i= nformative. There are other provers being developed which will implement so= me flavour of HoTT more "faithfully", and it might be easier to d= evelop 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.=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 pai= n point in Lean. It's a particularly nasty one too, as far as mathemati= cians 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" th= en they begin to question what kind of crazy system you are using which can= not deduce this immediately. As an interesting experiment, find your favour= ite mathematician, preferably one who does not know what a Cohen-Macauley r= ing is, and ask them whether they think it will be true that if R and S are= isomorphic rings and R is Cohen-Macauley then S is too. They will be very = confident that this is true, even if they do not know the definition; stand= ard mathematical definitions are isomorphism-invariant. This is part of our= code of conduct, in fact.

However in Lean I b= elieve that the current plan is to try and make a tactic which will resolve= this issue. This has not yet been done, and as far as I can see this is a = place where UniMath is a more natural fit for "the way mathematicians = think". However now I've looked over what has currently been forma= lised in UniMath I am wondering whether there are pain points for it, which= Lean manages to get over more easily. That is somehow where I'm coming= from.
=C2=A0
=C2=A0F= or example, say you have a theorem about bimodules over semisimple rings wh= ose proof starts =E2=80=9Cwlog, by Artin-Wedderburn, we can assume both alg= ebras are multimatrix algebras over division rings.=E2=80=9D =C2=A0Is that = step something you=E2=80=99d be able to deal with easily in Lean?=C2=A0 If = not, that=E2=80=99s somewhere that down the line HoTT might make things mor= e practical.

This is a great exam= ple! To be honest I am slightly confused about why we are not running into = this sort of thing already. As far as I can see this would be a great test = case for the (still very much under development) transport tactic. Maybe we= don't have enough classification theorems. I think that our hope in ge= neral is that this sort of issue can be solved with automation.
<= br>
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 assis= tant.

Best,

Noah=C2=A0

On Sat, May 25, 2019= at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote:
=
On page 117 of https://arxiv.org/pdf/1808.10690.pdf appea= rs the "additivity axiom".=C2=A0 Please let me know if the follow= ing formulation of the such axiom is correct:

3D"additivity.=



<= /div>

On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey w= rote:
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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXC= h3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--0000000000008c0fae0589b8feeb--