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.2 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-x237.google.com (mail-lj1-x237.google.com [IPv6:2a00:1450:4864:20::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 78ea5fca for ; Sat, 25 May 2019 13:13:30 +0000 (UTC) Received: by mail-lj1-x237.google.com with SMTP id g8sf2317156lja.12 for ; Sat, 25 May 2019 06:13:30 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558790010; cv=pass; d=google.com; s=arc-20160816; b=X3GRuccwJCDGELG2H9WiLeBiT0IwwwMYDr1t101OOCaCo3nVs8wL2CtfyoSrO6HKEJ 2v+rNX59UMvR7RG58kgYPdIRKRcTwdEHy8jGVZFBzbIaX8wRsTizONRUafZv6MtoakmN Vd3IYsr2M//T8NxO2Nk+Q2y/84deN0/P1hmmWzUrTSPUPnZunY4BNzqPeYp8zXTMQ62x OePBA1uyHVQHkA4NtxdgT+NmF8MFsTEobubAyuIjQqocj2djd2NavxTJOhuv8FvpqLpY Xo0wGkpvRNJkpQ+9+ArWJ+IBGGRs81RdESrH+FBsfP+bgoPGE8W8RNt3nxPv1T8IKnDa QF6A== 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:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature:dkim-signature; bh=MsO5GmQBoDpLA/DIiVtM2SWTmP4R7J7uYzgN/rRE32I=; b=U7BbmGP35te5mFzFkp6O5HcJ7flu6o9LeUL9mLPCpBTmoknqnsmcspEUVz2Ua4BuBg VzGBeQe3Hx3jpuKXHnDzDUQjxu3YXodL9Gb0/3XcNhaQvBgxIMAGT4bhGm5eOv2l6kXG /j/19AT5J6WDCa08A7aI94DcAsba0ojub7ZloXVFYJAUJ08iHedxgm+I/WVLCqRs3SDa OquhDNDjnLcexSEi31udJFCBGy+D0LTbHJGi39mwjko0HzanHhqf1x/4mj1Vc2JTBvRc gjwwykdY26ILfY8gpbTsIifZtXFf3I+Mt2Qgc7yuE6rv4HT3xjysJbdzJCNX+wx8vRja zajA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=dNYreS5+; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22c 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=MsO5GmQBoDpLA/DIiVtM2SWTmP4R7J7uYzgN/rRE32I=; b=T5e4YUaaznBnC2sogAG/N8I6Kxb8AsW4oHfe2rO6fYHhTPmli5ASIWAcA1QwZB/2mN ccLDpCg6rJ+/bdc71+PwR2pusR2Cp9vmmnR86yjw3QjV4em1TSdbvILKU8JK0Wd1eaaT 6zIM76tUnvMzRT2ku9xgN4I3xB5RXl2LJZj0ZK04NBYs08Nvx1sJChuojh0S75qKH/aj SH4mV+k2Rb9G5mETznV/wXhmE6DjOHwsOc6DeCaPqkx4gvoprRocuwT+Ext5KKN5vyd6 IJH9Yari8aVY/SpVLIQORcq8INzw6Bd1lCMo+Z+F/hPcatYPrbOqV3NROuR1ezYJkP2c NRYQ== 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 :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=MsO5GmQBoDpLA/DIiVtM2SWTmP4R7J7uYzgN/rRE32I=; b=gWXNklmiWvANwRUFlWgOvfGfZQQr7LXaQaB2MkHRR9VNyc/2yyXlg+hE602Dhm5RdB KCFWxYqriUU+2juYoIjKBXaMemp1W6osyn2+e0jQe+tBXWpa7KslmLomyXz2r0zEI79/ Ey3AA9Skkk9kuIEkEn1pb3m5h9Gx7colsoSWKNo59SKibjuy2uHyGajsUFsVEMpXM8iM HPGWM5m5yZlXPk1H4m1UPFMzeV90wuY2eq8iGGSWIuJYzu5+nItmL2C315nHCHCmQ7Vm ROndfkXOIfPB7THS2CWEvj3oskUc1jm0ECpizoQ+K2AiFtQQ36juT4ekd9/LPwIa6uTm pYwg== 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: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=MsO5GmQBoDpLA/DIiVtM2SWTmP4R7J7uYzgN/rRE32I=; b=UUCyk9aSl2jEqLakZuiWyA3/KFoSbK+leREVFIu/FnD1PsGfZTlrGDZngvsk3My122 57HTkA3XLW0DnEBDxRnJWEwGudLpaPx8Zsgxa5B8Uc3I4A/TdAl581UGYaT2CYXnqAmB y5YBsrY4ZF2ZTzNDmUYlczUSJ8qrUFKvzZxjSW9YnWagZ9Lgg/ecjKPhzKOITrBWk5lp yABb8nRamafIArCQqjGMTOf+XEA1w1JXHs3OU4GJzgU1SHUhtwXY1uJnOa/Xh09CLgoE 6yI8FrGJxhCh8tCeJ7aiWFjMXyKuUNhGfk4u/6u4y4MSVzdCMndIY7dwVl/RHqABTMNc t4Nw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWum1hkL5LTvqH68WlhcvMjlGHLGYWDZiNdQY4lZSzWjZvXj5fR TPf6lSf/NxqVQHDCY1P/7xc= X-Google-Smtp-Source: APXvYqyzvGSnhx/dXURJjA1tsR9EAJ8iKXr66XWSjIbcNVt5+6lf+lcS9oQJULC6dQ0L/lIttjwwlg== X-Received: by 2002:a19:6a08:: with SMTP id u8mr26445775lfu.143.1558790010234; Sat, 25 May 2019 06:13:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:651a:: with SMTP id z26ls1354994ljb.1.gmail; Sat, 25 May 2019 06:13:29 -0700 (PDT) X-Received: by 2002:a2e:914d:: with SMTP id q13mr35093177ljg.140.1558790009586; Sat, 25 May 2019 06:13:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558790009; cv=none; d=google.com; s=arc-20160816; b=q+5c1BbwmK1w9s5lygXHQQcAAZ/uz9ZAGHeiFHj4m9GFgA8V11Gazzc9zGv0ezuAle Ym1A8BeW7uMefRmxAFU1hN6TA+8Bp5D6DpvPonE8qI/qIKDqpfd6WpeTsSXx/Nct4JNy YiVAAYv0qXXqh2XPonvOidqoCelRuaAJ+noeX/x0jp44rq19xI3fH7ngAbONF3ff1+oZ RiU2L09+u2uVgOLlobxlGayjOsWU4LBWiUudnHYYLMGrNwF1IdJXutAPQvK7iilXYzM6 Stnh1K2ui/vK42POiqCqa0fZjWXdBvrrLv4RVgDiljimXePgeMYe9zWQrbp59Z+8OX4c yT/g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=4H3Wq1QM1alpAbkMreXg8hJM8jYRRfAhpPF3XW+zzcU=; b=cztRDXfrLcIHgRgCfxZwbgN4RH9fMu6RKJqodCB/yISlmZSS22LQmQlD9lTyJ3EwxB Q9JEZPFlXrzBHwbHwvyopadPmFcMI0jKmUmt/a5syHqnFaNISfIPbD0ZKH+2J1UqYVQB aapNE5jpPTroW+WHRHQtWda8dscmUaV/T6FoMTOtw4wqE31ZVcy3/uLoBL94PpcSuoty Kj8PV9wesOhW0oC2LvgzWaEQDG+lSKywalNUgJ5PWC2GiyC/agbXv/5/l5QovbFnbOBH a8NZqY/wm7qmEyLnBYMDvFrSl6qZMGQ0ZAqyAcY/BcBae/QyJw8AcyLC3BU2w1k38wV5 iMJw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=dNYreS5+; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22c 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-x22c.google.com (mail-lj1-x22c.google.com. [2a00:1450:4864:20::22c]) by gmr-mx.google.com with ESMTPS id h3si342812lfm.3.2019.05.25.06.13.29 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 25 May 2019 06:13:29 -0700 (PDT) Received-SPF: pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22c as permitted sender) client-ip=2a00:1450:4864:20::22c; Received: by mail-lj1-x22c.google.com with SMTP id h19so2590212ljj.4 for ; Sat, 25 May 2019 06:13:29 -0700 (PDT) X-Received: by 2002:a2e:6817:: with SMTP id c23mr33161429lja.145.1558790009036; Sat, 25 May 2019 06:13:29 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Kevin Buzzard Date: Sat, 25 May 2019 14:13:11 +0100 Message-ID: Subject: Fwd: [HoTT] doing "all of pure mathematics" in type theory To: 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=dNYreS5+; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::22c 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 Sat, 25 May 2019 at 12:26, Thierry Coquand w= rote: > > > Some further references: > > - the UniMath library > > https://github.com/UniMath/UniMath/blob/master/UniMath/CONTENTS.md > (in particular representation of the notion of triangulated categories) Aah. So I think my question is this. The maths library for the Lean theorem prover has a bunch of MSc level algebra (localisations, completions, Noetherian rings), undergraduate level topology, but it is just beginning to develop a reasonable undergraduate level analysis library. Analysis has gone much more slowly than algebra because for some reason a bunch of complicated design decisions about partial functions had to be made, and e.g. people are still trying to figure out the best way to formalise manifolds. Lean also seems to find unbundled structures easier to work with than bundled structures, so whilst there is some category theory, it hasn't really yet found an application. I am hoping to integrate it into the work on schemes which is being done but somehow things keep being easier without it. So somehow currently the pain points seem to be getting category theory to work nicely (although this might be solvable if we try harder) and generally trying to work out how mathematicians use partial functions when talking about calculus and manifolds. I am unclear about whether these are issues intrinsic to the system or whether we are just not smart enough to know how to work the system. Conversely, in Isabelle/HOL doing real analysis is a dream, they have extensive real analysis libraries; the pain point that Lean has or might have simply isn't there, apparently. But doing schemes is painful in Isabelle/HOL, because sheaves of rings mean manipulating things which are rings, but without the typeclass system. Looking at UniMath I see a *huge* amount of category theory stuff. Then for algebra I see rings and modules, and there are things like the reals and the p-adics. What about schemes? Have people formalised schemes in UniMath? We ran into issues in Lean which needed solutions, but the pain points were just ignorance on our part (I'm a mathematician, and I needed to learn what type theory was). Real analysis seems to be easier to do in simple type theory than Lean's dependent type theory. How would this look in UniMath? This viewpoint that a type is a "space" rather than a "set" -- it's going to make some things easier, and some things harder. What does it make harder? Because propositions are subsingletons in Lean, and equality is a proposition, types have a much more set-ish feel to them. > > -Voevodsky=E2=80=99s paper > > https://www.cambridge.org/core/services/aop-cambridge-core/content/view/= S0960129514000577 Voevodsky says in this paper "we come to the view that not only homotopy theory but the whole of Mathematics is the study of structures on homotopy types". On the other hand, if you talk to someone like Larry Paulson, he would tell you that simple type theory is enough to do all (pure) mathematics, and if you talk to one of the set theorists in Berkeley they would no doubt tell you that ZFC set theory is enough to do all mathematics, except for perhaps some bits where it's more convenient to have some large cardinals. All of these views are correct in some sense, but they are all hiding the fact that actually *some* mathematics is quite hard to do in the system preferred by one person, and turns out to be much easier if it's done in one of the other systems. For example schemes are relatively painless in Lean's dependent type theory, but would be painful in Isabelle/HOL. On the other hand real analysis is relatively painless in Isabelle/HOL and yet in Lean we still have not proved that the derivative of sin is cos. How does UniMath fit into all this? There are clearly things which could be done in UniMath but which have not been done. But why have they not been done? Is it just a matter of time, or are there things which are actually going to be *hard* to do in UniMath's foundations and doing in them in, say, ZFC or another kind of type theory would be much easier? Kevin > > - The paper https://lmcs.episciences.org/4814/pdf > contains a presentation of the categorical semantics of type theory using= univalence; > Section 2.3 discusses some differences between the =E2=80=9Cclassical=E2= =80=9D approach to representation of structures > and the approach in the univalent setting. > > The system is compatible with classical logic and choice (but this has n= ot been needed in these examples). > > Best regards, > Thierry > > > > On 25 May 2019, at 12:22, Steve Awodey wrote: > > A useful example for you might be Floris van Doorn=E2=80=99s formalizatio= n of > the Atiyah-Hirzebruch and Serre spectral sequences for cohomology > in HoTT using Lean: > > https://arxiv.org/abs/1808.10690 > > Regards, > > Steve > > On May 25, 2019, at 12:12 PM, Kevin Buzzard w= rote: > > 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 m= odern pure mathematics in Lean. One could ask more generally about a projec= t of formalising many of the statements of modern pure mathematics in an ar= bitrary system, such as HoTT. I know enough about the formalisation process= to know that whatever system one chooses, there will be pain points, becau= se some mathematical ideas fit more readily into some foundational systems = than others. > > I have seen enough of Lean to become convinced that the pain points would= be surmountable in Lean. I have seen enough of Isabelle/HOL to become skep= tical about the idea that it would be suitable for all of modern pure mathe= matics, although it is clearly suitable for some of it; however it seems th= at simple type theory struggles to handle things like tensor products of sh= eaves of modules on a scheme, because sheaves are dependent types and it se= ems that one cannot use Isabelle's typeclass system to handle the rings sho= wing 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 speaking at the Big = Proof conference in Edinburgh this coming Wednesday on the pain points invo= lved with formalising mathematical objects in dependent type theory and dur= ing 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 theorems publishsed = by the Annals of Mathematics over the last few years, so for example I am t= alking about formalising statements of theorems involving L-functions of ab= elian varieties over number fields, Hodge theory, cohomology of algebraic v= arieties, 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 . Cl= assical logic and the axiom of choice are absolutely essential -- I am only= interested in the hard-core "classical mathematician" stance of the way ma= thematics works, and what it is. > > If this is not the right forum for this question, I would be happily dire= cted to somewhere more suitable. After spending 10 minutes failing to get o= nto ##hott on freenode ("you need to be identified with services") I decide= d it was easier just to ask here. If people want to chat directly I am usua= lly around at https://leanprover.zulipchat.com/ (registration required, ful= l names are usually used, I'll start a HoTT thread in #mathematics). > > Kevin Buzzard > > -- > You received this message because you are subscribed to the Google Groups= "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.co= m. > 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/BFBE1A09-A246-4DAD-8AD2-25C3C517A7FE%40cmu.edu. > 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/CAH52Xb0EK8xf1d6Oq9AgAcnjenu4Nhu7H7VcvDWToMpVKVtCog%40ma= il.gmail.com. For more options, visit https://groups.google.com/d/optout.