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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pl1-x63d.google.com (mail-pl1-x63d.google.com [IPv6:2607:f8b0:4864:20::63d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 30502978 for ; Tue, 4 Jun 2019 20:32:32 +0000 (UTC) Received: by mail-pl1-x63d.google.com with SMTP id a5sf14695443pla.3 for ; Tue, 04 Jun 2019 13:32:32 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1559680351; cv=pass; d=google.com; s=arc-20160816; b=q3+JR3LbzQvuTc9FE25lyAo7GDjQ7B4ljj0uxJI1yvneJ8/6VQ0rnnQneivUjYxNwh MXKU4i7ulZj5MDh+YwjRptSGfl2dACU7DDiDHvGA1IchMHLSrBeiXRPz8hRwP/VBh3lz O4FWWDnPfvJRhELLYO4aYTQRGSjG+4hF7MkpqGveEfetbamnMcQAucL6v9aalv2YOK8m ZzNAtKRQqTJ0Zz+4S18yMTXdRmfZVGxovsMrcSlpzN+GpEwIWTnOB/+G/HUw2HvKC2aQ SAESQGx27mi3a+vcpe6G+IaDRCELFeaUcZVVSRFwh1WjVvMYucsFz6iA1LozjDnjtpbc oH0A== 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; bh=IiKBBjcHT4lqIrLukuV6/cU8kYAZ4aIMHEWTvtDRkEs=; b=Fr9HLmf3mpCcNfhmTLCqy9E1jj1vK7iKGdi6dWAIVuW1pspDfz4NYuCM5DQ1xIaPFO t5QZVaKCQa3cDlCbRYM3pQVUIWOnpmoqQCJD45LpHFbmA67lG9B51UdToVArKyPVNG46 NmM4bGvYC3BrVRVV3auoh/BmGvdRugJCkyBZE6LgZQVnYDfkHkrMIH34eTqFXwh5c4tz zdBXKWcbSE1PZlRNajmmOwLq+af2rqojZSGwGQuYd1jZNYotu3TjjzLeCiEDH+IUxt6L GnR/QylFOL/FANs3U1dRKgV1S2pRkl8mkT2iP3EVawvlA43W2OPf+5aT/CAbHRQDTBKk ZgKg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=xX14CFAB; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c35 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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=IiKBBjcHT4lqIrLukuV6/cU8kYAZ4aIMHEWTvtDRkEs=; b=torv5Alf+YZFuuzBo6WvxyIGSHMyhFvv6ze0M1EL3bWkuuS2nCfngYJIG2lLI2VSOq 1lGN7XEoJHtlUZDR8Mt7TQUM+0psgRfmoFNxcgDuNDhDL6bhm2nuprb+bYDckcFQuKsd YO5F31SIOHHjn+RdLlM4zj+2Vq2ATortFfAjW+aGOLAdaoHqYBBrW3sBjL1A1Vpez25P 7x9eR1iZ72VIxTlwBJkZGUTjgXkjKCCtJ+vm8pkS2bnda+iU7eNP24H0HZ/Bl/16n0fx Ryv/s7hP5RvWGYVz6qac3gZZG9gFq/TnYZ9JEqUdjkk8/Hws/Uhz2fo/TmXBzF7AQn6N NZ4Q== 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=IiKBBjcHT4lqIrLukuV6/cU8kYAZ4aIMHEWTvtDRkEs=; b=AvRko9wwWM4MU5dmbsWYqZ9QMo0LI7wceI/SrTmUpDraeCNladRnTZl4p+8NTs4Czm URSPFhlTRkVHpy761WVRibhJRB0ZTmclzh0RY3BWvFrlgNFnQ/QgmL9szsD86fAH7xyG mUNQ8FQjkj2AbIXVccGeIubVjuakU9Mr/8ZSn0iDhB/CwsVUlaVO5dEYJATxYJALevg6 w+t6MGlxR0pfsNqrmJP7csE+5gh1WNUJ1IsQWUtIP8HXkcJjZVWqrk0YlWeJmG13Mzay x5IFx+yCSnlThhqQbRG+E1ewNW4PFBZZzF6eD1nvKI6KTZDTnWO4RjQ0sk/qzETfYB9h +LDA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUeNTftK7p1icBDNUEX81Eu7ewmJiiCQvymVxG8LonUYrLqYUtU LQkQFyvlcau3Svw73AYyLuo= X-Google-Smtp-Source: APXvYqzALwFCTOmZ/C2VlU1GsIXB6/yWl8pwrSpH/67Kh4pI3+GkHC+iPZ6sqUTq+0aEvME8F78Ugg== X-Received: by 2002:a62:e917:: with SMTP id j23mr35726951pfh.55.1559680350729; Tue, 04 Jun 2019 13:32:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:36cc:: with SMTP id d195ls4556176pga.6.gmail; Tue, 04 Jun 2019 13:32:30 -0700 (PDT) X-Received: by 2002:a65:4c4b:: with SMTP id l11mr549794pgr.9.1559680350277; Tue, 04 Jun 2019 13:32:30 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1559680350; cv=none; d=google.com; s=arc-20160816; b=J1amgObXtUVpFN2scR1eK21FtrtuugZTm+BXmgpSPaZsrRywaQmJrIjyQKuG3OmEIc MrpNty+9xYXvl69Vuc473nLd2en8DFlzrHPjmU5lcJ+MXPVThK/OT4DZCPbY4t0NESg/ EuEF5wf9xRaaYd+1PtI27wsOU9OHrmQqppEpou/HbXYw968d6GUvixm0BedViYl/NxXa 24oUATwfhPBNUDb1pHShsjYBRC9pWa0tE5yeEiQwsDjSEx89gEi8G+JaAFhplG50/tRx pBUrbmzUDsSAS51lioNvdY73Pg1aoHveB7KxJS/8I0qID6GYkZN4VGsHNe4EeeqcEZo+ QDKQ== 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=sA4/WT8514o6nnyf9W27zZwPf1sNEK2aMeVVQh4ycGQ=; b=D7Q11A95GRNaMDIIX+3h2ygQMiWzR0xCFHrsLVXcxGzRRVzQB/Mq973doueOjDnJFl pRqPCxkCj7knht8nSz6dMgwbCs+IRAEsZRfZW5zJdo8+hT89udGDaToDQgycE9l5n7T5 FIOOw5qMWIXmoEaR0OMAnToDqC3b4uYHurLZP7qXyCBDmZyQO+MRYtcMheyqNOejyZPO 7w1DILGf+Yu5kUQTVZEG4kfPIE12WGWY0QUBw8ACH6OP9Bk6DeHiU6wCdpXZL46wIgsB An3iP6Yet7zQQZhyO0LkUy1Z3eRC+6pE2TPWyBdgbonFa+E214XEnzz3h3H2iJ8u7xoV ZmoQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=xX14CFAB; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c35 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc35.google.com (mail-yw1-xc35.google.com. [2607:f8b0:4864:20::c35]) by gmr-mx.google.com with ESMTPS id y13si355574pfl.3.2019.06.04.13.32.30 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Tue, 04 Jun 2019 13:32:30 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c35 as permitted sender) client-ip=2607:f8b0:4864:20::c35; Received: by mail-yw1-xc35.google.com with SMTP id k8so4548473ywh.0 for ; Tue, 04 Jun 2019 13:32:30 -0700 (PDT) X-Received: by 2002:a81:3c83:: with SMTP id j125mr19334245ywa.226.1559680349295; Tue, 04 Jun 2019 13:32:29 -0700 (PDT) Received: from mail-yb1-f176.google.com (mail-yb1-f176.google.com. [209.85.219.176]) by smtp.gmail.com with ESMTPSA id 207sm4873257ywo.98.2019.06.04.13.32.27 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Tue, 04 Jun 2019 13:32:27 -0700 (PDT) Received: by mail-yb1-f176.google.com with SMTP id g62so8466745ybg.7 for ; Tue, 04 Jun 2019 13:32:27 -0700 (PDT) X-Received: by 2002:a25:81d2:: with SMTP id n18mr9207995ybm.223.1559680347167; Tue, 04 Jun 2019 13:32:27 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> In-Reply-To: From: Michael Shulman Date: Tue, 4 Jun 2019 13:32:14 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Kevin Buzzard Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=xX14CFAB; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c35 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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 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 w= rote: > > On Sun, 2 Jun 2019 at 17:30, Bas Spitters wrot= e: > > > > Dear Kevin, > > > > Looking at your slides from big proof, the transfer package you're aski= ng for seems to be very close to what is provided by HoTT. > > https://xenaproject.wordpress.com/2019/06/02/equality-part-3-canonical-= isomorphism/ > > This is explained in many places (e.g. the book). Here's an early artic= le explaining it for algebraic structures: > > http://www.cse.chalmers.se/~nad/publications/coquand-danielsson-isomorp= hism-is-equality.pdf > > > > Have you looked at any of this? Does it provide what you are looking fo= r? > > 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 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 caref= ul > >> > 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 (man= y thanks to all the people who replied) that dependent type theory + impred= icative 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 m= ore suited to mathematics, written by someone who knows what they're doing = (de Moura). Using nonconstructive maths e.g. LEM or AC etc in Lean 3 is jus= t a matter of writing some incantation at the top of a file and then not th= inking about it any more. HoTT might be more appropriate for mathematics --= or at least for some kinds of mathematics -- but its implementation in an = actual piece of software seems a bit more hacky at this point ("use Coq, bu= t don't use these commands or these tactics"), which maybe raises the entry= barrier for mathematicians a bit (and speaking from personal experience, a= lready this entry barrier is quite high). High level tactics are absolutely= crucial for mathematical Lean users. This is one of the reasons that the L= ean documentation is not ideal for mathematicians -- mathematicians need ve= ry early on to be able to use tactics such as `ring` or `norm_num` to do ca= lculations 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 possib= le I am becoming convinced that it can really change mathematics. In my exp= erience the biggest obstruction to it changing mathematics is simply that m= athematicians do not see the point of it, or what it has to offer a modern = working mathematician; they can see no immediate benefits in learning how t= his stuff works. In short, I think type theory has an image problem. Sure t= here are category theorists who know about it, but how many category theori= sts are there in an average maths department? In the UK at least, the answe= r is "much less than 1", and I cannot see that changing any time soon. I wo= uld love to draw the mathematics and computer science communities closer to= gether over ideas like this, but it's hard work. I am wondering whether dev= eloping accessible databases of undergraduate level mathematics would at le= ast make mathematicians sit up and take notice, but when I look at what has= been done in these various systems I do not see this occurring. This weeke= nd I've learnt something about UniMath, but whilst it might do bicategories= very well (which are not on our undergraduate curriculum), where is the ba= sic analysis? Where is the stuff which draws mathematicians in? This by no = means a criticism of unimath -- it is in fact a far more broad criticism of= all of the systems out there. Lean 3 might have schemes but they still can= 't prove that the derivative of sin is cos, and Isabelle/HOL might never ha= ve schemes. I know that Gonthier and his coauthors had to make a lot of und= ergraduate level maths (Galois theory, algebraic number theory, group theor= y) when formalising the odd order theorem in Coq, but it turns out that the= odd order theorem is perhaps not a good "selling point" for mathematics fo= rmalisation when you're trying to sell to "normal research mathematicians",= and I don't know what is. I'm now wondering making formalised undergraduat= e mathematics more accessible to untrained mathematicians is a better appro= ach, but who knows. Obviously "AI which can solve the Riemann hypothesis" w= ill 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 bu= nch of extremely smart people, both mathematicians and computer scientists,= have invested a lot of time in thinking about how to do mathematics with t= ype theory. I find it very frustrating that mathematicians are not beginnin= g to notice. Of course there are exceptions. One day though -- will there s= imply be a gigantic wave which crashes through mathematics and forces mathe= maticians to sit up and take notice? I guess we simply do not know, but if = there is, I hope I'm still around. > >> > > > >> > > Kevin > >> > > > >> > > > >> > > > >> > > On Sun, 26 May 2019 at 06:50, Bas Spitters wrote: > >> > >> > >> > >> There has been progress in making a cleaner interface with the st= andard Coq tactics. (Some abstractions were broken at the ocaml level) > >> > >> I'm hopeful that this can be lead to a clean connection between t= he HoTT library and more of the Coq developments in the not too distant fut= ure. > >> > >> 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 c= onnection 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, ther= e'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 cu= rrently published in the Annals. > >> > >> > >> > >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder w= rote: > >> > >>> > >> > >>> UniMath vs HoTT wasn=E2=80=99t exactly my point, UniMath =3D Boo= k-HoTT is of a category from =E2=80=9CCoq with the indices-matter option pl= us the HoTT library." =E2=80=9CCoq with the indices-matter option plus th= e HoTT 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 c= an do in Coq are broken by using the "indices-matter" option and relatedly = not using the built-in type Prop. Quoting from https://arxiv.org/abs/1610.= 04591 "This small change makes the whole standard library unusable, and man= y 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* tact= ics are available in Coq+indices-matter+HoTT, but not many of the more adva= nced ones, and to my knowledge, not tactics needed for complicated homotopi= cal 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 as= sumed k even if you used the without-k option, and HITs were put in by a ha= ck that wasn't totally clear if it worked, etc.) So I'm likely wrong in so= me 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 doe= s catch up some of the pain points involving transporting from my previous = email should go away automatically. (Side comment: once you start talking = about transporting stuff related to categories across equivalences of categ= ories it's only going to get more painful in ordinary type theory, but will= remain easy in HoTT approaches.) > >> > >>> > >> > >>> Best, > >> > >>> > >> > >>> Noah > >> > >>> > >> > >>> p.s. Installed Lean last week. Looking forward to using it next= year when Scott and I are both at MSRI. > >> > >>> > >> > >>> On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard wrote: > >> > >>>> > >> > >>>> Hi Noah. Thank you for pointing out the category error. It seem= s to me that sometimes when I say "HoTT" I should be saying, for example, "= UniMath". > >> > >>>> > >> > >>>> Tactics in Lean are absolutely crucial for library development.= Coq has some really powerful tactics, right? UniMath can use those tactics= , presumably? > >> > >>>> > >> > >>>> I understand that UniMath, as implemented in Coq, takes Coq and= adds some "rules" of the form "you can't use this functionality" and also = adds at least one new axiom (univalence). > >> > >>>> > >> > >>>> On Sat, 25 May 2019 at 15:50, Noah Snyder w= rote: > >> > >>>>> > >> > >>>>> I=E2=80=99d also imagine that a =E2=80=9Cpractical=E2=80=9D im= plementation would likely have some kind of =E2=80=9Ctwo-level=E2=80=9D typ= e theory where you can use types that behave classically when that=E2=80=99= s 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 "fai= thfully", 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 ty= pe theory this is going to involve annoying book-keeping which it seems lik= e 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 on= e too, as far as mathematicians are concerned, because when you tell a math= ematician "well this ring R is Cohen-Macauley, and here's a ring S which is= isomorphic to R, but we cannot immediately deduce in Lean that S is Cohen-= Macauley" then they begin to question what kind of crazy system you are usi= ng which cannot deduce this immediately. As an interesting experiment, find= your favourite mathematician, preferably one who does not know what a Cohe= n-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 w= ill be very confident that this is true, even if they do not know the defin= ition; 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 m= ake 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 fo= r "the way mathematicians think". However now I've looked over what has cur= rently been formalised in UniMath I am wondering whether there are pain poi= nts for it, which Lean manages to get over more easily. That is somehow whe= re I'm coming from. > >> > >>>> > >> > >>>>> > >> > >>>>> For example, say you have a theorem about bimodules over semi= simple rings whose proof starts =E2=80=9Cwlog, by Artin-Wedderburn, we can = 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 Lean?= If not, that=E2=80=99s somewhere that down the line HoTT might make thing= s more practical. > >> > >>>> > >> > >>>> > >> > >>>> This is a great example! To be honest I am slightly confused ab= out why we are not running into this sort of thing already. As far as I can= see this would be a great test case for the (still very much under develop= ment) 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 assi= stant. > >> > >>>>> > >> > >>>>> 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 t= he "additivity axiom". Please let me know if the following formulation of = 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 cohom= ology > >> > >>>>>>> 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 generally= about a project of formalising many of the statements of modern pure mathe= matics in an arbitrary system, such as HoTT. I know enough about the formal= isation process to know that whatever system one chooses, there will be pai= n points, because some mathematical ideas fit more readily into some founda= tional systems than others. > >> > >>>>>>> > > >> > >>>>>>> > I have seen enough of Lean to become convinced that the pa= in 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 mo= dern pure mathematics, although it is clearly suitable for some of it; howe= ver it seems that simple type theory struggles to handle things like tensor= products of sheaves of modules on a scheme, because sheaves are dependent = types and it seems that one cannot use Isabelle's typeclass system to handl= e 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 = blessing and a curse. However I would like to know more details. I am speak= ing at the Big Proof conference in Edinburgh this coming Wednesday on the p= ain points involved with formalising mathematical objects in dependent type= theory and during the preparation of my talk I began to wonder what the an= alogous picture was with HoTT. > >> > >>>>>>> > > >> > >>>>>>> > Everyone will have a different interpretation of "modern p= ure mathematics" so to fix our ideas, let me say that for the purposes of t= his discussion, "modern pure mathematics" means the statements of the theor= ems publishsed by the Annals of Mathematics over the last few years, 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, 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 essenti= al -- I am only interested in the hard-core "classical mathematician" stanc= e of the way mathematics works, and what it is. > >> > >>>>>>> > > >> > >>>>>>> > If this is not the right forum for this question, I would = be happily directed to somewhere more suitable. After spending 10 minutes f= ailing to get onto ##hott on freenode ("you need to be identified with serv= ices") I decided it was easier just to ask here. If people want to chat dir= ectly I am usually around at https://leanprover.zulipchat.com/ (registratio= n required, full names are usually used, I'll start a HoTT thread in #mathe= matics). > >> > >>>>>>> > > >> > >>>>>>> > Kevin Buzzard > >> > >>>>>>> > > >> > >>>>>>> > -- > >> > >>>>>>> > You received this message because you are subscribed to th= e Google Groups "Homotopy Type Theory" group. > >> > >>>>>>> > To unsubscribe from this group and stop receiving emails f= rom it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > >> > >>>>>>> > To view this discussion on the web visit https://groups.go= ogle.com/d/msgid/HomotopyTypeTheory/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40= googlegroups.com. > >> > >>>>>>> > For more options, visit https://groups.google.com/d/optout= . > >> > >>>>>>> > >> > >>>>>> -- > >> > >>>>>> You received this message because you are subscribed to the G= oogle 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.googl= e.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40goo= glegroups.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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR= 9oTQOmMw%40mail.gmail.com. > >> > >>>>> > >> > >>>>> > >> > >>>>> For more options, visit https://groups.google.com/d/optout. > >> > >>> > >> > >>> -- > >> > >>> You received this message because you are subscribed to the Goog= le 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.c= om/d/msgid/HomotopyTypeTheory/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmw= Rsr1iwztPg%40mail.gmail.com. > >> > >>> For more options, visit https://groups.google.com/d/optout. > >> > >> -- > >> You received this message because you are subscribed to the Google Gro= ups "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/m= sgid/HomotopyTypeTheory/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62= bO5L3A%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/msgi= d/HomotopyTypeTheory/CAH52Xb0XD3F9%3DXc2eHZDAyFHQ-3e%2BHUXc7kRTp_%2BvhzBPVx= -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/CAOvivQzFBjtA33McF1nAerfcnFRbnWLAw73-F3GPBumbVqetag%40ma= il.gmail.com. For more options, visit https://groups.google.com/d/optout.