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-ot1-x33c.google.com (mail-ot1-x33c.google.com [IPv6:2607:f8b0:4864:20::33c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ca6495af for ; Sun, 26 May 2019 05:50:36 +0000 (UTC) Received: by mail-ot1-x33c.google.com with SMTP id 68sf7011172otu.18 for ; Sat, 25 May 2019 22:50:35 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558849835; cv=pass; d=google.com; s=arc-20160816; b=AJMxD86qOC+s7mRoaKCFsGnrr4K6xCdfBXRYaCCh0Vxg2Xk78HGSHLs/n3b/+Pevcj pGnbTrvxNZ9qJPYCDb1TKY+xPFkAoos/4vsfX/rPd2orKfdCqm9ow4h8DifhDA5nI4M/ 7wUoRvnSkEhXT3JMIGbpq4NWnPCei2oJQys+PKGxHv7RGVOnBXKbA/EXTVOiwo05ai/W EGcM1ymgjvZ5F3JbH8S9KQhWF5zxYkNrDKU+z+T47WlHWEEVirIjB7zPZ/2Ss1UcoPTe Qrnl3HjemY+TXOvQl9fAdj2p5fBnBjK0UGaltS93W83AltxiUI7xTq4FDJ7kXu4DS/wu sUHw== 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=VamPAqgXdRkwNeYAqCCZ5dQ4s4ocA+5t5Qrk2Ycnbkg=; b=gi7FSa7sftf4Z28c61yhZEawzVNv3ZG3vJ+jVglW6PZJjpCOoRwF4J0bqLR3slkVzv Sxv91SgaJpbHitCFmm68VyhWynHp1wcDN0ytodGhK/OsW0r6Fmd6LvzNqnSUvly8GhOO Aq6LtQsYhOB4HbkcKG3dsHd5bNh3qFnL6J+yJbGSnOtPMwsxkNlt53M5VmOFYbJgQF1y j2UMZsYcIx77OKYcyZmlspWrpD/qBcxpH1p8uuEX6Ql9AsNxoHTD5+ZXXfPgScXivVCD yw8fQAB4RUQ4ZT5ypZiW99ND9KxSAjgNsvdrg6lldC+iYxyzxwxemiFnAlLURoutRkzs Fn4Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=PLkLiRNX; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c2c 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=VamPAqgXdRkwNeYAqCCZ5dQ4s4ocA+5t5Qrk2Ycnbkg=; b=NERa6nyz1XDE59bT6Arg8z0P/4dSaOeTeOQVhf++y5ltbBOMs/Yj0vAYf9GtQnNMGa URmPn5JNT/fBVU+K6ln7HLr8u5LV+PMPvvjejJCVsVfrrZr3wXgayB4bLTglFALdeJEC +/mcjCexsh8xVmVwns9FQpZFFrWeRRPb5J5FkAp4Un3jA7oqt57IWe4tGBpTSvzadAmS GxhhhSDI4DoyQEny/Pk5qHqyRr24n2V+82NYolvkJw7G2tRUDUZG2j1gVA2yxmrtoaco gmm+JvKsmffmQP9LpXcSDaUjzDufl2+Nxx9QHHWOiOaIJaZE5sOO3wDgCYISiuwN9VmX emyg== 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=VamPAqgXdRkwNeYAqCCZ5dQ4s4ocA+5t5Qrk2Ycnbkg=; b=myF1EluvE+510fXc5/avMyq0c0t2TlsFUlkNEMvHaDHny7USA65D/37mpeZ8dnjDjQ B7KkR/yHqkJkdQUv1mqG8cr1LsdFu7yc/F/ONaBjbtKhOcc2bTUCfpfRUZm74uo8+jJw Y98yU6BhChyh+vQZgI7FLX6OG0lwrvwh9Rbj29EE14rDGbA494ZO0+ItiAEmcIeUSrr7 G773SE3DfMDWFDfePZmXqiSs9UvidNxnR77srhmoFtTkzofYFmvPq1dlPjpE80P3sooO rM2zoN0jYYZVtKKQSJuuo1aivVwyNehbLi7xiyGhbhTdQzEuXTxfC+Crqcsz5sHjbFAc SiXQ== 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=VamPAqgXdRkwNeYAqCCZ5dQ4s4ocA+5t5Qrk2Ycnbkg=; b=EdlfFp+x18/DAGWT9UqjUGK04WKJIto2ZpboPMQz9cVKamZWJHu916E+AApYCIVe9I SdF0c+799LLiRe/4gjQdiG6CxqCv4tjHHNTt2DO56gsrPIpQLXPhbSyVyG/3IIpUbe06 n/cHYGCXQmWh5oCb0Cecn4mBIXyjAyqkMkkjC3aGS0SQMe3yLQhjlokWk0FhO423ugN2 oFayYTjwD7IlinYcvdmdYMIvORmUJMO2ZoekQlxs9rQ9IuD+i41C2DOauY4+CWFv9Iwz W8Z+KK5MhKzV73t7smGs18mn0vnQl4L4HBgplbfV4B8szrd0liWy1MY29VBOTUAeHt/T kosA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAV3xv65qFiTqtHskLNVEo1EKYar7q4zlwg4BKLH1wS+Nzzr7SrQ GNq7mHTMN26hFenqGSCWfBY= X-Google-Smtp-Source: APXvYqxUVoZsRQ5qA+yPaNorv2q9OjBsRLJGWUc02m2CzG42Z9kNnFaQlHMOhcLo6nfX4Idh8NNnCQ== X-Received: by 2002:aca:54d8:: with SMTP id i207mr11456159oib.9.1558849834548; Sat, 25 May 2019 22:50:34 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:a8c2:: with SMTP id r185ls2007636oie.15.gmail; Sat, 25 May 2019 22:50:34 -0700 (PDT) X-Received: by 2002:aca:e044:: with SMTP id x65mr11340821oig.70.1558849834117; Sat, 25 May 2019 22:50:34 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558849834; cv=none; d=google.com; s=arc-20160816; b=IprkonLH37lEgJxiOzRTI9Gz4AcAYKdOV+NCz7+QwwNq+bjnkPwMUh5DNW7hBnWQse UsJ5rWZXRh8GjecfgWN+vCCf3ZoIohlkFUNOyhH6hKwLiR4dLciYSRl6zYQpkL+2Uadl PwUb2mG8kveDmo8N0n4UC5xBfJfS1bf2UgReZW2Py3We/jZscgVeiAaT1HxOxpgogMr5 /pceQN81zKNZ9ACxw+prik85DP3iqfSJ7joSWsBzopSGrZY1xstGRp3hxloD/luKwfFl SBc8ws6I4Vkv/8OK8oHK4BPZjdhW1GNsIjoNBbRYyajYpY/elJtl8s8EViFvu4yd6PJC DQow== 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=ybxl1GapumLbxql2RPGnSf9yERz61OtPQ62M8w3Psrc=; b=LTJoUC3w0aG3ItUlORXE1ihvQHGs3dM917ObnSHMPbKnoCncDyjyNnZsp3bAXlZ77j JVKjf4mJcsrGgBxxEr56oC1P4zK3X8Z7vL2GmIse/v6VY7hdu29OYO+qtN1iP7KTH0CB CWmNxlKb41oHt6DMK0dGY3Aa9553eGM81NCpRqaqwgaT5TL6u7P8Et7uuOsnpyDdv4qw 919WUOaNcw1R0YUpirJUq36BdwXnIqwk+bEvPS/bcxm4WkQ07Is7rYfNH98bsDIpNo8/ 8R87K2gapRZR6TFZ530GWJjCF/72XXAeVQosrhmPpcEGDwK7FK2UbZjB2FcQQufvDWlm mWJQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=PLkLiRNX; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c2c 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-yw1-xc2c.google.com (mail-yw1-xc2c.google.com. [2607:f8b0:4864:20::c2c]) by gmr-mx.google.com with ESMTPS id a79si261524oib.2.2019.05.25.22.50.34 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 25 May 2019 22:50:34 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c2c as permitted sender) client-ip=2607:f8b0:4864:20::c2c; Received: by mail-yw1-xc2c.google.com with SMTP id w18so5332781ywa.12 for ; Sat, 25 May 2019 22:50:34 -0700 (PDT) X-Received: by 2002:a81:49d6:: with SMTP id w205mr40801017ywa.263.1558849833538; Sat, 25 May 2019 22:50:33 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> In-Reply-To: From: Bas Spitters Date: Sun, 26 May 2019 07:50:21 +0200 Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Noah Snyder Cc: Kevin Buzzard , Homotopy Type Theory , Juan Ospina Content-Type: multipart/alternative; boundary="0000000000009617770589c40265" 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=PLkLiRNX; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c2c 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: , --0000000000009617770589c40265 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable There has been progress in making a cleaner interface with the standard Coq tactics. (Some abstractions were broken at the ocaml level) I'm hopeful that this can be lead to a clean connection between the HoTT library and more of the Coq developments in the not too distant future. As it exists in agda now. IIUC, UniMath does not allow any of the standard library or it's tactics, or even record types, since Vladimir wanted to have a very tight connection between type theory and it's semantics in simplicial sets. So, I don't expect them to connect to other developments, but I could be wrong. About the bundled/unbundled issue, which also exists in Coq, there's some recent progress "frame type theory" which should be applicable to both Coq and lean: http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51 Coming back to Kevin's question, yes, HoTT (plus classical logic for sets), seems to be the most natural foundation for mathematics as is currently published in the Annals. On Sat, May 25, 2019 at 6:42 PM Noah Snyder wrote: > 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 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 not usi= ng > 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 ou= t > the standard library and replaced it with a minimal core that is sufficie= nt > 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 tha= t > 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 so= me > of the pain points involving transporting from my previous email should g= o > away automatically. (Side comment: once you start talking about > transporting stuff related to categories across equivalences of categorie= s > 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 whe= n > 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, "UniMa= th". >> >> 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 som= e >> "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 implementat= ion 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 theor= y >>> 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 mathematici= an >> "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 yo= u >> are using which cannot deduce this immediately. As an interesting >> experiment, find your favourite mathematician, preferably one who does n= ot >> know what a Cohen-Macauley ring is, and ask them whether they think it w= ill >> be true that if R and S are isomorphic rings and R is Cohen-Macauley the= n S >> is too. They will be very confident that this is true, even if they do n= ot >> 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 pa= in >> points for it, which Lean manages to get over more easily. That is someh= ow >> 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 ass= ume both >>> algebras are multimatrix algebras over division rings.=E2=80=9D Is tha= t step >>> something you=E2=80=99d be able to deal with easily in Lean? If not, t= hat=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 w= e >> are not running into this sort of thing already. As far as I can see thi= s >> 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 o= f 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 formaliz= ation 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 gen= erally >>>>> about a project of formalising many of the statements of modern pure >>>>> mathematics in an arbitrary system, such as HoTT. I know enough about= the >>>>> formalisation process to know that whatever system one chooses, there= will >>>>> be pain points, because some mathematical ideas fit more readily into= some >>>>> foundational systems than others. >>>>> > >>>>> > I have seen enough of Lean to become convinced that the pain points >>>>> would be surmountable in Lean. I have seen enough of Isabelle/HOL to = become >>>>> skeptical about the idea that it would be suitable for all of modern = pure >>>>> mathematics, although it is clearly suitable for some of it; however = it >>>>> seems that simple type theory struggles to handle things like tensor >>>>> products of sheaves of modules on a scheme, because sheaves are depen= dent >>>>> 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 bles= sing >>>>> 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 pa= in >>>>> points involved with formalising mathematical objects in dependent ty= pe >>>>> theory and during the preparation of my talk I began to wonder what t= he >>>>> 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 the= orems >>>>> publishsed by the Annals of Mathematics over the last few years, so f= or >>>>> example I am talking about formalising statements of theorems involvi= ng >>>>> 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 t= he >>>>> hard-core "classical mathematician" stance of the way mathematics wor= ks, >>>>> and what it is. >>>>> > >>>>> > If this is not the right forum for this question, I would be happil= y >>>>> directed to somewhere more suitable. After spending 10 minutes failin= g 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 direct= ly 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-41= a5-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-42e= b-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/CAO0tDg4dyjZHueTPQ= EYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%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. > --=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/CAOoPQuTNxVJ5%2B1Xotk3wzCgaW0C4wcxOdkpHANbOYdK5rCRkiA%40= mail.gmail.com. For more options, visit https://groups.google.com/d/optout. --0000000000009617770589c40265 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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 conn= ection between the HoTT library and more of the Coq developments in the not= too distant future.
As it exists in agda now.

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

About the bundled/unbundled issue, whi= ch also exists in Coq, there's some recent progress "frame type th= eory" which should be applicable to both Coq and lean:

<= /div>
Coming back to Kevin's question, yes, HoTT (plus classical lo= gic for sets), seems to be the most natural foundation for mathematics as i= s currently published in the Annals.

On Sat, May 25, 2019 at 6:42 = PM Noah Snyder <n= snyder@gmail.com> wrote:
UniMath vs HoTT wasn=E2=80=99t exactly my point, UniMat= h =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-ma= tter option plus the HoTT library" is of the same category as "Le= an plus the math library" and then it makes sense to compare how pract= ically useful they are for math.

Here= it's important to note that most advanced things that you can do in Co= q are broken by using the "indices-matter" option and relatedly n= ot using the built-in type Prop.=C2=A0 Quoting from=C2=A0https://arxiv.org/abs/1610.045= 91 "This small change makes the whole standard library unusable, a= nd many tactics stop working, too.=C2=A0 The solution was rather drastic: w= e ripped out the standard library and replaced it with a minimal core that = is sufficient for the basic tactics to work." =C2=A0

(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 advance= d ones, and to my knowledge, not tactics needed for complicated homotopical= calculations.)

I should say I've never used C= oq, just Agda. =C2=A0(When I was using Agda the situation was even worse, t= hings 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.) =C2=A0So I'm likely wrong in some places above.
<= div>
So I think from a practical point of view, =E2=80=9CCoq = with the indices-matter option plus the HoTT library" is well behind o= rdinary Coq (and also Lean) for doing 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 transporting stuff related to categories acros= s equivalences of categories it's only going to get more painful in ord= inary 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 whe= n Scott and I are both at MSRI.

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

Tactics in L= ean are absolutely crucial for library development. Coq has some really pow= erful 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 fu= nctionality" and also adds at least one new axiom (univalence).
<= div>
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 woul= d likely have some kind of =E2=80=9Ctwo-level=E2=80=9D type theory where yo= u can use types that behave classically when that=E2=80=99s better and HoTT= types when that=E2=80=99s better.

<= div>But plain Coq has such types, right?

OK so thi= s has all been extremely informative. There are other provers being develop= ed which will implement some flavour of HoTT more "faithfully", a= nd it might be easier to develop maths libraries in such provers.

For example, if G and H are isomorphic groups and you want to tra= nslate a theorem or construction across the isomorphism.=C2=A0 In ordinary = type theory this is going to involve annoying book-keeping which it seems l= ike you=E2=80=99d have to do separately for each kind of mathematical objec= t.

Yes. This is a pain point in Lean.= It's a particularly nasty one too, as far as mathematicians are concer= ned, 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 i= mmediately 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 mathematicia= n, 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 ring= s and R is Cohen-Macauley then S is too. They will be very confident that t= his 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. Thi= s has not yet been done, and as far as I can see this is a place where UniM= ath is a more natural fit for "the way mathematicians think". How= ever now I've looked over what has currently been formalised in UniMath= I am wondering whether there are pain points for it, which Lean manages to= get over more easily. That is somehow where I'm coming from.
=
=C2=A0
=C2=A0For example, say you have a theorem about bimodules over se= misimple rings whose proof starts =E2=80=9Cwlog, by Artin-Wedderburn, we ca= n assume both algebras 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 mig= ht make things more practical.

Th= is 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 woul= d be a great test case for the (still very much under development) transpor= t tactic. Maybe we don't have enough classification theorems. I think t= hat our hope in general is that this sort of issue can be solved with autom= ation.

Kevin



But mostly I just want to say you=E2=80=99re making a categ= ory error in your question.=C2=A0 HoTT is an abstract type theory, not a pr= oof assistant.

Best,

Noah=C2=A0

On Sat, May = 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote:
On page 117 of <= a href=3D"https://arxiv.org/pdf/1808.10690.pdf" target=3D"_blank">https://a= rxiv.org/pdf/1808.10690.pdf 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/CAOoPQuTNxVJ5%2B1Xotk3wzCgaW0C4= wcxOdkpHANbOYdK5rCRkiA%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--0000000000009617770589c40265--