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-wr1-x43d.google.com (mail-wr1-x43d.google.com [IPv6:2a00:1450:4864:20::43d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 01dd553e for ; Sun, 2 Jun 2019 17:56:04 +0000 (UTC) Received: by mail-wr1-x43d.google.com with SMTP id b19sf7224719wrh.17 for ; Sun, 02 Jun 2019 10:56:04 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1559498164; cv=pass; d=google.com; s=arc-20160816; b=HFp31gbO+1aJRLyI73aY0hLIwd47cDvIj8D2813skB2OZ+to5W6mHe0MBkn7kOCp3k 1phem00OhfYy4QbeUfqTdWQMy5iWbDgQa5rz2hXQa+sK3/uvBERpi3YxdoCutxHr/wVm MbNIo+wjLdXGoDGoj6C0itu/eKjXLCvSRPgxqbfnU0G+pJ8nRhI0k4/TmadMSE9nCRQw +g+SfYH16aW9Doz7aES0w/HJnQr4HWyTN4tIT+IQAhPfEp0+NYp0QlEyt6PIuEP73+Wx fsoX6zTf5GRzW3avrj89//70BbORYzTxNbREyE2bwQjuecTlc+LUnXXcy9jHt7CLlr3a kEvA== 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=c9xFHckLt1L4L+UQ2Iy7sBaqLc8xGdP8gZNbLZIF3Rg=; b=fwQIez/i0IN5KbQDxqD4NZs/igTAAD6wNjL5YVQOPXuro6cZ+vD+6wr08ePsHh7v2m q3vEHEjNzPr8r4WtaBjukvanGiemG9fIsm2NNe0s/8Ue1ndquGk+4ZG7Zdx8Cow040/b EZuQi5zV77RJag4etUJoWXWFSgi2knMBu5l8rhJ6xP/F/wVYOTx6Z9AEeFErQNjGYWop YY+t14mJUexRKjYxtVwCeRvkN6gYK0SZh/6ZImc5U1YjPMsktGV0zuRhUhi9fMOirgMn GimKxluRxaipy3DJikgSNnm/VA+hp+09mepE8yN6RK04A9+Pu+aP8aX0KPjilxowGRlL DHUA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=jECeZuiu; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22b 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=c9xFHckLt1L4L+UQ2Iy7sBaqLc8xGdP8gZNbLZIF3Rg=; b=sRT6kSiYpjLi65lduczsDSHBWJzPGuDNl9whLw4jE7FyormT6mrvJ0qiE3LatUeUb4 sewiancF3RDSiIs+wUio8eb3BCLoMWJHe7C6+ffkSxDciYSzHlHopte+LVwGRYnuQ5si 2GErBoHNE9HeH3VWykAEcg+OJpwx5Gayk1X4/F1kenn8o+ZdFuV6c5qpBaq4uyIwzMMh 4JolPjrVEp5Xk/ZwN+p/dhPAuQUIVkSx4xbT1TlaimU5H1xmiE5IqaBR4Ge8r5PTQ00O kNynmAGJkA0T4oGO4OTEDnHWiMQuEA3aeb9k3qRIKGVle7PwnL1Aa7R73JI2Orielv7K ZT9Q== 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=c9xFHckLt1L4L+UQ2Iy7sBaqLc8xGdP8gZNbLZIF3Rg=; b=CLz0JIV7X21iNvj8H8CjUnCFU5NXv/1l3cEfc++DmDJIkQe0wp9z2rh72rySlg9tvO NKsBI4BGp/WdMI+2cy0clEjMcJ18YQov1eEoimfGDN8pNqrlusEJMOldJD88CyNfO4uu 25UHw+kW62eOxsvGQqZDBhHOP1HbVC/VZBoeLYlG06uTHszn+1aahr684dk/xMBYQ22a PBieYHXUL5uMcFkvVl0KDNnIqnUt8lv0Ed7w+2cFr8UfEHAFX+xbqYhrrxaIX2k6BdSD 2t3GhFmRndQ7o50g64YxbTSasaM60/g9wdlGBJFyRydZE6LQBs/hinJRSXCD2FdhPgDP GeOw== 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=c9xFHckLt1L4L+UQ2Iy7sBaqLc8xGdP8gZNbLZIF3Rg=; b=BeW719t399AyIUJZ9yedOGOlZoM8hCj1950hTGW1F4Vqj3pTYjRuKmE1sjjQtaqz1y HeYpqbYtMfnEPRGpMY7OH9GBJkn/SK6v3fTuaaxhXVpHeILu5qG7s2EYvCKY1l6RTNgv XZZpeY0gwOHMOrAqNqIrOoSfgAOTJf8Ga899uARbO9IknFIeWEwv67GYaCnwFtRy/EuV rf/6E88zZ+Rl5HAcZak4bJQAAhu8MSLxXM7VpjVG3gBuqCFQFrGb5Zh6mclRq40o5gYC 9N1yDML/49WqAQBGhImuXdsVHexlapKpOhxoHgMcwX5qQ0NLC6rpDGYHbpyKD8ppDoMd kgOA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUldrVJUCX6kh7ozPuWH8Rh6zHRsVw5iSUHA3uF8xaH5eEaFAJl ZqLfeyr102/B+NBYxBw9hp8= X-Google-Smtp-Source: APXvYqy96Iya/yOINykrfZDJ4UlaKnsa+1EMlnwb64gLmFMd007mv/fJfjl48LDaKCSmCSwLZMHUHg== X-Received: by 2002:adf:e485:: with SMTP id i5mr1974581wrm.75.1559498163921; Sun, 02 Jun 2019 10:56:03 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:f505:: with SMTP id t5ls1083766wmh.0.canary-gmail; Sun, 02 Jun 2019 10:56:03 -0700 (PDT) X-Received: by 2002:a1c:151:: with SMTP id 78mr5311167wmb.58.1559498163255; Sun, 02 Jun 2019 10:56:03 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1559498163; cv=none; d=google.com; s=arc-20160816; b=fHXtFXawGoh3f6x+BR3k7D71X74I81gkcsjbZT70shktKLHlFDaSN0/eCQi9xn9a7H GSZ/jJ5D5CU1c7WK1+WQOWjcrF1JgS2xKFfPu9CPgIElYKbLE/QlM2HLlKSUQD5TPp0T Is9qse6DDt+U0TRgMTo2m0nO0bqwOJFNy/gM1192CQw0+MJwx6A/YvRm9IEjPW2z9hHX rzXKk5kPPgLAxaQTc6XYL0HmJvrN41MGfhrvuhjjDGKKW5BswZYsygbpr7XLnjJ1ctdp /7LT8RkH6NCX3AI2tXx3Z1otWeF2iLbG4XDU8Cbh5lrGq5AcbSEsuYfcRdkwve59xgR4 y/oQ== 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=4fYeeMUw/jc2X9NE/LpY07X19AYWNTo7UYl88t9/6eU=; b=PAHh+joDbD2ZAYykk0iqV89DxYLF3NwPdlwEfytavIvpc24cPLMVShI4INfZgHTtTr v6QdfPaDvj15iB1g5XiyGPbaZmb7Ap6Pix0Vbfx//kBUmsh8CgkAfog33N+9PZniMkq2 Fo5wqUC4Mh39c9p7PF2PlqhnuHfmX5ZYw4NcGi5R3hNWrioSiTHkDZI/+8ohT1efewUp FE7RRhtJ7c1TGJwQZoJCcxVEW0bepVH06lrFaPvCshoNCK2rTJigz+fwfjbzOYsmR9by Et9sTVmGhYg16T+5JnXBsTRyLio4rCQMiY1YFR5Kr9PuWQ3LqFfUnPz15SO5qwwzbKVa osxQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=jECeZuiu; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22b 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-x22b.google.com (mail-lj1-x22b.google.com. [2a00:1450:4864:20::22b]) by gmr-mx.google.com with ESMTPS id z11si417483wmc.2.2019.06.02.10.56.03 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 02 Jun 2019 10:56:03 -0700 (PDT) Received-SPF: pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22b as permitted sender) client-ip=2a00:1450:4864:20::22b; Received: by mail-lj1-x22b.google.com with SMTP id a10so10835189ljf.6 for ; Sun, 02 Jun 2019 10:56:03 -0700 (PDT) X-Received: by 2002:a2e:6817:: with SMTP id c23mr12301368lja.145.1559498162709; Sun, 02 Jun 2019 10:56:02 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> In-Reply-To: From: Kevin Buzzard Date: Sun, 2 Jun 2019 18:55:45 +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=jECeZuiu; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22b 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: , On Sun, 2 Jun 2019 at 17:30, Bas Spitters wrote: > > Dear Kevin, > > Looking at your slides from big proof, the transfer package you're asking= for seems to be very close to what is provided by HoTT. > https://xenaproject.wordpress.com/2019/06/02/equality-part-3-canonical-is= omorphism/ > This is explained in many places (e.g. the book). Here's an early article= explaining it for algebraic structures: > http://www.cse.chalmers.se/~nad/publications/coquand-danielsson-isomorphi= sm-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 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 wr= ote: >> >> > 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 = thanks to all the people who replied) that dependent type theory + impredic= ative prop "got lucky", in that Coq has been around for a long time, and Le= an 3 is an attempt to model basically the same type theory but in a way mor= e suited to mathematics, written by someone who knows what they're doing (d= e Moura). Using nonconstructive maths e.g. LEM or AC etc in Lean 3 is just = a matter of writing some incantation at the top of a file and then not thin= king about it any more. HoTT might be more appropriate for mathematics -- o= r at least for some kinds of mathematics -- but its implementation in an ac= tual 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 b= arrier for mathematicians a bit (and speaking from personal experience, alr= eady this entry barrier is quite high). High level tactics are absolutely c= rucial for mathematical Lean users. This is one of the reasons that the Lea= n 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 calc= ulations with real numbers or in commutative rings, and these tactics are n= ot even mentioned in the standard Lean documentation. >> > > >> > > I am a working mathematician who two years ago knew nothing about th= is 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 exper= ience the biggest obstruction to it changing mathematics is simply that mat= hematicians do not see the point of it, or what it has to offer a modern wo= rking mathematician; they can see no immediate benefits in learning how thi= s stuff works. In short, I think type theory has an image problem. Sure the= re are category theorists who know about it, but how many category theorist= s are 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 woul= d love to draw the mathematics and computer science communities closer toge= ther over ideas like this, but it's hard work. I am wondering whether devel= oping accessible databases of undergraduate level mathematics would at leas= t make mathematicians sit up and take notice, but when I look at what has b= een 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 v= ery well (which are not on our undergraduate curriculum), where is the basi= c analysis? Where is the stuff which draws mathematicians in? This by no me= ans a criticism of unimath -- it is in fact a far more broad criticism of a= ll 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 have= schemes. I know that Gonthier and his coauthors had to make a lot of under= graduate level maths (Galois theory, algebraic number theory, group theory)= when formalising the odd order theorem in Coq, but it turns out that the o= dd order theorem is perhaps not a good "selling point" for mathematics form= alisation when you're trying to sell to "normal research mathematicians", a= nd I don't know what is. I'm now wondering making formalised undergraduate = mathematics more accessible to untrained mathematicians is a better approac= h, but who knows. Obviously "AI which can solve the Riemann hypothesis" wil= l 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 bunc= h of extremely smart people, both mathematicians and computer scientists, h= ave invested a lot of time in thinking about how to do mathematics with typ= e theory. I find it very frustrating that mathematicians are not beginning = to notice. Of course there are exceptions. One day though -- will there sim= ply be a gigantic wave which crashes through mathematics and forces mathema= ticians to sit up and take notice? I guess we simply do not know, but if th= ere 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 stan= dard 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 futur= e. >> > >> As it exists in agda now. >> > >> >> > >> IIUC, UniMath does not allow any of the standard library or it's ta= ctics, or even record types, since Vladimir wanted to have a very tight con= nection between type theory and it's semantics in simplicial sets. So, I do= n't expect them to connect to other developments, but I could be wrong. >> > >> >> > >> About the bundled/unbundled issue, which also exists in Coq, there'= s some recent progress "frame type theory" which should be applicable to bo= th 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 fo= r sets), seems to be the most natural foundation for mathematics as is curr= ently published in the Annals. >> > >> >> > >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder wro= te: >> > >>> >> > >>> UniMath vs HoTT wasn=E2=80=99t exactly my point, UniMath =3D Book-= HoTT is of a category from =E2=80=9CCoq with the indices-matter option plus= the HoTT library." =E2=80=9CCoq with the indices-matter option plus the = HoTT library" is of the same category as "Lean plus the math library" and t= hen 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 no= t using the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04= 591 "This small change makes the whole standard library unusable, and many = tactics stop working, too. The solution was rather drastic: we ripped out = the standard library and replaced it with a minimal core that is sufficient= for the basic tactics to work." >> > >>> >> > >>> (In particular, I was in error in my previous email, *some* tactic= s are available in Coq+indices-matter+HoTT, but not many of the more advanc= ed ones, and to my knowledge, not tactics needed for complicated homotopica= l calculations.) >> > >>> >> > >>> I should say I've never used Coq, just Agda. (When I was using Ag= da the situation was even worse, things like pattern matching secretly assu= med k even if you used the without-k option, and HITs were put in by a hack= that wasn't totally clear if it worked, etc.) So I'm likely wrong in some= places above. >> > >>> >> > >>> So I think from a practical point of view, =E2=80=9CCoq with the i= ndices-matter option plus the HoTT library" is well behind ordinary Coq (an= d also Lean) for doing ordinary mathematics. However, if and when it does = catch up some of the pain points involving transporting from my previous em= ail should go away automatically. (Side comment: once you start talking ab= out transporting stuff related to categories across equivalences of categor= ies it's only going to get more painful in ordinary type theory, but will r= emain easy in HoTT approaches.) >> > >>> >> > >>> Best, >> > >>> >> > >>> Noah >> > >>> >> > >>> p.s. Installed Lean last week. Looking forward to using it next y= ear 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, "Un= iMath". >> > >>>> >> > >>>> Tactics in Lean are absolutely crucial for library development. C= oq has some really powerful tactics, right? UniMath can use those tactics, = presumably? >> > >>>> >> > >>>> I understand that UniMath, as implemented in Coq, takes Coq and a= dds some "rules" of the form "you can't use this functionality" and also ad= ds at least one new axiom (univalence). >> > >>>> >> > >>>> On Sat, 25 May 2019 at 15:50, Noah Snyder wro= te: >> > >>>>> >> > >>>>> I=E2=80=99d also imagine that a =E2=80=9Cpractical=E2=80=9D impl= ementation would likely have some kind of =E2=80=9Ctwo-level=E2=80=9D type = theory where you can use types that behave classically when that=E2=80=99s = better and HoTT types when that=E2=80=99s better. >> > >>>> >> > >>>> >> > >>>> But plain Coq has such types, right? >> > >>>> >> > >>>> OK so this has all been extremely informative. There are other pr= overs being developed which will implement some flavour of HoTT more "faith= fully", 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 tr= anslate a theorem or construction across the isomorphism. In ordinary type= theory this is going to involve annoying book-keeping which it seems like = you=E2=80=99d have to do separately for each kind of mathematical object. >> > >>>> >> > >>>> >> > >>>> Yes. This is a pain point in Lean. It's a particularly nasty one = too, as far as mathematicians are concerned, because when you tell a mathem= atician "well this ring R is Cohen-Macauley, and here's a ring S which is i= somorphic to R, but we cannot immediately deduce in Lean that S is Cohen-Ma= cauley" then they begin to question what kind of crazy system you are using= which cannot deduce this immediately. As an interesting experiment, find y= our favourite mathematician, preferably one who does not know what a Cohen-= Macauley ring is, and ask them whether they think it will be true that if R= and S are isomorphic rings and R is Cohen-Macauley then S is too. They wil= l be very confident that this is true, even if they do not know the definit= ion; standard mathematical definitions are isomorphism-invariant. This is p= art of our code of conduct, in fact. >> > >>>> >> > >>>> However in Lean I believe that the current plan is to try and mak= e a tactic which will resolve this issue. This has not yet been done, and a= s 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 curre= ntly been formalised in UniMath I am wondering whether there are pain point= s for 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 semisi= mple rings whose proof starts =E2=80=9Cwlog, by Artin-Wedderburn, we can as= sume 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 = more practical. >> > >>>> >> > >>>> >> > >>>> This is a great example! To be honest I am slightly confused abou= t why we are not running into this sort of thing already. As far as I can s= ee this would be a great test case for the (still very much under developme= nt) 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 wi= th automation. >> > >>>> >> > >>>> Kevin >> > >>>> >> > >>>> >> > >>>>> >> > >>>>> But mostly I just want to say you=E2=80=99re making a category e= rror in your question. HoTT is an abstract type theory, not a proof assist= ant. >> > >>>>> >> > >>>>> Best, >> > >>>>> >> > >>>>> Noah >> > >>>>> >> > >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina wrote: >> > >>>>>> >> > >>>>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the= "additivity axiom". Please let me know if the following formulation of th= e 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 f= ormalization of >> > >>>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomol= ogy >> > >>>>>>> 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 p= roject https://formalabstracts.github.io/ wants to formalise many of the st= atements of modern pure mathematics in Lean. One could ask more generally a= bout a project of formalising many of the statements of modern pure mathema= tics in an arbitrary system, such as HoTT. I know enough about the formalis= ation process to know that whatever system one chooses, there will be pain = points, because some mathematical ideas fit more readily into some foundati= onal systems than others. >> > >>>>>>> > >> > >>>>>>> > I have seen enough of Lean to become convinced that the pain= points would be surmountable in Lean. I have seen enough of Isabelle/HOL t= o become skeptical about the idea that it would be suitable for all of mode= rn pure mathematics, although it is clearly suitable for some of it; howeve= r it seems that simple type theory struggles to handle things like tensor p= roducts of sheaves of modules on a scheme, because sheaves are dependent ty= pes 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 t= he fact that "all constructions must be isomorphism-invariant" is both a bl= essing and a curse. However I would like to know more details. I am speakin= g at the Big Proof conference in Edinburgh this coming Wednesday on the pai= n points involved with formalising mathematical objects in dependent type t= heory and during the preparation of my talk I began to wonder what the anal= ogous picture was with HoTT. >> > >>>>>>> > >> > >>>>>>> > Everyone will have a different interpretation of "modern pur= e mathematics" so to fix our ideas, let me say that for the purposes of thi= s discussion, "modern pure mathematics" means the statements of the theorem= s publishsed by the Annals of Mathematics over the last few years, so for e= xample I am talking about formalising statements of theorems involving L-fu= nctions of abelian varieties over number fields, Hodge theory, cohomology o= f algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and t= he like; one can see titles and more at http://annals.math.princeton.edu/20= 19/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= happily directed to somewhere more suitable. After spending 10 minutes fai= ling to get onto ##hott on freenode ("you need to be identified with servic= es") I decided it was easier just to ask here. If people want to chat direc= tly I am usually around at https://leanprover.zulipchat.com/ (registration = required, full names are usually used, I'll start a HoTT thread in #mathema= tics). >> > >>>>>>> > >> > >>>>>>> > 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 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40go= oglegroups.com. >> > >>>>>>> > For more options, visit https://groups.google.com/d/optout. >> > >>>>>>> >> > >>>>>> -- >> > >>>>>> 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googl= egroups.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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9o= TQOmMw%40mail.gmail.com. >> > >>>>> >> > >>>>> >> > >>>>> For more options, visit https://groups.google.com/d/optout. >> > >>> >> > >>> -- >> > >>> You received this message because you are subscribed to the Google= Groups "Homotopy Type Theory" group. >> > >>> To unsubscribe from this group and stop receiving emails from it, = send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> > >>> To view this discussion on the web visit https://groups.google.com= /d/msgid/HomotopyTypeTheory/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRs= r1iwztPg%40mail.gmail.com. >> > >>> For more options, visit https://groups.google.com/d/optout. >> >> -- >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msg= id/HomotopyTypeTheory/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO= 5L3A%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/CAH52Xb0XD3F9%3DXc2eHZDAyFHQ-3e%2BHUXc7kRTp_%2BvhzBPVx-8= g%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.