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-lj1-x23d.google.com (mail-lj1-x23d.google.com [IPv6:2a00:1450:4864:20::23d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e61e4b0f for ; Tue, 4 Jun 2019 20:58:39 +0000 (UTC) Received: by mail-lj1-x23d.google.com with SMTP id p13sf3491209ljc.9 for ; Tue, 04 Jun 2019 13:58:38 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1559681918; cv=pass; d=google.com; s=arc-20160816; b=oulv2Qm1cCBa45SIaPHisBKJkGfWG7yL0LC3EebwF6isZlTMlVl2NNh8Ou2dAe82uB qkCpT72X7XuwqdAJctZOx/H19OwaqoF7c6bh8r6yomj/02PxN79aIi2Dz7wKSEyfXCF4 HXxQEEQOpPxojz52qd39JAFAaxPQYsGM6PAGCU6OqmAS/Vt5f4iCDfoszmQsXOuoU7hL sRQVq8Q0nvPPYHx7BMeSxopCAeHPsdiGGROs/QQmeQpQO3mgM01kYQBwJJpBGzu+1dbH Bpxky3T6Rf7MKcubh74PmZuiLdF7bmcwP7n+yVxfO4LD/5XyYcfr+Ew8TNCIdjhvcEyG CMbQ== 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=X/eNMc6LN0FMEj9x33VQeMHVUikq7/NcYvHMbLbNnk8=; b=Z8PFu+mB3xQBThU+zutTdmv+YFiGjCdpaln3O5v+KZOMKWj1msRXDVKH/aq4jyAdUh JhsarFz/fkbHJyofDR/jshyeNeDS0vlVoXFrh5DotyFViWErRb45ynE8SvyoG48V/0Db TMf1Z07amn/c046DjQHBH+js7tO6kUcZuCxzQDjeFzQZTR/DEw5KAMIHShsPe3gqFrR5 5jJ7ppcjo8jZd0nQDiJYCS1RrWX50r3dQ83VGDR40rftxvtsxHmGNDLm6poWvn/Ub5bm LTc5CFl20D8/QNCPcAlVfsR/MGPBoa3NsPvFnMtvnilev7x3PwN10ZG93TPw43tSHlCU 2r7g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=p0w36vre; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::234 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=X/eNMc6LN0FMEj9x33VQeMHVUikq7/NcYvHMbLbNnk8=; b=CI36npmd9BSJdAlKvXsVxoc/MOe7KfklN3/9hxbB3B56SpB+Kw31l3AmUqCYhIXJ28 ltGG3Nge+cNVq15JzQ/8xE2OLjmJc9e2JownVrBWeXfD6bA+VB4yUJ89zPnieJVlXu32 d2nybQ6ojR1RPZiqgvz7rfyYvf4YYUbwk2iGZFsy/WkshGnmBtoRVZni61EZbXu9bE+v kEP9QwoWl5VSQf1TmCblpl5g78dtFaU16rBJwWm+VRClbYTNlx4JHQ8Z8HRUr3XeQ2IS EEhiPCltKbE4vrK2NPkOXEKUfwVIOXpKiG6qAEU8oqxM/lZKUmKfx8AOsGdS7shbywaq PN9A== 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=X/eNMc6LN0FMEj9x33VQeMHVUikq7/NcYvHMbLbNnk8=; b=Y5suCf5O1VZmAEjA+da6u5iGXe2vWGANixqCr2RknP4/4B9h5fgy5bIKH/9DRVA1ie f5iTYiRoUDjIsc8jzqmtpdgBZd0XFD5oEVIn3VDmQn+u/lirC4rikdl/A/Qv+9wU7gnH 1NvLvdNsVCckMKJRHeaR9vDPq+OJ3fW29ZiT12QmZQYQ/Chf/+Jcr9220p467prjE96R os6IusKzp/+xwRlRp0Fd4zuF+t+ZOW+c949JIHBX10Tq9j8c+PhnH4dsaiVIzrImb0+M H5JUoMI+TonjVII+6vr6uDNxcT8CWlHv4Dx1gSqOq7u32bB6IKb49FQ9IBHHUqE787UU TpbA== 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=X/eNMc6LN0FMEj9x33VQeMHVUikq7/NcYvHMbLbNnk8=; b=msIT8aqnpY8DEpDLV2/RtFw7KUUFQAhTmXPjxMUWZ1fEDh+Ed4EQv+XaOcPzDEtoph UyKHEPjkQaK3VZqwE/O3lxRJLrQkblA+OEMgRcWDs+xoj3FLD0x+yD+rN5E0r0Xa6UnX afDD+YEEBSIG76XakwhJnF9Gqc2wWdUMU0vU/m3zpm54aUVFHkxvRRhpmBNaZmJjRC6s gkAOgCeQab0sXIuKJUZoOk8QVBmKZSzTCuIVrlH4RUptC4Zky7l6JkCAS/e3RGhqxu8G fBeXAmS9I391kjtsmDo6Fu5Bww1xysdoYDh/7gxB8dxKYzk2mA9k03xSvI8IZqNCSFVG eeOQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUs+AV5Ly0ToDOa7kc9rjcphShn3/14fV0Y5NhE0uz48XO+qfUI KGVPbFQ8+ejGNprGyCaNwG4= X-Google-Smtp-Source: APXvYqyDeqVR0ZzlTovgD6/tFVO/NmT2uZiIlb7U4LE643AMRzzAgygPBu44qvIVv5vhNAFU6oeEnQ== X-Received: by 2002:a2e:5c6:: with SMTP id 189mr6360058ljf.22.1559681918108; Tue, 04 Jun 2019 13:58:38 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:614d:: with SMTP id m13ls1167lfk.1.gmail; Tue, 04 Jun 2019 13:58:37 -0700 (PDT) X-Received: by 2002:ac2:4252:: with SMTP id m18mr17370257lfl.100.1559681917346; Tue, 04 Jun 2019 13:58:37 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1559681917; cv=none; d=google.com; s=arc-20160816; b=W3MRhSE8q0bI2/tl6eiKWFTwQ0RC4RFm8DgqN2Gav5oLoULcz4ELrSjSh0N3xVxPdk qCi24tnCaZqfnamy5N3gZEQzTQbeRtSALoObzGRjdEELdavLvfBzMYVqrmJMNGumPHi5 WCAZdRIZotZwlABjPbAGI2hqpF6YKAH2bhDXlS0oMp5BMmDoiOis17vyOuDyPCX3XM6O H4VJUddHKbjgySz3BCOCHmV4Oqog5FkxXRWtJkncsBSxh78QwD4G0LlWuRqWleV+ZS9r 65JF5I4wwxU6tgCe2elRIvbdG9TJff5hwLaui9bk6fC2wK0XYF8LhN65tsoAG4/WwW6a eyjg== 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=vjfbktHD6kp79hFTUCxo15dZk8cvxQydcdscM3iqT2k=; b=wBwVsL1sZcPwu4OS1d69Nv260AtursSDTORzmsHco6NlARCVjTF5D73zxiTCt3rtwl fR/BpfSl+7/RIe+kZDhNBsdUuDWgJz7rMFVC5O0DnM/ZZEwbpHnHYUUM+SvG8SIwk+ob LpEiBJMBPwA0hs3Kyf/zDh76957XofjpHJqPPUPbyHPgHCklgJxr2psTlkU7SMyyIoGL ixr+/RUwHyK2cNXnqjm76TrsnkgBCdpIjKTqFl4i7+cNi3Hz1cCyA//lxbSGT0JhRZJR QYdukKNtDjoqaHhanSUR5STEyF5qfyYqnCTN6+ngKxJ5dH4C9nofO7jEo15U2nBg2LTJ zFKw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=p0w36vre; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::234 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-x234.google.com (mail-lj1-x234.google.com. [2a00:1450:4864:20::234]) by gmr-mx.google.com with ESMTPS id n4si705349lfl.3.2019.06.04.13.58.37 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 04 Jun 2019 13:58:37 -0700 (PDT) Received-SPF: pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::234 as permitted sender) client-ip=2a00:1450:4864:20::234; Received: by mail-lj1-x234.google.com with SMTP id a10so17847140ljf.6 for ; Tue, 04 Jun 2019 13:58:37 -0700 (PDT) X-Received: by 2002:a2e:6e01:: with SMTP id j1mr17822855ljc.135.1559681916924; Tue, 04 Jun 2019 13:58:36 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> In-Reply-To: From: Kevin Buzzard Date: Tue, 4 Jun 2019 21:58:19 +0100 Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Michael Shulman Cc: Homotopy Type Theory 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=p0w36vre; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::234 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: , The Langlandsy folk (of whom I am one, I guess) sometimes use "canonical" in a completely different way :-/ Randomly googling led me to https://mathoverflow.net/questions/127691/reconciling-lusztigs-results-with= -the-langlands-philosophy (and I'm sure there are other examples -- I've even used it in my own work) where "canonical" is being used to describe a bijection between two sets. This is the thing I've referred to as "mission creep". Everyone thinking about functors and natural transformations etc -- all of these thoughts come to nothing when faced with the assertion that the Langlands correspondence is "canonical". What I believe the word means in that context is "this bijection of sets satisfies a whole bunch of cool properties, and I reserve the right to add to this list of cool properties in the future". This usage of the word has bothered me for years. When Gee and I were trying to write down a precise statement of local Langlands functoriality we ran into this; different experts seemed to have slightly different lists. When we were doing calculations we ran into a property which wasn't on any of the lists we'd seen, but which we wanted to be true, and we asked about whether this property was expected to be true in general, and/or was proved in any of the cases where the local Langlands conjectures were theorems. David Vogan said that indeed it should be on the list and even sketched a proof that it was true in the case of real and complex groups for us; other experts had not seen it before. At that time it really did feel like "canonical" was the same as "magical"; the more questions you asked, the more beautiful it got. The notion was completely unformalisable. One day someone might discover some elusive Tannakian category structure on some set of automorphic representations and all of a sudden the word might acquire some formal meaning, but until then this usage of the word remains a complete mystery to me -- I guess it may as well simply be replaced with the word "mysterious" or "beautiful" or something which is clearly not meant to be definable. As for the other issue, it would be easier to discuss if there were some formalisation of the proof that the structure presheaf on the spectrum of a commutative ring was a sheaf, in one of these HoTT systems. As far as I know this has not yet been done. Part of me wants to encourage the HoTT community to try formalising this statement ("an affine scheme is a scheme", if you like) in some HoTT proof verification system. Of course I could try doing it myself in Lean HoTT but I know I'll never get round to it. There is some subtlety here, which I am still perhaps doing a poor job of explaining. It all boils down to this very sneaky use of "=3D" in EGA. Kevin On Tue, 4 Jun 2019 at 21:32, Michael Shulman wrote: > > I think that often when mathematicians say that an isomorphism is > "canonical" they mean that they've declared transport along it to be > an implicit coercion. So although you can always transport across any > isomorphism, the "canonical" ones are those that don't require > notation. That is, the distinction between canonical and > non-canonical does not reside in the formal system, but in the > superstructure of implicit arguments, coercions, and elaboration built > on top of it. > > > On Sun, Jun 2, 2019 at 10:56 AM Kevin Buzzard = wrote: > > > > On Sun, 2 Jun 2019 at 17:30, Bas Spitters wr= ote: > > > > > > Dear Kevin, > > > > > > Looking at your slides from big proof, the transfer package you're as= king for seems to be very close to what is provided by HoTT. > > > https://xenaproject.wordpress.com/2019/06/02/equality-part-3-canonica= l-isomorphism/ > > > This is explained in many places (e.g. the book). Here's an early art= icle explaining it for algebraic structures: > > > http://www.cse.chalmers.se/~nad/publications/coquand-danielsson-isomo= rphism-is-equality.pdf > > > > > > Have you looked at any of this? Does it provide what you are looking = for? > > > > There is a subtle difference. HoTT transfers theorems and definitions > > across all isomorphisms. In the definition of a scheme, the stacks > > project transfers an exact sequence along a *canonical isomorphism*. > > Canonical isomorphism is denoted by "=3D" in some literature (e.g. see > > some recent tweets by David Roberts like > > https://twitter.com/HigherGeometer/status/1133993485034332161). This > > is some sort of weird half-way house, not as extreme as HoTT, not as > > weak as DTT, but some sort of weird half-way house where > > mathematicians claim to operate; this is an attitude which is > > beginning to scare me a little. > > > > Kevin > > > > > > Best, > > > > > > Bas > > > > > > On Sun, May 26, 2019 at 7:00 PM Kevin Buzzard wrote: > > >> > > >> I would like to again thank the people who have been responding to m= y > > >> 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 guy= s > > >> 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 scien= ce > > >> 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 gue= ss > > >> 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 m= e > > >> a while ago but I knew far less then about everything so it was a bi= t > > >> 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 usi= ng > > >> 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 a= t > > >> the things he formalised, he was doing things like the p-adic number= s, > > >> 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) an= d > > >> 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 page= s" > > >> old-fashioned when it was now possible to formalise things in a proo= f > > >> 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 al= so > > >> how suitable it looks for formalisation. > > >> > > >> Thanks again to this community for all the comments and all the link= s > > >> and all the corrections. If anyone is going to Big Proof in Edinburg= h > > >> this coming week I'd be happy to talk more. > > >> > > >> Kevin > > >> > > >> > > > >> > If you want to restrict to classical maths. Then please have a car= eful > > >> > 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 b= e > > >> > 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 (m= any thanks to all the people who replied) that dependent type theory + impr= edicative prop "got lucky", in that Coq has been around for a long time, an= d Lean 3 is an attempt to model basically the same type theory but in a way= more suited to mathematics, written by someone who knows what they're doin= g (de Moura). Using nonconstructive maths e.g. LEM or AC etc in Lean 3 is j= ust a matter of writing some incantation at the top of a file and then not = thinking about it any more. HoTT might be more appropriate for mathematics = -- or at least for some kinds of mathematics -- but its implementation in a= n actual piece of software seems a bit more hacky at this point ("use Coq, = but don't use these commands or these tactics"), which maybe raises the ent= ry barrier for mathematicians a bit (and speaking from personal experience,= already this entry barrier is quite high). High level tactics are absolute= ly crucial for mathematical Lean users. This is one of the reasons that the= Lean documentation is not ideal for mathematicians -- mathematicians need = very early on to be able to use tactics such as `ring` or `norm_num` to do = calculations with real numbers or in commutative rings, and these tactics a= re not even mentioned in the standard Lean documentation. > > >> > > > > >> > > I am a working mathematician who two years ago knew nothing abou= t this way of doing mathematics on a computer. Now I have seen what is poss= ible I am becoming convinced that it can really change mathematics. In my e= xperience the biggest obstruction to it changing mathematics is simply that= mathematicians do not see the point of it, or what it has to offer a moder= n working mathematician; they can see no immediate benefits in learning how= this stuff works. In short, I think type theory has an image problem. Sure= there are category theorists who know about it, but how many category theo= rists are there in an average maths department? In the UK at least, the ans= wer is "much less than 1", and I cannot see that changing any time soon. I = would love to draw the mathematics and computer science communities closer = together over ideas like this, but it's hard work. I am wondering whether d= eveloping accessible databases of undergraduate level mathematics would at = least make mathematicians sit up and take notice, but when I look at what h= as been done in these various systems I do not see this occurring. This wee= kend I've learnt something about UniMath, but whilst it might do bicategori= es very well (which are not on our undergraduate curriculum), where is the = basic analysis? Where is the stuff which draws mathematicians in? This by n= o 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 c= an't prove that the derivative of sin is cos, and Isabelle/HOL might never = have schemes. I know that Gonthier and his coauthors had to make a lot of u= ndergraduate level maths (Galois theory, algebraic number theory, group the= ory) when formalising the odd order theorem in Coq, but it turns out that t= he odd order theorem is perhaps not a good "selling point" for mathematics = formalisation when you're trying to sell to "normal research mathematicians= ", and I don't know what is. I'm now wondering making formalised undergradu= ate mathematics more accessible to untrained mathematicians is a better app= roach, but who knows. Obviously "AI which can solve the Riemann hypothesis"= will work, but that looks to me like a complete fantasy at this point. > > >> > > > > >> > > One thing I have learnt over the last two years is that a whole = bunch of extremely smart people, both mathematicians and computer scientist= s, have invested a lot of time in thinking about how to do mathematics with= type theory. I find it very frustrating that mathematicians are not beginn= ing to notice. Of course there are exceptions. One day though -- will there= simply be a gigantic wave which crashes through mathematics and forces mat= hematicians to sit up and take notice? I guess we simply do not know, but i= f there is, I hope I'm still around. > > >> > > > > >> > > Kevin > > >> > > > > >> > > > > >> > > > > >> > > On Sun, 26 May 2019 at 06:50, Bas Spitters wrote: > > >> > >> > > >> > >> There has been progress in making a cleaner interface with the = standard Coq tactics. (Some abstractions were broken at the ocaml level) > > >> > >> I'm hopeful that this can be lead to a clean connection between= the HoTT library and more of the Coq developments in the not too distant f= uture. > > >> > >> 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, th= ere's some recent progress "frame type theory" which should be applicable t= o 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 logi= c 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 B= ook-HoTT is of a category from =E2=80=9CCoq with the indices-matter option = plus the HoTT library." =E2=80=9CCoq with the indices-matter option plus = the HoTT library" is of the same category as "Lean plus the math library" a= nd 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 relatedl= y not using the built-in type Prop. Quoting from https://arxiv.org/abs/161= 0.04591 "This small change makes the whole standard library unusable, and m= any tactics stop working, too. The solution was rather drastic: we ripped = out the standard library and replaced it with a minimal core that is suffic= ient for the basic tactics to work." > > >> > >>> > > >> > >>> (In particular, I was in error in my previous email, *some* ta= ctics are available in Coq+indices-matter+HoTT, but not many of the more ad= vanced ones, and to my knowledge, not tactics needed for complicated homoto= pical calculations.) > > >> > >>> > > >> > >>> I should say I've never used Coq, just Agda. (When I was usin= g 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 t= he indices-matter option plus the HoTT library" is well behind ordinary Coq= (and also Lean) for doing ordinary mathematics. However, if and when it d= oes catch up some of the pain points involving transporting from my previou= s email should go away automatically. (Side comment: once you start talkin= g about transporting stuff related to categories across equivalences of cat= egories it's only going to get more painful in ordinary type theory, but wi= ll remain easy in HoTT approaches.) > > >> > >>> > > >> > >>> Best, > > >> > >>> > > >> > >>> Noah > > >> > >>> > > >> > >>> p.s. Installed Lean last week. Looking forward to using it ne= xt 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 se= ems to me that sometimes when I say "HoTT" I should be saying, for example,= "UniMath". > > >> > >>>> > > >> > >>>> Tactics in Lean are absolutely crucial for library developmen= t. Coq has some really powerful tactics, right? UniMath can use those tacti= cs, presumably? > > >> > >>>> > > >> > >>>> I understand that UniMath, as implemented in Coq, takes Coq a= nd adds some "rules" of the form "you can't use this functionality" and als= o 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 = implementation would likely have some kind of =E2=80=9Ctwo-level=E2=80=9D t= ype 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 othe= r provers being developed which will implement some flavour of HoTT more "f= aithfully", and it might be easier to develop maths libraries in such prove= rs. > > >> > >>>> > > >> > >>>>> For example, if G and H are isomorphic groups and you want t= o translate a theorem or construction across the isomorphism. 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 concerned, because when you tell a ma= thematician "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 Cohe= n-Macauley" then they begin to question what kind of crazy system you are u= sing which cannot deduce this immediately. As an interesting experiment, fi= nd your favourite mathematician, preferably one who does not know what a Co= hen-Macauley ring is, and ask them whether they think it will be true that = if R and S are isomorphic rings and R is Cohen-Macauley then S is too. They= will be very confident that this is true, even if they do not know the def= inition; 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, a= nd 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 c= urrently been formalised in UniMath I am wondering whether there are pain p= oints for it, which Lean manages to get over more easily. That is somehow w= here I'm coming from. > > >> > >>>> > > >> > >>>>> > > >> > >>>>> For 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 Is that step something you=E2=80=99d be able to deal with easily in Le= an? If not, that=E2=80=99s somewhere that down the line HoTT might make th= ings 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 c= an see this would be a great test case for the (still very much under devel= opment) transport tactic. Maybe we don't have enough classification theorem= s. I think that our hope in general is that this sort of issue can be solve= d with automation. > > >> > >>>> > > >> > >>>> Kevin > > >> > >>>> > > >> > >>>> > > >> > >>>>> > > >> > >>>>> But mostly I just want to say you=E2=80=99re making a catego= ry error in your question. HoTT is an abstract type theory, not a proof as= sistant. > > >> > >>>>> > > >> > >>>>> 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: > > >> > >>>>>> > > >> > >>>>>> > > >> > >>>>>> > > >> > >>>>>> > > >> > >>>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote= : > > >> > >>>>>>> > > >> > >>>>>>> A useful example for you might be Floris van Doorn=E2=80= =99s formalization of > > >> > >>>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for coh= omology > > >> > >>>>>>> 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 abstrac= ts project https://formalabstracts.github.io/ wants to formalise many of th= e statements of modern pure mathematics in Lean. One could ask more general= ly about a project of formalising many of the statements of modern pure mat= hematics in an arbitrary system, such as HoTT. I know enough about the form= alisation process to know that whatever system one chooses, there will be p= ain points, because some mathematical ideas fit more readily into some foun= dational 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/H= OL 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; ho= wever it seems that simple type theory struggles to handle things like tens= or products of sheaves of modules on a scheme, because sheaves are dependen= t types and it seems that one cannot use Isabelle's typeclass system to han= dle the rings showing up in a sheaf of rings. > > >> > >>>>>>> > > > >> > >>>>>>> > I have very little experience with HoTT. I have heard th= at the fact that "all constructions must be isomorphism-invariant" is both = a blessing and a curse. However I would like to know more details. I am 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. > > >> > >>>>>>> > > > >> > >>>>>>> > 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 involving = L-functions of abelian varieties over number fields, Hodge theory, cohomolo= gy of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow a= nd the like; one can see titles and more at http://annals.math.princeton.ed= u/2019/189-3 . Classical logic and the axiom of choice are absolutely essen= tial -- I am only interested in the hard-core "classical mathematician" sta= nce of the way mathematics works, and what it is. > > >> > >>>>>>> > > > >> > >>>>>>> > If this is not the right forum for this question, I woul= d be happily directed to somewhere more suitable. After spending 10 minutes= failing to get onto ##hott on freenode ("you need to be identified with se= rvices") 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/ (registrat= ion required, full names are usually used, I'll start a HoTT thread in #mat= hematics). > > >> > >>>>>>> > > > >> > >>>>>>> > Kevin Buzzard > > >> > >>>>>>> > > > >> > >>>>>>> > -- > > >> > >>>>>>> > You received this message because you are subscribed to = the Google Groups "Homotopy Type Theory" group. > > >> > >>>>>>> > To unsubscribe from this group and stop receiving emails= from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > >> > >>>>>>> > To view this discussion on the web visit https://groups.= google.com/d/msgid/HomotopyTypeTheory/a57315f6-cbd6-41a5-a3b7-b585e33375d4%= 40googlegroups.com. > > >> > >>>>>>> > For more options, visit https://groups.google.com/d/opto= ut. > > >> > >>>>>>> > > >> > >>>>>> -- > > >> > >>>>>> 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 fr= om it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > >> > >>>>>> To view this discussion on the web visit https://groups.goo= gle.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40g= ooglegroups.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 fro= m it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > >> > >>>>> > > >> > >>>>> To view this discussion on the web visit https://groups.goog= le.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHM= oR9oTQOmMw%40mail.gmail.com. > > >> > >>>>> > > >> > >>>>> > > >> > >>>>> For more options, visit https://groups.google.com/d/optout. > > >> > >>> > > >> > >>> -- > > >> > >>> You received this message because you are subscribed to the Go= ogle 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%2BoXRLhsN3O7uXCh3D%2BSfBSsr-h= mwRsr1iwztPg%40mail.gmail.com. > > >> > >>> For more options, visit https://groups.google.com/d/optout. > > >> > > >> -- > > >> You received this message because you are subscribed to the Google G= roups "Homotopy Type Theory" group. > > >> To unsubscribe from this group and stop receiving emails from it, se= nd an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > >> To view this discussion on the web visit https://groups.google.com/d= /msgid/HomotopyTypeTheory/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW= 62bO5L3A%40mail.gmail.com. > > >> For more options, visit https://groups.google.com/d/optout. > > > > -- > > You received this message because you are subscribed to the Google Grou= ps "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/ms= gid/HomotopyTypeTheory/CAH52Xb0XD3F9%3DXc2eHZDAyFHQ-3e%2BHUXc7kRTp_%2BvhzBP= Vx-8g%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/CAH52Xb0v2jbutOG7bfgroYn%2B3HdD_rWtz9BC505fH1NdpnLzrQ%40= mail.gmail.com. For more options, visit https://groups.google.com/d/optout.