```
From: Kevin Buzzard <kevin.m.buzzard@gmail.com>
To: Steve Awodey <awodey@cmu.edu>
Cc: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] doing "all of pure mathematics" in type theory
Date: Sat, 25 May 2019 13:23:01 +0100 [thread overview]
Message-ID: <CAH52Xb3UieniG=vV=XCm8+EAn9=1Lsqq2EptRuJZXhy+C94pnA@mail.gmail.com> (raw)
In-Reply-To: <BFBE1A09-A246-4DAD-8AD2-25C3C517A7FE@cmu.edu>
I am aware of Floris' work (which is in Lean 2, which used HoTT; Lean
3 has an impredicative Prop). My question is broader. It does not
surprise me that doing homotopy theory is nice in homotopy type
theory. What I am interested in is what happens when one tries to do
other kinds of "normal mathematics" such as for example formalising
parts of EGA.
On Sat, 25 May 2019 at 11:22, Steve Awodey <awodey@cmu.edu> wrote:
>
> A useful example for you might be Floris van Doorn’s formalization 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 <kevin.m.buzzard@gmail.com> 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 mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because 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 skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however 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 handle the rings showing up in a sheaf of rings.
> >
> > I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a 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 involved with formalising mathematical objects in dependent type 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 theorems 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 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 failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full 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/msgid/HomotopyTypeTheory/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.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/CAH52Xb3UieniG%3DvV%3DXCm8%2BEAn9%3D1Lsqq2EptRuJZXhy%2BC94pnA%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.
```

next prev parent reply other threads:[~2019-05-25 12:23 UTC|newest]Thread overview:31+ messages / expand[flat|nested] mbox.gz Atom feed top 2019-05-25 10:12 Kevin Buzzard 2019-05-25 10:22 ` Steve Awodey2019-05-25 12:23 ` Kevin Buzzard [this message][not found] ` <B7D67BBA-5E0B-4438-908D-4EF316C8C1F1@chalmers.se> [not found] ` <CAH52Xb1Y=Xq=012v_-KSDUuwgnKpEp5qjrxgtUJf+qc_0RWJUg@mail.gmail.com> 2019-05-25 13:13 ` Fwd: " Kevin Buzzard 2019-05-25 13:34 ` Juan Ospina 2019-05-25 14:50 ` Noah Snyder 2019-05-25 15:36 ` Kevin Buzzard 2019-05-25 16:41 ` Noah Snyder 2019-05-26 5:50 ` Bas Spitters 2019-05-26 11:41 ` Kevin Buzzard 2019-05-26 12:09 ` Bas Spitters 2019-05-26 17:00 ` Kevin Buzzard 2019-05-27 2:33 ` Daniel R. Grayson 2019-06-02 16:30 ` Bas Spitters 2019-06-02 17:55 ` Kevin Buzzard 2019-06-02 20:46 ` Nicola Gambino 2019-06-02 20:59 ` Valery Isaev 2019-06-04 20:32 ` Michael Shulman 2019-06-04 20:58 ` Kevin Buzzard 2019-06-06 16:30 ` Matt Oliveri 2019-05-27 13:09 ` Assia Mahboubi 2019-05-28 9:50 ` Michael Shulman 2019-05-28 10:13 ` Nils Anders Danielsson 2019-05-28 10:22 ` Michael Shulman 2019-05-29 19:04 ` Martín Hötzel Escardó 2019-05-30 17:14 ` Michael Shulman 2019-06-02 17:49 ` Kevin Buzzard 2019-06-04 20:50 ` Martín Hötzel Escardó 2019-06-05 17:11 ` Thorsten Altenkirch 2019-05-28 15:20 ` Joyal, André 2019-05-27 8:41 ` Nils Anders Danielsson

Be sure your reply has aReply instructions:You may reply publicly to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the--to,--cc, and--in-reply-toswitches of git-send-email(1): git send-email \ --in-reply-to='CAH52Xb3UieniG=vV=XCm8+EAn9=1Lsqq2EptRuJZXhy+C94pnA@mail.gmail.com' \ --to=kevin.m.buzzard@gmail.com \ --cc=HomotopyTypeTheory@googlegroups.com \ --cc=awodey@cmu.edu \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting theIn-Reply-Toheader via mailto: links, try the mailto: link

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).