Fwd: [HoTT] doing "all of pure mathematics" in type theory

[Kevin Buzzard <kevin.m.buzzard@gmail.com>]

On Sat, 25 May 2019 at 12:26, Thierry Coquand <Thierry.Coquand@cse.gu.se> wrote:
>
>
> 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’s 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 “classical” approach to representation of structures
> and the approach in the univalent setting.
>
>  The system is compatible with classical logic and choice (but this has not been needed in these examples).
>
>  Best regards,
>  Thierry
>
>
>
> On 25 May 2019, at 12: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/BFBE1A09-A246-4DAD-8AD2-25C3C517A7FE%40cmu.edu.
> 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/CAH52Xb0EK8xf1d6Oq9AgAcnjenu4Nhu7H7VcvDWToMpVKVtCog%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.