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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x53f.google.com (mail-ed1-x53f.google.com [IPv6:2a00:1450:4864:20::53f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 46cd3521 for ; Sun, 26 May 2019 17:00:22 +0000 (UTC) Received: by mail-ed1-x53f.google.com with SMTP id p14sf23950344edc.4 for ; Sun, 26 May 2019 10:00:22 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558890021; cv=pass; d=google.com; s=arc-20160816; b=HmUiKcTW3GJPWZpIuFUcATAQCYVunPC5+iXRpsTqJQ8Hx5gNe4iJ8MCfx16E02fqdM 6LZ3POjsyhTDxSYyEadLyZVDOSgogh89yazPYzf0IAUTPg3aTzd42IrxlzvphUQu7KZp uWxebD8x9FlAEXa6hQX7nL1gQJu1nDhSf3nTvIPQAWcjK7pbFX+G83VaB74bCVD9EjFp QCp10TnIaEpmnG/9sdO50AgkkoDp5ByoOyDCSDbQO/U+MB/cgol4JQeR7GFsa5OWxeaq 6oUF0EHT+La8k16Ete3uswwjnM+myxMPETiYhAuUPK5V3uiQVl8I0+mynCcLj/Pat1Xw B5ng== 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:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature:dkim-signature; bh=eqMmFWv0tpaaZcX61CkFrkyN4hHIfK6+WBhZuK49zfg=; b=fykiBOfgUjj9Z5KPftAIsL3++K/iS5BwH5BfgGycKdvd0W4U74YSS6Kapf4QtRvgfY 2OX0ihv+tR0rqulkJSy6+tCQ/Rx7RbijSThEH5vvMD6pkW+Wp6u+PMpACZ2p+NPKkejp maapwyEWzwoyaOo3G2+oWoEeBKKYQKmNFfEryeIxyJku1P/wuA04+kljit0Hi187oiGB 2fbTrLmqB8omSiKQ9dtaQ8aoyAplIBMtUXXDStJ75umFCF/yoIdvB52h/DP5LoHMT18v MXDDYVDKoIbDKgCS5I7TGhCMNJrqKQexEr/mdeul6NnnNaQHbyZ+ftv8qlNc5BEiYrJN ChMw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=cTiKU1fS; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22a 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=eqMmFWv0tpaaZcX61CkFrkyN4hHIfK6+WBhZuK49zfg=; b=MxiX8R+uua2zob0t5rbfAscPSvp+FfQa5nngLgItCIWJFiw0SVW7w1pWuNwbOQ4F9r nlHl1TNALXAu71S8X4C3orh9iTJWl8wvAnJ124OeUdPMgnHbeExPvfQ/C5oBvgpSU2kn QNsm95n0m5JKmRoyjo/hpl/Wj2hn6aZSvlAlxQRS/Nn2jJcrRw69Gt91mrRcYTPCX836 w4lauIyfc68lR0guTIjZjp6SNFHA7iDunn9IzAS5u5DI2NwJjC5kDKzxDon3WG+QbDiz C4obxOUa0AazIZ2Pwz1m2qJO2shlVZZwNbytjO0qukWULO8kEetIT4ZkNOSninI3D8Gk DGsQ== 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=eqMmFWv0tpaaZcX61CkFrkyN4hHIfK6+WBhZuK49zfg=; b=k68rQoYtSZ/xRHKXJoDTiFR2CamhBHgErn5TDyK7YY6ZcZ0KemD/FSC+aGwfgE575D tdOCF6xsXPv6rnm5CyHHFwZj7a1HgAdkYU8YaWV04hNaFiGAMxBILSIrRZ9FYI7uuWXY KrPc10Qc8sx1NcZspTKtuttPOjTk0f0kcobBvJJkBSFBd1JuH0CdVeXWTAlsdLY3LjV/ QpH0FdmTTKAPG5P5lvPzihm8ofzYjqvad7upoZyHcFECNkZkVYytB4FcKVEuKwDKcTo9 gQYYvV0EJAS9GuWZsX6xIfTC5Ca9cEXrmu/nEqC4X/WPc21eHtLgOJyJEi9FjmMdARUS 7UyQ== 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:content-transfer-encoding :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=eqMmFWv0tpaaZcX61CkFrkyN4hHIfK6+WBhZuK49zfg=; b=YUSrLCeDCkS+Lr/vggOasMcg+ggn5rnRx4I1ulRx8H3CLDEnSC9pTAa6+TpIszX5BZ 7NyJpvZ4LdEC/NqW4O/sxMcVdF53krbR5ANIGhfFci5OSFjF4yUuTw451tPxPXnlNDff V6H95ODbCS2u/JgLBNaNf5k7r08jnQTa7F036KPqXlpQWSrjrAs15xl3L0NZWoy5fXpF cMNvXjnVJblcXeLpdVcTFLBfJ9Nd0W7ZTw7EbpS0zRPqC2ALzOPFbab7ywUFCbJL+VAc 63Od55mKmDqOLbcdGUa49L7FOnScvQo1F48WgkQITZUrrdQcmFGQlwySleIB52whZh4J evMg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAW8m3+f8aQoxy3sNfSgNBZfWeMjK+XYEGhfhdH3gDOH8v3VTOPH xQs8ztxD0DbNUyXLprpd0SI= X-Google-Smtp-Source: APXvYqxDVOhixgW5wAaSKQPTPjvH5DLHrZxEb/OEUDtjrLOIMmgVMUzSEFOEklK13c/Oqg8TrmZHLQ== X-Received: by 2002:a17:906:6a50:: with SMTP id n16mr93244392ejs.119.1558890021583; Sun, 26 May 2019 10:00:21 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:aef7:: with SMTP id f52ls4055063edd.13.gmail; Sun, 26 May 2019 10:00:20 -0700 (PDT) X-Received: by 2002:a50:86fb:: with SMTP id 56mr118177444edu.83.1558890020955; Sun, 26 May 2019 10:00:20 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558890020; cv=none; d=google.com; s=arc-20160816; b=BpjZmAHKSfNqqHKue6BCG8+PY/QZXbuNTPOk05dgvEu7GFo7CV0xZOTS34cFZZlM+e 1BhgtYR6Ejw3vS9neQn+RLEU2NjMmhlv06uH7U+kOudKBeB3dR9B7cfNvpGFHPnx9EmS oAQ+FgIdWf/2tu1VxuEJGGy3Ghz+AhMPuaxPGw9A6vU7KdqGyihgaCSNm9rmhyhvVMyY KoHKxS0fSS4I/npsDKGC8iluIfI1Xu/Kwjt3LlqZGF2D1YyoY7EgqPrIScTpEiuiWRYt PMQ/NAoYhkdU/st312gwqsJsgQrRODY81/GiXwN95bDpTLdZLeHdWN/EzPz4zLmTePy6 kH7g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=mQw0rZZO4BnAyqRufFhRNaVV9n4zO8kJS6R703siEhk=; b=Ep6UfYCJqU9mK4bhX5nwRdxKbm2njEjtJzjCcPyp/4cwmrbVdIeYLjmQdREW6laXSU kVCgEyzYp4D4PQtwynFLXWxM1m79VD5Pw4VStNRkRHD2RU2195HgFW07omsbNe0H0c+5 prg5wqvK3VUWh07RED1YnBwTFyNSAvvFq9HwZfrhuw40CkLnP3f7/LvjzEF5EGtZ7cjs V802T5EhjD7YCml23GK6+d8r78Ci3tV/TT+z3fsVPThwnBbjDVXA71VflEwiMo85yybx kcCA4QRD8J+cdUFJC3Vx0mhSHqKF3pwmu8vs2LUXR8YFa/CgHgZwdd7OWzpIVDW+N/73 BHfw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=cTiKU1fS; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22a 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-lj1-x22a.google.com (mail-lj1-x22a.google.com. [2a00:1450:4864:20::22a]) by gmr-mx.google.com with ESMTPS id l30si531680edd.4.2019.05.26.10.00.20 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 26 May 2019 10:00:20 -0700 (PDT) Received-SPF: pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22a as permitted sender) client-ip=2a00:1450:4864:20::22a; Received: by mail-lj1-x22a.google.com with SMTP id r76so1864497lja.12 for ; Sun, 26 May 2019 10:00:20 -0700 (PDT) X-Received: by 2002:a2e:97cf:: with SMTP id m15mr16370874ljj.135.1558890020541; Sun, 26 May 2019 10:00:20 -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 18:00:01 +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: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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=cTiKU1fS; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22a 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: , I would like to again thank the people who have been responding to my posts this weekend with links and further reading. I know the Lean literature but I knew very little indeed about HoTT / UniMath at the start of this weekend; at least now I feel like I know where you guys are. On Sun, 26 May 2019 at 13:09, Bas Spitters wrote= : > It's a slow process, but I believe we are making progress. I agree that it's a slow process! I think that in any computer science department you can find people who know about these tools, indeed in the computer science department at my university there are people using things like Coq for program verification. I think that one measure of success would be when in most mathematics departments you can find someone who knows about this stuff. My personal experience is that we seem to be far from this, at this point. Bas points out the EU-funded project ForMath and I know that Paulson has an EU grant in Cambridge for Isabelle (my impression is that it is centred in the computer science department) and there is a Lean one based in Amsterdam which I know has mathematicians involved. For me the shock is that now I've seen what these things can do, I am kind of stunned that mathematicians don't know more about them. > You seem to be mixing at least two issues. > - HoTT/UF as a foundation > - Current implementations in proof assistants. Yes; when I started this thread I was very unclear about how everything fitted together. I asked a bit on the Lean chat but I guess many people are like me -- they know one system, and are not experts at all in what is going on with the other systems. I had forgotten about the mathcomp book! Someone pointed it out to me a while ago but I knew far less then about everything so it was a bit more intimidating. Thanks for reminding me. I think I have basically said all I had to say (and have managed to get my ideas un-muddled about several things). But here is a parting shot. Voevodsky was interested in formalising mathematics in a proof assistant. Before that, Voevodsky was a "traditional mathematician" and proved some great theorems and made some great constructions using mathematical objects called schemes. Theorems about schemes (his development of a homotopy theory for schemes) are what got him his Fields Medal. Schemes were clearly close to his heart. But looking at the things he formalised, he was doing things like the p-adic numbers, and lots and lots of category theory. I am surprised that he did not attempt to formalise the basic theory of schemes. Grothendieck's EGA is written in quite a "formal" way (although nowhere near as formal as what would be needed to formalise it easily in a proof assistant) and Johan de Jong's Stacks Project https://stacks.math.columbia.edu/ is another very solid attempt to lay down the foundations of the theory. I asked Johan whether he now considered his choice of "nice web pages" old-fashioned when it was now possible to formalise things in a proof assistant, and he said that he did not have time to learn how to use a proof assistant. But Voevodsky was surely aware of this work, and also how suitable it looks for formalisation. Thanks again to this community for all the comments and all the links and all the corrections. If anyone is going to Big Proof in Edinburgh this coming week I'd be happy to talk more. Kevin > > If you want to restrict to classical maths. Then please have a careful > look at how its done in mathematical components: > https://math-comp.github.io/mcb/ > and the analysis library that is currently under development. > https://github.com/math-comp/analysis > > If you went to help connecting this to the HoTT library, it will be > much appreciated. > https://github.com/HoTT/HoTT > > Best wishes, > > Bas > > On Sun, May 26, 2019 at 1:41 PM Kevin Buzzard = wrote: > > > > It seems to me, now I understand much better what is going on (many tha= nks to all the people who replied) that dependent type theory + impredicati= ve 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 s= uited to mathematics, written by someone who knows what they're doing (de M= oura). Using nonconstructive maths e.g. LEM or AC etc in Lean 3 is just a m= atter of writing some incantation at the top of a file and then not thinkin= g about it any more. HoTT might be more appropriate for mathematics -- or a= t least for some kinds of mathematics -- but its implementation in an actua= l 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 barr= ier for mathematicians a bit (and speaking from personal experience, alread= y this entry barrier is quite high). High level tactics are absolutely cruc= ial for mathematical Lean users. This is one of the reasons that the Lean d= ocumentation is not ideal for mathematicians -- mathematicians need very ea= rly on to be able to use tactics such as `ring` or `norm_num` to do calcula= tions 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 experien= ce the biggest obstruction to it changing mathematics is simply that mathem= aticians do not see the point of it, or what it has to offer a modern worki= ng mathematician; they can see no immediate benefits in learning how this s= tuff 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 a= re 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 l= ove to draw the mathematics and computer science communities closer togethe= r over ideas like this, but it's hard work. I am wondering whether developi= ng accessible databases of undergraduate level mathematics would at least m= ake 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 a= nalysis? 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 pr= ove that the derivative of sin is cos, and Isabelle/HOL might never have sc= hemes. I know that Gonthier and his coauthors had to make a lot of undergra= duate level maths (Galois theory, algebraic number theory, group theory) wh= en 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 formali= sation when you're trying to sell to "normal research mathematicians", and = I don't know what is. I'm now wondering making formalised undergraduate mat= hematics more accessible to untrained mathematicians is a better approach, = but who knows. Obviously "AI which can solve the Riemann hypothesis" will w= ork, 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 o= f extremely smart people, both mathematicians and computer scientists, have= invested a lot of time in thinking about how to do mathematics with type t= heory. 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 mathematic= ians 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 w= rote: > >> > >> There has been progress in making a cleaner interface with the standar= d Coq tactics. (Some abstractions were broken at the ocaml level) > >> I'm hopeful that this can be lead to a clean connection between the Ho= TT 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 tacti= cs, or even record types, since Vladimir wanted to have a very tight connec= tion 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 s= ome 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 s= ets), seems to be the most natural foundation for mathematics as is current= ly 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-HoT= T is of a category from =E2=80=9CCoq with the indices-matter option plus th= e HoTT library." =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 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 u= sing the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04591= "This small change makes the whole standard library unusable, and many tac= tics stop working, too. The solution was rather drastic: we ripped out the= standard library and replaced it with a minimal core that is sufficient fo= r the basic tactics to work." > >>> > >>> (In particular, I was in error in my previous email, *some* tactics a= re available in Coq+indices-matter+HoTT, but not many of the more advanced = ones, and to my knowledge, not tactics needed for complicated homotopical c= alculations.) > >>> > >>> 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 pl= aces above. > >>> > >>> So I think from a practical point of view, =E2=80=9CCoq with the indi= ces-matter option plus the HoTT library" is well behind ordinary Coq (and a= lso Lean) for doing ordinary mathematics. However, if and when it does cat= ch 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 rema= in 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, "UniMa= th". > >>>> > >>>> Tactics in Lean are absolutely crucial for library development. Coq = has some really powerful tactics, right? UniMath can use those tactics, pre= sumably? > >>>> > >>>> 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 impleme= ntation would likely have some kind of =E2=80=9Ctwo-level=E2=80=9D type the= ory where you can use types that behave classically when that=E2=80=99s bet= ter 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 prove= rs being developed which will implement some flavour of HoTT more "faithful= ly", 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 trans= late 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= , as far as mathematicians are concerned, because when you tell a mathemati= cian "well this ring R is Cohen-Macauley, and here's a ring S which is isom= orphic to R, but we cannot immediately deduce in Lean that S is Cohen-Macau= ley" then they begin to question what kind of crazy system you are using wh= ich cannot deduce this immediately. As an interesting experiment, find your= favourite mathematician, preferably one who does not know what a Cohen-Mac= auley ring is, and ask them whether they think it will be true that if R an= d S are isomorphic rings and R is Cohen-Macauley then S is too. They will b= e very confident that this is true, even if they do not know the definition= ; standard mathematical definitions are isomorphism-invariant. This is part= of our code of conduct, in fact. > >>>> > >>>> However in Lean I believe that the current plan is to try and make a= tactic which will resolve this issue. This has not yet been done, and as f= ar as I can see this is a place where UniMath is a more natural fit for "th= e way mathematicians think". However now I've looked over what has currentl= y been formalised in UniMath I am wondering whether there are pain points f= or it, which Lean manages to get over more easily. That is somehow where I'= m coming from. > >>>> > >>>>> > >>>>> For example, say you have a theorem about bimodules over semisimpl= e rings whose proof starts =E2=80=9Cwlog, by Artin-Wedderburn, we can assum= e 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, that=E2=80=99s somewhere that down the line HoTT might make things mor= e practical. > >>>> > >>>> > >>>> This is a great example! To be honest I am slightly confused about w= hy 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 th= ink 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 erro= r 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 w= rote: > >>>>>> > >>>>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the "a= dditivity axiom". Please let me know if the following formulation of the s= uch axiom is correct: > >>>>>> > >>>>>> > >>>>>> > >>>>>> > >>>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: > >>>>>>> > >>>>>>> A useful example for you might be Floris van Doorn=E2=80=99s form= alization 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 proj= ect https://formalabstracts.github.io/ wants to formalise many of the state= ments of modern pure mathematics in Lean. One could ask more generally abou= t a project of formalising many of the statements of modern pure mathematic= s in an arbitrary system, such as HoTT. I know enough about the formalisati= on process to know that whatever system one chooses, there will be pain poi= nts, because some mathematical ideas fit more readily into some foundationa= l systems than others. > >>>>>>> > > >>>>>>> > I have seen enough of Lean to become convinced that the pain po= ints 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 = pure mathematics, although it is clearly suitable for some of it; however i= t seems that simple type theory struggles to handle things like tensor prod= ucts of sheaves of modules on a scheme, because sheaves are dependent types= and it seems that one cannot use Isabelle's typeclass system to handle the= rings showing up in a sheaf of rings. > >>>>>>> > > >>>>>>> > I have very little experience with HoTT. I have heard that the = fact that "all constructions must be isomorphism-invariant" is both a bless= ing and a curse. However I would like to know more details. I am speaking a= t the Big Proof conference in Edinburgh this coming Wednesday on the pain p= oints involved with formalising mathematical objects in dependent type theo= ry and during the preparation of my talk I began to wonder what the analogo= us picture was with HoTT. > >>>>>>> > > >>>>>>> > Everyone will have a different interpretation of "modern pure m= athematics" so to fix our ideas, let me say that for the purposes of this d= iscussion, "modern pure mathematics" means the statements of the theorems p= ublishsed by the Annals of Mathematics over the last few years, so for exam= ple I am talking about formalising statements of theorems involving L-funct= ions of abelian varieties over number fields, Hodge theory, cohomology of a= lgebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the = like; one can see titles and more at http://annals.math.princeton.edu/2019/= 189-3 . Classical logic and the axiom of choice are absolutely essential --= I am only interested in the hard-core "classical mathematician" stance of = the way mathematics works, and what it is. > >>>>>>> > > >>>>>>> > If this is not the right forum for this question, I would be ha= ppily 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 directly= I am usually around at https://leanprover.zulipchat.com/ (registration req= uired, full names are usually used, I'll start a HoTT thread in #mathematic= s). > >>>>>>> > > >>>>>>> > Kevin Buzzard > >>>>>>> > > >>>>>>> > -- > >>>>>>> > You received this message because you are subscribed to the Goo= gle Groups "Homotopy Type Theory" group. > >>>>>>> > To unsubscribe from this group and stop receiving emails from i= t, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > >>>>>>> > To view this discussion on the web visit https://groups.google.= com/d/msgid/HomotopyTypeTheory/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googl= egroups.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%40googlegr= oups.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, s= end an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > >>>>> > >>>>> To view this discussion on the web visit https://groups.google.com/= d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQO= mMw%40mail.gmail.com. > >>>>> > >>>>> > >>>>> For more options, visit https://groups.google.com/d/optout. > >>> > >>> -- > >>> You received this message because you are subscribed to the Google Gr= oups "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/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1i= wztPg%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/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3= A%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.