Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] doing "all of pure mathematics" in type theory
@ 2019-05-25 10:12 Kevin Buzzard
  2019-05-25 10:22 ` Steve Awodey
  0 siblings, 1 reply; 31+ messages in thread
From: Kevin Buzzard @ 2019-05-25 10:12 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 3305 bytes --]

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.

[-- Attachment #1.2: Type: text/html, Size: 3866 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-25 10:12 [HoTT] doing "all of pure mathematics" in type theory Kevin Buzzard
@ 2019-05-25 10:22 ` Steve Awodey
  2019-05-25 12:23   ` Kevin Buzzard
                     ` (2 more replies)
  0 siblings, 3 replies; 31+ messages in thread
From: Steve Awodey @ 2019-05-25 10:22 UTC (permalink / raw)
  To: Kevin Buzzard; +Cc: Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-25 10:22 ` Steve Awodey
@ 2019-05-25 12:23   ` Kevin Buzzard
       [not found]   ` <B7D67BBA-5E0B-4438-908D-4EF316C8C1F1@chalmers.se>
  2019-05-25 13:34   ` Juan Ospina
  2 siblings, 0 replies; 31+ messages in thread
From: Kevin Buzzard @ 2019-05-25 12:23 UTC (permalink / raw)
  To: Steve Awodey; +Cc: Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Fwd: [HoTT] doing "all of pure mathematics" in type theory
       [not found]     ` <CAH52Xb1Y=Xq=012v_-KSDUuwgnKpEp5qjrxgtUJf+qc_0RWJUg@mail.gmail.com>
@ 2019-05-25 13:13       ` Kevin Buzzard
  0 siblings, 0 replies; 31+ messages in thread
From: Kevin Buzzard @ 2019-05-25 13:13 UTC (permalink / raw)
  To: Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-25 10:22 ` Steve Awodey
  2019-05-25 12:23   ` Kevin Buzzard
       [not found]   ` <B7D67BBA-5E0B-4438-908D-4EF316C8C1F1@chalmers.se>
@ 2019-05-25 13:34   ` Juan Ospina
  2019-05-25 14:50     ` Noah Snyder
  2 siblings, 1 reply; 31+ messages in thread
From: Juan Ospina @ 2019-05-25 13:34 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 4630 bytes --]

On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the "additivity 
axiom".  Please let me know if the following formulation of the such axiom 
is correct:

[image: additivity.jpg]



On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey 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....@gmail.com 
> <javascript:>> 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 <javascript:>. 
>
> > 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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 8375 bytes --]

[-- Attachment #2: additivity.jpg --]
[-- Type: image/jpeg, Size: 18737 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-25 13:34   ` Juan Ospina
@ 2019-05-25 14:50     ` Noah Snyder
  2019-05-25 15:36       ` Kevin Buzzard
  0 siblings, 1 reply; 31+ messages in thread
From: Noah Snyder @ 2019-05-25 14:50 UTC (permalink / raw)
  To: Juan Ospina; +Cc: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 7350 bytes --]

HoTT is NOT a specific proof assistant the way that Lean is.  Instead it’s
a different flavor of type theory which is well attuned to things that have
a homotopical flavor.  It can be implemented in various proof assistants
(Coq, Agda, Lean 2) but none of them are really fully designed for HoTT.
But the kind of practical question you’re asking depends on the
implementation.  I don’t think any of the implementations are practical in
the way that you want.  For example, I’m not aware of any kind of “tactics”
for HoTT.  The bookkeeping involved in saying that the two proofs of
Eckman-Hilton for 3-loops agree (which I could explain in one hand gesture
in person and where I understand all the relevant issues in HoTT) is very
very intimidating practically.  I’d also imagine that a “practical”
implementation would likely have some kind of “two-level” type theory where
you can use types that behave classically when that’s better and HoTT types
when that’s better.

HoTT is mostly better for math that’s explicitly homotopical.  But there
are situations in more ordinary math where you can see why it would be
useful.  For example, if G and H are isomorphic groups and you want to
translate a theorem or construction across the isomorphism.  In ordinary
type theory this is going to involve annoying book-keeping which it seems
like you’d have to do separately for each kind of mathematical object.  In
HoTT that happens automatically.  For example, say you have a theorem about
bimodules over semisimple rings whose proof starts “wlog, by
Artin-Wedderburn, we can assume both algebras are multimatrix algebras over
division rings.”  Is that step something you’d be able to deal with easily
in Lean?  If not, that’s somewhere that down the line HoTT might make
things more practical.

But mostly I just want to say you’re making a category error in your
question.  HoTT is an abstract type theory, not a proof assistant.

Best,

Noah

On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> 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 the
> such axiom is correct:
>
> [image: additivity.jpg]
>
>
>
> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey 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....@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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 9395 bytes --]

[-- Attachment #2: additivity.jpg --]
[-- Type: image/jpeg, Size: 18737 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-25 14:50     ` Noah Snyder
@ 2019-05-25 15:36       ` Kevin Buzzard
  2019-05-25 16:41         ` Noah Snyder
  0 siblings, 1 reply; 31+ messages in thread
From: Kevin Buzzard @ 2019-05-25 15:36 UTC (permalink / raw)
  To: Noah Snyder; +Cc: Juan Ospina, Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 9733 bytes --]

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, "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 <nsnyder@gmail.com> wrote:

> I’d also imagine that a “practical” implementation would likely have some
> kind of “two-level” type theory where you can use types that behave
> classically when that’s better and HoTT types when that’s 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
"faithfully", 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 type theory
> this is going to involve annoying book-keeping which it seems like you’d
> 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 mathematician
"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 using which cannot deduce this immediately. As an interesting
experiment, find your 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 will be very confident that this is true, even if they do not
know the definition; 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 make 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 for "the way
mathematicians think". However now I've looked over what has currently been
formalised in UniMath I am wondering whether there are pain points 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 semisimple rings
> whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras
> are multimatrix algebras over division rings.”  Is that step something
> you’d be able to deal with easily in Lean?  If not, that’s somewhere that
> down the line HoTT might make things more practical.
>

This is a great example! To be honest I am slightly confused about 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 development)
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’re making a category error in your
> question.  HoTT is an abstract type theory, not a proof assistant.
>
> Best,
>
> Noah
>
> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> 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 the
>> such axiom is correct:
>>
>> [image: additivity.jpg]
>>
>>
>>
>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey 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....@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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com
>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com?utm_medium=email&utm_source=footer>
>> .
>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
> 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/CAH52Xb3k4fmuPfpDSO%3DJmb3k19v3m6MjOLweQb_u8n0icdt0rQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 12940 bytes --]

[-- Attachment #2: additivity.jpg --]
[-- Type: image/jpeg, Size: 18737 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-25 15:36       ` Kevin Buzzard
@ 2019-05-25 16:41         ` Noah Snyder
  2019-05-26  5:50           ` Bas Spitters
  2019-05-27  8:41           ` Nils Anders Danielsson
  0 siblings, 2 replies; 31+ messages in thread
From: Noah Snyder @ 2019-05-25 16:41 UTC (permalink / raw)
  To: Kevin Buzzard; +Cc: Homotopy Type Theory, Juan Ospina

[-- Attachment #1: Type: text/plain, Size: 12121 bytes --]

UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a
category from “Coq with the indices-matter option plus the HoTT library."
“Coq with the indices-matter option plus the 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 can 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 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* tactics are
available in Coq+indices-matter+HoTT, but not many of the more advanced
ones, and to my knowledge, not tactics needed for complicated homotopical
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 assumed 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, “Coq 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 does 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 categories
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 <kevin.m.buzzard@gmail.com>
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, "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 <nsnyder@gmail.com> wrote:
>
>> I’d also imagine that a “practical” implementation would likely have some
>> kind of “two-level” type theory where you can use types that behave
>> classically when that’s better and HoTT types when that’s 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
> "faithfully", 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 type theory
>> this is going to involve annoying book-keeping which it seems like you’d
>> 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 mathematician
> "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 using which cannot deduce this immediately. As an interesting
> experiment, find your 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 will be very confident that this is true, even if they do not
> know the definition; 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 make 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 for
> "the way mathematicians think". However now I've looked over what has
> currently been formalised in UniMath I am wondering whether there are pain
> points 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 semisimple
>> rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both
>> algebras are multimatrix algebras over division rings.”  Is that step
>> something you’d be able to deal with easily in Lean?  If not, that’s
>> somewhere that down the line HoTT might make things more practical.
>>
>
> This is a great example! To be honest I am slightly confused about 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 development)
> 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’re making a category error in your
>> question.  HoTT is an abstract type theory, not a proof assistant.
>>
>> Best,
>>
>> Noah
>>
>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> 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 the
>>> such axiom is correct:
>>>
>>> [image: additivity.jpg]
>>>
>>>
>>>
>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey 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....@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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com
>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com?utm_medium=email&utm_source=footer>
>>> .
>>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com
>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com?utm_medium=email&utm_source=footer>
>> .
>
>
>> 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-hmwRsr1iwztPg%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 16876 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-25 16:41         ` Noah Snyder
@ 2019-05-26  5:50           ` Bas Spitters
  2019-05-26 11:41             ` Kevin Buzzard
  2019-05-27  8:41           ` Nils Anders Danielsson
  1 sibling, 1 reply; 31+ messages in thread
From: Bas Spitters @ 2019-05-26  5:50 UTC (permalink / raw)
  To: Noah Snyder; +Cc: Kevin Buzzard, Homotopy Type Theory, Juan Ospina

[-- Attachment #1: Type: text/plain, Size: 14134 bytes --]

There has been progress in making a cleaner interface with the standard 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 future.
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 connection
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, there'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 currently
published in the Annals.

On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote:

> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a
> category from “Coq with the indices-matter option plus the HoTT library."
> “Coq with the indices-matter option plus the 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 can 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 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* tactics are
> available in Coq+indices-matter+HoTT, but not many of the more advanced
> ones, and to my knowledge, not tactics needed for complicated homotopical
> 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 assumed 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, “Coq 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 does 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 categories
> 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 <kevin.m.buzzard@gmail.com>
> 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, "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 <nsnyder@gmail.com> wrote:
>>
>>> I’d also imagine that a “practical” implementation would likely have
>>> some kind of “two-level” type theory where you can use types that behave
>>> classically when that’s better and HoTT types when that’s 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
>> "faithfully", 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 type theory
>>> this is going to involve annoying book-keeping which it seems like you’d
>>> 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 mathematician
>> "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 using which cannot deduce this immediately. As an interesting
>> experiment, find your 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 will be very confident that this is true, even if they do not
>> know the definition; 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 make 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 for
>> "the way mathematicians think". However now I've looked over what has
>> currently been formalised in UniMath I am wondering whether there are pain
>> points 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 semisimple
>>> rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both
>>> algebras are multimatrix algebras over division rings.”  Is that step
>>> something you’d be able to deal with easily in Lean?  If not, that’s
>>> somewhere that down the line HoTT might make things more practical.
>>>
>>
>> This is a great example! To be honest I am slightly confused about 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 development)
>> 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’re making a category error in your
>>> question.  HoTT is an abstract type theory, not a proof assistant.
>>>
>>> Best,
>>>
>>> Noah
>>>
>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> 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 the
>>>> such axiom is correct:
>>>>
>>>> [image: additivity.jpg]
>>>>
>>>>
>>>>
>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey 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....@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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com
>>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com?utm_medium=email&utm_source=footer>
>>>> .
>>>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com
>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com?utm_medium=email&utm_source=footer>
>>> .
>>
>>
>>> 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-hmwRsr1iwztPg%40mail.gmail.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
> 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/CAOoPQuTNxVJ5%2B1Xotk3wzCgaW0C4wcxOdkpHANbOYdK5rCRkiA%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 18925 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-26  5:50           ` Bas Spitters
@ 2019-05-26 11:41             ` Kevin Buzzard
  2019-05-26 12:09               ` Bas Spitters
  0 siblings, 1 reply; 31+ messages in thread
From: Kevin Buzzard @ 2019-05-26 11:41 UTC (permalink / raw)
  To: Bas Spitters; +Cc: Noah Snyder, Homotopy Type Theory, Juan Ospina

[-- Attachment #1: Type: text/plain, Size: 18691 bytes --]

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 + impredicative
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 more
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 just a
matter of writing some incantation at the top of a file and then not
thinking 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,
but don't use these commands or these tactics"), which maybe raises the
entry barrier for mathematicians a bit (and speaking from personal
experience, already this entry barrier is quite high). High level tactics
are absolutely crucial for mathematical Lean users. This is one of the
reasons that the Lean 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 calculations 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 possible I am
becoming convinced that it can really change mathematics. In my experience
the biggest obstruction to it changing mathematics is simply that
mathematicians 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
this stuff works. In short, I think type theory has an image problem. Sure
there are category theorists who know about it, but how many category
theorists 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 would love to draw the mathematics and computer science communities
closer together over ideas like this, but it's hard work. I am wondering
whether developing accessible databases of undergraduate level mathematics
would at least 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 weekend I've learnt something about UniMath, but whilst it might do
bicategories very well (which are not on our undergraduate curriculum),
where is the basic 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 have schemes. I know that Gonthier and his
coauthors had to make a lot of undergraduate level maths (Galois theory,
algebraic number theory, group theory) 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 formalisation when you're trying to
sell to "normal research mathematicians", and I don't know what is. I'm now
wondering making formalised undergraduate mathematics more accessible to
untrained mathematicians is a better approach, but who knows. Obviously "AI
which can solve the Riemann hypothesis" will 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 bunch of
extremely smart people, both mathematicians and computer scientists, have
invested a lot of time in thinking about how to do mathematics with type
theory. I find it very frustrating that mathematicians are not beginning to
notice. Of course there are exceptions. One day though -- will there simply
be a gigantic wave which crashes through mathematics and forces
mathematicians 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 <b.a.w.spitters@gmail.com> wrote:

> There has been progress in making a cleaner interface with the standard
> 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 future.
> 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 connection
> 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, there'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
> currently published in the Annals.
>
> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote:
>
>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a
>> category from “Coq with the indices-matter option plus the HoTT library."
>> “Coq with the indices-matter option plus the 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 can 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 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* tactics are
>> available in Coq+indices-matter+HoTT, but not many of the more advanced
>> ones, and to my knowledge, not tactics needed for complicated homotopical
>> 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 assumed 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, “Coq 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 does 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 categories
>> 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 <kevin.m.buzzard@gmail.com>
>> 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, "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 <nsnyder@gmail.com> wrote:
>>>
>>>> I’d also imagine that a “practical” implementation would likely have
>>>> some kind of “two-level” type theory where you can use types that behave
>>>> classically when that’s better and HoTT types when that’s 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
>>> "faithfully", 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 type theory
>>>> this is going to involve annoying book-keeping which it seems like you’d
>>>> 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 mathematician
>>> "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 using which cannot deduce this immediately. As an interesting
>>> experiment, find your 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 will be very confident that this is true, even if they do not
>>> know the definition; 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 make 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 for
>>> "the way mathematicians think". However now I've looked over what has
>>> currently been formalised in UniMath I am wondering whether there are pain
>>> points 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 semisimple
>>>> rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both
>>>> algebras are multimatrix algebras over division rings.”  Is that step
>>>> something you’d be able to deal with easily in Lean?  If not, that’s
>>>> somewhere that down the line HoTT might make things more practical.
>>>>
>>>
>>> This is a great example! To be honest I am slightly confused about 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 development)
>>> 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’re making a category error in your
>>>> question.  HoTT is an abstract type theory, not a proof assistant.
>>>>
>>>> Best,
>>>>
>>>> Noah
>>>>
>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com>
>>>> 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 the
>>>>> such axiom is correct:
>>>>>
>>>>> [image: additivity.jpg]
>>>>>
>>>>>
>>>>>
>>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey 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....@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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com
>>>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com?utm_medium=email&utm_source=footer>
>>>>> .
>>>>> 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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com
>>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com?utm_medium=email&utm_source=footer>
>>>> .
>>>
>>>
>>>> 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-hmwRsr1iwztPg%40mail.gmail.com
>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com?utm_medium=email&utm_source=footer>
>> .
>> 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/CAH52Xb3k9b8D0oW8Ue8XGY-ZAJZHfmc1pTRTJO1Qg%3D3Dw0zwuA%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 23667 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-26 11:41             ` Kevin Buzzard
@ 2019-05-26 12:09               ` Bas Spitters
  2019-05-26 17:00                 ` Kevin Buzzard
  2019-05-27 13:09                 ` Assia Mahboubi
  0 siblings, 2 replies; 31+ messages in thread
From: Bas Spitters @ 2019-05-26 12:09 UTC (permalink / raw)
  To: Kevin Buzzard; +Cc: Noah Snyder, Homotopy Type Theory, Juan Ospina

Dear Kevin,

We've been working on making formalization accessible to
mathematicians for a long time. E.g. in our formath project:
http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath

It's a slow process, but I believe we are making progress.

You seem to be mixing at least two issues.
- HoTT/UF as a foundation
- Current implementations in proof assistants.

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 <kevin.m.buzzard@gmail.com> 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 + impredicative 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 more 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 just a matter of writing some incantation at the top of a file and then not thinking 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, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean 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 calculations 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 possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians 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 this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists 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 would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least 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 weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic 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 have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) 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 formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will 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 bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians 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 <b.a.w.spitters@gmail.com> wrote:
>>
>> There has been progress in making a cleaner interface with the standard 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 future.
>> 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 connection 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, there'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 currently published in the Annals.
>>
>> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote:
>>>
>>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library."   “Coq with the indices-matter option plus the 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 can 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 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* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical 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 assumed 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, “Coq 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 does 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 categories 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 <kevin.m.buzzard@gmail.com> 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, "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 <nsnyder@gmail.com> wrote:
>>>>>
>>>>> I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s 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 "faithfully", 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 type theory this is going to involve annoying book-keeping which it seems like you’d 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 mathematician "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 using which cannot deduce this immediately. As an interesting experiment, find your 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 will be very confident that this is true, even if they do not know the definition; 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 make 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 for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points 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 semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.”  Is that step something you’d be able to deal with easily in Lean?  If not, that’s somewhere that down the line HoTT might make things more practical.
>>>>
>>>>
>>>> This is a great example! To be honest I am slightly confused about 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 development) 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’re making a category error in your question.  HoTT is an abstract type theory, not a proof assistant.
>>>>>
>>>>> Best,
>>>>>
>>>>> Noah
>>>>>
>>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> 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 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’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....@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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%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-hmwRsr1iwztPg%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/CAOoPQuTnM2F9a5VTGKjfxemPCizRyiAoM_VDYNgfTnF89gCBKg%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  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-05-27 13:09                 ` Assia Mahboubi
  1 sibling, 2 replies; 31+ messages in thread
From: Kevin Buzzard @ 2019-05-26 17:00 UTC (permalink / raw)
  To: Bas Spitters; +Cc: Noah Snyder, Homotopy Type Theory, Juan Ospina

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 <b.a.w.spitters@gmail.com> 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 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 <kevin.m.buzzard@gmail.com> 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 + impredicative 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 more 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 just a matter of writing some incantation at the top of a file and then not thinking 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, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean 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 calculations 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 possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians 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 this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists 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 would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least 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 weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic 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 have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) 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 formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will 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 bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians 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 <b.a.w.spitters@gmail.com> wrote:
> >>
> >> There has been progress in making a cleaner interface with the standard 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 future.
> >> 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 connection 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, there'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 currently published in the Annals.
> >>
> >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote:
> >>>
> >>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library."   “Coq with the indices-matter option plus the 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 can 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 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* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical 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 assumed 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, “Coq 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 does 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 categories 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 <kevin.m.buzzard@gmail.com> 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, "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 <nsnyder@gmail.com> wrote:
> >>>>>
> >>>>> I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s 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 "faithfully", 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 type theory this is going to involve annoying book-keeping which it seems like you’d 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 mathematician "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 using which cannot deduce this immediately. As an interesting experiment, find your 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 will be very confident that this is true, even if they do not know the definition; 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 make 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 for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points 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 semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.”  Is that step something you’d be able to deal with easily in Lean?  If not, that’s somewhere that down the line HoTT might make things more practical.
> >>>>
> >>>>
> >>>> This is a great example! To be honest I am slightly confused about 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 development) 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’re making a category error in your question.  HoTT is an abstract type theory, not a proof assistant.
> >>>>>
> >>>>> Best,
> >>>>>
> >>>>> Noah
> >>>>>
> >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> 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 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’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....@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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%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-hmwRsr1iwztPg%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/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3A%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-26 17:00                 ` Kevin Buzzard
@ 2019-05-27  2:33                   ` Daniel R. Grayson
  2019-06-02 16:30                   ` Bas Spitters
  1 sibling, 0 replies; 31+ messages in thread
From: Daniel R. Grayson @ 2019-05-27  2:33 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 2967 bytes --]

On Sunday, May 26, 2019 at 12:00:21 PM UTC-5, Kevin Buzzard wrote:
 
>
> ... 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.
>

UniMath was formed from Voevodsky's Foundations (see 

    https://github.com/UniMath/Foundations

) and some formalizations based on it by other people, starting with 
Benedikt 
Ahrens and me, and continuing with many others.  In particular, the  
formalization of category theory began with Ahrens' formalization of the 
material in a joint
paper of his with Kapulkin and Shulman, see 

    
https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/README.md

, and has been continued by other people, not Voevodsky.

Voevodsky was probably too busy writing his papers on the semantics of the 
system to turn to
formalizing the basic theory of schemes.  For a while he said he wasn't 
even interested in formalizing
his proof of the Milnor conjecture, because he was confident it was 
correct.  Then later he said, in a talk,
that it would be important top find a constructive proof of the Milnor 
conjecture, and to formalize it, 
pinpointing a particular argument due to Merkurjev and Suslin as being 
non-constructive, see the remark
under the entry at 

   
http://www.math.ias.edu/Voevodsky/voevodsky-publications_abstracts.html#UniMath-1

I also remember, perhaps in early 2014, that he told me he was thinking of 
formalizing the definition of scheme
(or maybe variety) so he could talk about it at a forthcoming talk, but he 
never did that.

Eventually UniMath should have the theory of schemes in it.

By the way, to go back to your original question, I think there are no 
"pain points" in formalizing
traditional mathematics in UniMath.  The pain and challenge seem only to 
come when generalizing traditional facts
about sets so they apply also to types that are not assumed to be sets.  
For an example of that,
see Peter Lumsdaine's proof of transfinite induction into a family of types 
at

    
https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/WellFoundedRelations.v#L208

or see our proof with Bezem and Buchholtz that the type of ℤ-torsors 
satisfies the induction principle into
a family of types that the circle satisfies, at

    https://github.com/UniMath/SymmetryBook/blob/master/ZTors.tex

-- 
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/d57bb2de-ff98-484b-8bc0-9c3f31620a47%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 4318 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-25 16:41         ` Noah Snyder
  2019-05-26  5:50           ` Bas Spitters
@ 2019-05-27  8:41           ` Nils Anders Danielsson
  1 sibling, 0 replies; 31+ messages in thread
From: Nils Anders Danielsson @ 2019-05-27  8:41 UTC (permalink / raw)
  To: Homotopy Type Theory

On 25/05/2019 18.41, Noah Snyder wrote:
> (When I was using Agda the situation was even worse, things like
> pattern matching secretly assumed 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.)

Things are a bit better now. Jesper Cockx and others have worked out a
better story for --without-K, and Anders Mörtberg, Andrea Vezzosi and
others have implemented --cubical, with direct support for HITs.

-- 
/NAD

-- 
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/0e51ad31-29cb-d054-5e96-1544732f47eb%40cse.gu.se.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-26 12:09               ` Bas Spitters
  2019-05-26 17:00                 ` Kevin Buzzard
@ 2019-05-27 13:09                 ` Assia Mahboubi
  2019-05-28  9:50                   ` Michael Shulman
  1 sibling, 1 reply; 31+ messages in thread
From: Assia Mahboubi @ 2019-05-27 13:09 UTC (permalink / raw)
  To: Bas Spitters, Kevin Buzzard
  Cc: Noah Snyder, Homotopy Type Theory, Juan Ospina

Dear Bas, dear all,

thanks for the advertising this work. A small clarification:

Le 26/05/2019 à 14:09, Bas Spitters a écrit :
>
> 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/

the mathematical components library is about constructive mathematics
and is formalized in CIC (Gallina) without axiom ...

> and the analysis library that is currently under development.
> https://github.com/math-comp/analysis

... but the analysis one is indeed about classical mathematics.

Best wishes,

assia

> 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 <kevin.m.buzzard@gmail.com> 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 + impredicative 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 more 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 just a matter of writing some incantation at the top of a file and then not thinking 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, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean 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 calculations 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 possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians 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 this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists 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 would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least 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 weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic 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 have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) 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 formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will 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 bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians 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 <b.a.w.spitters@gmail.com> wrote:
>>>
>>> There has been progress in making a cleaner interface with the standard 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 future.
>>> 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 connection 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, there'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 currently published in the Annals.
>>>
>>> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote:
>>>>
>>>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library."   “Coq with the indices-matter option plus the 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 can 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 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* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical 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 assumed 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, “Coq 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 does 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 categories 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 <kevin.m.buzzard@gmail.com> 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, "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 <nsnyder@gmail.com> wrote:
>>>>>>
>>>>>> I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s 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 "faithfully", 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 type theory this is going to involve annoying book-keeping which it seems like you’d 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 mathematician "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 using which cannot deduce this immediately. As an interesting experiment, find your 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 will be very confident that this is true, even if they do not know the definition; 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 make 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 for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points 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 semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.”  Is that step something you’d be able to deal with easily in Lean?  If not, that’s somewhere that down the line HoTT might make things more practical.
>>>>>
>>>>>
>>>>> This is a great example! To be honest I am slightly confused about 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 development) 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’re making a category error in your question.  HoTT is an abstract type theory, not a proof assistant.
>>>>>>
>>>>>> Best,
>>>>>>
>>>>>> Noah
>>>>>>
>>>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> 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 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’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....@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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%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-hmwRsr1iwztPg%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/3f6331a7-688e-570b-01d8-d02a81eac96b%40inria.fr.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  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 15:20                     ` Joyal, André
  0 siblings, 2 replies; 31+ messages in thread
From: Michael Shulman @ 2019-05-28  9:50 UTC (permalink / raw)
  To: Kevin Buzzard; +Cc: Homotopy Type Theory

In my opinion there are several separate issues standing in the way of
a wider use of proof assistants.  One has to do with the design of the
underlying formal systems.  In this respect Book HoTT (the formal
system of the homotopy type theory book, with univalence and higher
inductive types added in an "ad hoc" way on top of intensional
Martin-Lof type theory) is a step forward over systems such as CiC and
MLTT on which Coq and Agda are based, due to various factors such as a
nice treatment of quotients, automatic isomorphism-invariance,
inductive and free constructions, etc.

However, Book HoTT is also a step backwards, because the presence of
non-computational "axioms" means that "execution" gets stuck whenever
you try to use univalence.  So you can prove automatically that
anything true about a group G is true about an isomorphic group H, but
if you then try to take some specific statement about some specific
group G and transfer it to a specific statement about a specific group
H along a specific isomorphism, what you'll get will be an unreadable
statement littered with explicit transports across univalence-induced
paths in the universe, rather than the "real" statement about H that
should be obtained from actually *applying* that specific isomorphism.
(To be fair, plenty of people using a system like Coq pre-HoTT had to
add their own axioms, such as function extensionality and UIP, and
when you want classical logic that's unavoidably an axiom.  But at
least the underlying type theory of Coq and Agda can "compute".)  More
modern homotopy type theories, which are generally based on cubical
structures, allow univalence to be "executed" by the system.  However,
these systems lack (so far) all the intended categorical semantics
(see below), and haven't yet been implemented in "real world" proof
assistants (though there are prototypes now in use and development).

In addition, as Noah mentioned, two-level theories with a stricter
kind of equality (which do *not* exist in UniMath, HoTT/Coq, or
HoTT/Agda -- this point is about having two different equalities on
the same type, not two different classes of types with different
equality behavior) are likely to make many things easier, but haven't
been implemented in real-world proof assistants either (apart from
some sneaky coding with typeclasses).

So overall, I would say that the underlying design of homotopy type
theories is not yet "in order" to achieve its hoped-for maximal
benefit in a proof assistant by the working mathematician, though
there are promising signs and progress is being made.

All the issues discussed above are what I would call "mathematical",
or perhaps more broadly "theoretical".  But a separate issue standing
in the way of wider use of proof assistants is what I would call
"engineering".  No matter how fancy we make the underlying formal
system, I believe it will always remain true (for the foreseeable
future) that a proof assistant needs a lot more detailed information
than an ordinary mathematician would care to provide, or need to see,
in writing and understanding a proof.  This is where we need things
like tactics, implicit arguments, elaboration, proof automation, etc.
to fill in the gaps and make the system usable in practice.  Here
there's been a lot of progress over the past decades, but I think
there's a long way to go too, and choosing a better underlying
foundation (like any form of HoTT, cubical or otherwise) may improve
things a bit but is not really a game-changer.

However, there's something completely different that I do believe has
the potential to be a game-changer.  There's already a very different
"gigantic wave crashing through mathematics": homotopy theory and
higher category theory.  Homotopy type theory gives type theory and
formalization the potential to ride that wave.  The real point here is
that when something is formalized in type theory -- constructively --
it is automatically true internally in all models of type theory, and
for homotopy type theory those models include higher categories.  Note
that the use of constructive logic has nothing to do with any
philosophical belief; classical logic can still be "true" in the "real
world", and yet constructive reasoning is valuable because it makes a
theorem true internally in more categories.

I think it's fairly hopeless to convince a classical mathematician
that they should put in a lot of work to convince a computer of the
truth of *something they already knew*.  But I have much more hope of
convincing them that they should tweak their proofs slightly, and
perhaps use a computer to help verify the validity of the tweaks, in
order that *essentially the same proof* will allow them to conclude a
*vastly more general theorem*.  Moreover, when working with higher
categories the advantage is even more pronounced, because homotopy
type theories introduce a totally new kind of proof that can be much
simpler than all the previously available options -- and the immediate
feedback involved in using a proof assistant is one of the best ways
to *learn* that style of proof.

In short, I think there's a huge public relations opportunity here for
type theory and computer formalization, which sadly even Voevodsky
missed out on.  Rather than selling it as a way to be absolutely sure
of proofs we already believe in (as important as that might be), we
should sell it as a framework for *entirely new proofs* that bring the
otherwise fiendishly complicated and technical world of higher
category theory "down to earth".  The experts in higher category
theory are familiar with the fact that in many respects it is "more
natural" and "better behaved" than ordinary category theory; but there
are thick barriers to entry preventing many of us from getting to that
point of expertise.  With synthetic mathematics in homotopy type
theory, we can envision one day teaching higher category theory to
undergraduates.

-- 
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/CAOvivQx_b2QkEL-HqMXQNJ_QA83KjdAnFe7RmmiPRRQX6tYk-A%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-28  9:50                   ` Michael Shulman
@ 2019-05-28 10:13                     ` Nils Anders Danielsson
  2019-05-28 10:22                       ` Michael Shulman
  2019-05-28 15:20                     ` Joyal, André
  1 sibling, 1 reply; 31+ messages in thread
From: Nils Anders Danielsson @ 2019-05-28 10:13 UTC (permalink / raw)
  To: Homotopy Type Theory

On 28/05/2019 11.50, Michael Shulman wrote:
> More modern homotopy type theories, which are generally based on
> cubical structures, allow univalence to be "executed" by the system.
> However, these systems lack (so far) all the intended categorical
> semantics (see below), and haven't yet been implemented in "real
> world" proof assistants (though there are prototypes now in use and
> development).

The latest release of Agda can be used in cubical mode, and supports
both univalence and higher inductive types. (As well as things like
higher inductive-coinductive-recursive types that may not have a proper
explanation.)

-- 
/NAD

-- 
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/9232f85a-6d64-84dc-a2d0-290c0fc6e760%40cse.gu.se.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  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ó
  0 siblings, 1 reply; 31+ messages in thread
From: Michael Shulman @ 2019-05-28 10:22 UTC (permalink / raw)
  To: Nils Anders Danielsson; +Cc: Homotopy Type Theory

Of course Agda is a real-world proof assistant, but its cubical mode
is still new and experimental, so I was counting it as a "prototype".
But I suppose that's not really fair, since unlike a custom-developed
prototype it presumably benefits from all the usability superstructure
of Agda.  Sorry!

On Tue, May 28, 2019 at 3:13 AM Nils Anders Danielsson <nad@cse.gu.se> wrote:
>
> On 28/05/2019 11.50, Michael Shulman wrote:
> > More modern homotopy type theories, which are generally based on
> > cubical structures, allow univalence to be "executed" by the system.
> > However, these systems lack (so far) all the intended categorical
> > semantics (see below), and haven't yet been implemented in "real
> > world" proof assistants (though there are prototypes now in use and
> > development).
>
> The latest release of Agda can be used in cubical mode, and supports
> both univalence and higher inductive types. (As well as things like
> higher inductive-coinductive-recursive types that may not have a proper
> explanation.)
>
> --
> /NAD
>
> --
> 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/9232f85a-6d64-84dc-a2d0-290c0fc6e760%40cse.gu.se.
> 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/CAOvivQyPDzzjLEQfB%3DC5jQSH8wzFpr%3DgG8E_4BSWaBtb95mg3w%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* RE: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-28  9:50                   ` Michael Shulman
  2019-05-28 10:13                     ` Nils Anders Danielsson
@ 2019-05-28 15:20                     ` Joyal, André
  1 sibling, 0 replies; 31+ messages in thread
From: Joyal, André @ 2019-05-28 15:20 UTC (permalink / raw)
  To: Michael Shulman, Kevin Buzzard; +Cc: Homotopy Type Theory

Dear Mike,

I would like to add my grain of salt to the discussion.
I think that mathematical research is more a communal activity than we think.
What is considered a proof largely depends on a consensus developed within the mathematical community.
Of course, the consensus relies on the opinions of experts and specialists. 
Publications and referees have an important role.
But there is also a mathematical culture based on knowledge of abstract ideas
and the mastery of symbolic computations.

Homotopy type theory is contributing to the present mathematical culture by bringing 
a new formalism and new abstract ideas.
It claims to be constructive and general (everything is a type).
There is an old philosophical debate concerning constructive mathematics
that was initiated by the work of Cantor, Kronecker, Hilbert, Brouwer and Bishop, to name a few.
It is true that a constructive theorem is in a sense better and more general.
In reality, constructive and non-constructive mathematics are the two faces of the same coin.
The latter is feeding the former with results to be proved constructively!
It seems obvious that the debate will endure for many generations to come.

I believe that the contributions of homotopy type theory to the mathematical
culture are important and real. It is worth developing abstractly and for
the purpose of creating user-friendly powerful proof assistants.
The language of type theory includes parametrised objects, sums, products, universes and univalence.
It is not incompatible with the language of category theory and of homotopy theory.
Hopefully, the three languages will be combined.

Best,
andré
________________________________________
From: homotopytypetheory@googlegroups.com [homotopytypetheory@googlegroups.com] on behalf of Michael Shulman [shulman@sandiego.edu]
Sent: Tuesday, May 28, 2019 5:50 AM
To: Kevin Buzzard
Cc: Homotopy Type Theory
Subject: Re: [HoTT] doing "all of pure mathematics" in type theory

In my opinion there are several separate issues standing in the way of
a wider use of proof assistants.  One has to do with the design of the
underlying formal systems.  In this respect Book HoTT (the formal
system of the homotopy type theory book, with univalence and higher
inductive types added in an "ad hoc" way on top of intensional
Martin-Lof type theory) is a step forward over systems such as CiC and
MLTT on which Coq and Agda are based, due to various factors such as a
nice treatment of quotients, automatic isomorphism-invariance,
inductive and free constructions, etc.

However, Book HoTT is also a step backwards, because the presence of
non-computational "axioms" means that "execution" gets stuck whenever
you try to use univalence.  So you can prove automatically that
anything true about a group G is true about an isomorphic group H, but
if you then try to take some specific statement about some specific
group G and transfer it to a specific statement about a specific group
H along a specific isomorphism, what you'll get will be an unreadable
statement littered with explicit transports across univalence-induced
paths in the universe, rather than the "real" statement about H that
should be obtained from actually *applying* that specific isomorphism.
(To be fair, plenty of people using a system like Coq pre-HoTT had to
add their own axioms, such as function extensionality and UIP, and
when you want classical logic that's unavoidably an axiom.  But at
least the underlying type theory of Coq and Agda can "compute".)  More
modern homotopy type theories, which are generally based on cubical
structures, allow univalence to be "executed" by the system.  However,
these systems lack (so far) all the intended categorical semantics
(see below), and haven't yet been implemented in "real world" proof
assistants (though there are prototypes now in use and development).

In addition, as Noah mentioned, two-level theories with a stricter
kind of equality (which do *not* exist in UniMath, HoTT/Coq, or
HoTT/Agda -- this point is about having two different equalities on
the same type, not two different classes of types with different
equality behavior) are likely to make many things easier, but haven't
been implemented in real-world proof assistants either (apart from
some sneaky coding with typeclasses).

So overall, I would say that the underlying design of homotopy type
theories is not yet "in order" to achieve its hoped-for maximal
benefit in a proof assistant by the working mathematician, though
there are promising signs and progress is being made.

All the issues discussed above are what I would call "mathematical",
or perhaps more broadly "theoretical".  But a separate issue standing
in the way of wider use of proof assistants is what I would call
"engineering".  No matter how fancy we make the underlying formal
system, I believe it will always remain true (for the foreseeable
future) that a proof assistant needs a lot more detailed information
than an ordinary mathematician would care to provide, or need to see,
in writing and understanding a proof.  This is where we need things
like tactics, implicit arguments, elaboration, proof automation, etc.
to fill in the gaps and make the system usable in practice.  Here
there's been a lot of progress over the past decades, but I think
there's a long way to go too, and choosing a better underlying
foundation (like any form of HoTT, cubical or otherwise) may improve
things a bit but is not really a game-changer.

However, there's something completely different that I do believe has
the potential to be a game-changer.  There's already a very different
"gigantic wave crashing through mathematics": homotopy theory and
higher category theory.  Homotopy type theory gives type theory and
formalization the potential to ride that wave.  The real point here is
that when something is formalized in type theory -- constructively --
it is automatically true internally in all models of type theory, and
for homotopy type theory those models include higher categories.  Note
that the use of constructive logic has nothing to do with any
philosophical belief; classical logic can still be "true" in the "real
world", and yet constructive reasoning is valuable because it makes a
theorem true internally in more categories.

I think it's fairly hopeless to convince a classical mathematician
that they should put in a lot of work to convince a computer of the
truth of *something they already knew*.  But I have much more hope of
convincing them that they should tweak their proofs slightly, and
perhaps use a computer to help verify the validity of the tweaks, in
order that *essentially the same proof* will allow them to conclude a
*vastly more general theorem*.  Moreover, when working with higher
categories the advantage is even more pronounced, because homotopy
type theories introduce a totally new kind of proof that can be much
simpler than all the previously available options -- and the immediate
feedback involved in using a proof assistant is one of the best ways
to *learn* that style of proof.

In short, I think there's a huge public relations opportunity here for
type theory and computer formalization, which sadly even Voevodsky
missed out on.  Rather than selling it as a way to be absolutely sure
of proofs we already believe in (as important as that might be), we
should sell it as a framework for *entirely new proofs* that bring the
otherwise fiendishly complicated and technical world of higher
category theory "down to earth".  The experts in higher category
theory are familiar with the fact that in many respects it is "more
natural" and "better behaved" than ordinary category theory; but there
are thick barriers to entry preventing many of us from getting to that
point of expertise.  With synthetic mathematics in homotopy type
theory, we can envision one day teaching higher category theory to
undergraduates.

--
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/CAOvivQx_b2QkEL-HqMXQNJ_QA83KjdAnFe7RmmiPRRQX6tYk-A%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/8C57894C7413F04A98DDF5629FEC90B15872D76E%40Pli.gst.uqam.ca.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-28 10:22                       ` Michael Shulman
@ 2019-05-29 19:04                         ` Martín Hötzel Escardó
  2019-05-30 17:14                           ` Michael Shulman
  0 siblings, 1 reply; 31+ messages in thread
From: Martín Hötzel Escardó @ 2019-05-29 19:04 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 2167 bytes --]

 Thanks for this discussion. I like it. 

Maybe I would like to argue with this point:

On 28/05/2019 10:50, Michael Shulman wrote:
> I think it's fairly hopeless to convince a classical mathematician
> that they should put in a lot of work to convince a computer of the
> truth of *something they already knew*.

I am not sure why the person who started this thread, a mathematician,
Kevin Buzzard, decided to put in such a lot of work, but did and he
has (in Lean), with his students.

But having interacted with a lot of students (from my institution, and
from everywhere in the world, from maths, logic, computer science and
philosophy departments (and once even a high school student in the
UniMath School)), what I can say is that they are not trying to
convince the computer. 

They are trying to convince themselves, using the computer to both 
check their understanding and record their understanding when 
the proof is complete.

If I am allowed to speak for myself, I created a univalent library in
Agda for the purpose of *doing something else*. However, it is nice to
stare at the library and see everything developed from first
principles. When presented with the mathematical literature, both as
students and experienced mathematicians, we are never sure how far
back one has to read until everything begins in a precise way. How
much have we created, and how do all the different fields of
mathematics interact with each other? When one records mathematics in
the computer, this begins to become clear, or at least the asnwers to such
questions become possible.

We don't need to *convince* anybody. This will *happen*. And it is
already happening. The students like it. This is my experience.

M.


-- 
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/c7197bc2-7fc5-4027-bed6-24b2d350950f%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 2986 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-29 19:04                         ` Martín Hötzel Escardó
@ 2019-05-30 17:14                           ` Michael Shulman
  2019-06-02 17:49                             ` Kevin Buzzard
  0 siblings, 1 reply; 31+ messages in thread
From: Michael Shulman @ 2019-05-30 17:14 UTC (permalink / raw)
  To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory

Thanks Martin!  Of course you are right that there are people who
don't need to be convinced and who derive benefit and pleasure from
their formalization efforts, and in our community we probably
encounter a lot of them.  However, I still maintain that the *average*
working mathematician is not yet going to find such work useful or
rewarding for its own sake.  If you go to, say, the U.S. Joint
Mathematics Meetings and stop a hundred mathematicians at random in
the lobby and ask whether they have ever formalized their work in a
proof assistant, how many do you think will say yes?

Perhaps I am too pessimistic.  But let me in turn offer myself as an
example: in addition to being a homotopy type theorist, I have another
hat as a classical category theorist and homotopy theorist.  When I
prove things in HoTT, I often formalize them in a proof assistant.
But when I prove things in classical mathematics, I very rarely
consider formalizing them.  Only once have I formalized a proof in
classical category theory; the experience was more time-consuming and
less enjoyable than I expected, and I have no plans to do it again.
And I expect that as classical mathematicians go, I am (even when I
have my classical mathematician hat on) pretty far on the
sympathetic-to-formalization side of the spectrum.



On Wed, May 29, 2019 at 12:05 PM Martín Hötzel Escardó
<escardo.martin@gmail.com> wrote:
>
>  Thanks for this discussion. I like it.
>
> Maybe I would like to argue with this point:
>
> On 28/05/2019 10:50, Michael Shulman wrote:
> > I think it's fairly hopeless to convince a classical mathematician
> > that they should put in a lot of work to convince a computer of the
> > truth of *something they already knew*.
>
> I am not sure why the person who started this thread, a mathematician,
> Kevin Buzzard, decided to put in such a lot of work, but did and he
> has (in Lean), with his students.
>
> But having interacted with a lot of students (from my institution, and
> from everywhere in the world, from maths, logic, computer science and
> philosophy departments (and once even a high school student in the
> UniMath School)), what I can say is that they are not trying to
> convince the computer.
>
> They are trying to convince themselves, using the computer to both
> check their understanding and record their understanding when
> the proof is complete.
>
> If I am allowed to speak for myself, I created a univalent library in
> Agda for the purpose of *doing something else*. However, it is nice to
> stare at the library and see everything developed from first
> principles. When presented with the mathematical literature, both as
> students and experienced mathematicians, we are never sure how far
> back one has to read until everything begins in a precise way. How
> much have we created, and how do all the different fields of
> mathematics interact with each other? When one records mathematics in
> the computer, this begins to become clear, or at least the asnwers to such
> questions become possible.
>
> We don't need to *convince* anybody. This will *happen*. And it is
> already happening. The students like it. This is my experience.
>
> M.
>
>
> --
> 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/c7197bc2-7fc5-4027-bed6-24b2d350950f%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/CAOvivQxAZEXiCSS5%2BipOszo%3DJeymDXL3jyfuNFdY7AKxAZSS4g%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  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
  1 sibling, 1 reply; 31+ messages in thread
From: Bas Spitters @ 2019-06-02 16:30 UTC (permalink / raw)
  To: Kevin Buzzard; +Cc: Noah Snyder, Homotopy Type Theory, Juan Ospina

[-- Attachment #1: Type: text/plain, Size: 23912 bytes --]

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-isomorphism/
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-isomorphism-is-equality.pdf

Have you looked at any of this? Does it provide what you are looking for?

Best,

Bas

On Sun, May 26, 2019 at 7:00 PM Kevin Buzzard <kevin.m.buzzard@gmail.com>
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 <b.a.w.spitters@gmail.com>
> 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 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 <kevin.m.buzzard@gmail.com>
> 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 +
> impredicative 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 more 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 just a matter of writing some incantation at the top of a file
> and then not thinking 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, but don't use these commands or these tactics"),
> which maybe raises the entry barrier for mathematicians a bit (and speaking
> from personal experience, already this entry barrier is quite high). High
> level tactics are absolutely crucial for mathematical Lean users. This is
> one of the reasons that the Lean 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 calculations 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 possible I
> am becoming convinced that it can really change mathematics. In my
> experience the biggest obstruction to it changing mathematics is simply
> that mathematicians 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 this stuff works. In short, I think type theory has an image
> problem. Sure there are category theorists who know about it, but how many
> category theorists 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 would love to draw the mathematics and computer science
> communities closer together over ideas like this, but it's hard work. I am
> wondering whether developing accessible databases of undergraduate level
> mathematics would at least 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 weekend I've learnt something about UniMath, but
> whilst it might do bicategories very well (which are not on our
> undergraduate curriculum), where is the basic 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 have schemes. I know that Gonthier
> and his coauthors had to make a lot of undergraduate level maths (Galois
> theory, algebraic number theory, group theory) 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 formalisation when
> you're trying to sell to "normal research mathematicians", and I don't know
> what is. I'm now wondering making formalised undergraduate mathematics more
> accessible to untrained mathematicians is a better approach, but who knows.
> Obviously "AI which can solve the Riemann hypothesis" will 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 bunch
> of extremely smart people, both mathematicians and computer scientists,
> have invested a lot of time in thinking about how to do mathematics with
> type theory. I find it very frustrating that mathematicians are not
> beginning to notice. Of course there are exceptions. One day though -- will
> there simply be a gigantic wave which crashes through mathematics and
> forces mathematicians 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 <b.a.w.spitters@gmail.com>
> wrote:
> > >>
> > >> There has been progress in making a cleaner interface with the
> standard 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 future.
> > >> 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
> connection 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, there'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
> currently published in the Annals.
> > >>
> > >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com>
> wrote:
> > >>>
> > >>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a
> category from “Coq with the indices-matter option plus the HoTT library."
>  “Coq with the indices-matter option plus the 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 can
> 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 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* tactics
> are available in Coq+indices-matter+HoTT, but not many of the more advanced
> ones, and to my knowledge, not tactics needed for complicated homotopical
> 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 assumed
> 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, “Coq 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
> does 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 categories 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 <
> kevin.m.buzzard@gmail.com> 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,
> "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 <nsnyder@gmail.com>
> wrote:
> > >>>>>
> > >>>>> I’d also imagine that a “practical” implementation would likely
> have some kind of “two-level” type theory where you can use types that
> behave classically when that’s better and HoTT types when that’s 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
> "faithfully", 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
> type theory this is going to involve annoying book-keeping which it seems
> like you’d 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
> mathematician "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 using which cannot deduce this immediately. As an interesting
> experiment, find your 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 will be very confident that this is true, even if they do not
> know the definition; 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 make
> 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 for
> "the way mathematicians think". However now I've looked over what has
> currently been formalised in UniMath I am wondering whether there are pain
> points 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
> semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can
> assume both algebras are multimatrix algebras over division rings.”  Is
> that step something you’d be able to deal with easily in Lean?  If not,
> that’s somewhere that down the line HoTT might make things more practical.
> > >>>>
> > >>>>
> > >>>> This is a great example! To be honest I am slightly confused about
> 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 development)
> 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’re making a category error in
> your question.  HoTT is an abstract type theory, not a proof assistant.
> > >>>>>
> > >>>>> Best,
> > >>>>>
> > >>>>> Noah
> > >>>>>
> > >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com>
> 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 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’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....@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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%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-hmwRsr1iwztPg%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/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3A%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/CAOoPQuT4kJr4cr8rqS2kMjNkQyj6rj8CxChXx82rWcapXtRDxQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 30796 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-05-30 17:14                           ` Michael Shulman
@ 2019-06-02 17:49                             ` Kevin Buzzard
  2019-06-04 20:50                               ` Martín Hötzel Escardó
  0 siblings, 1 reply; 31+ messages in thread
From: Kevin Buzzard @ 2019-06-02 17:49 UTC (permalink / raw)
  To: Michael Shulman
  Cc: Martín Hötzel Escardó, Homotopy Type Theory

On Thu, 30 May 2019 at 18:14, Michael Shulman <shulman@sandiego.edu> wrote:
>
> Thanks Martin!  Of course you are right that there are people who
> don't need to be convinced and who derive benefit and pleasure from
> their formalization efforts, and in our community we probably
> encounter a lot of them.  However, I still maintain that the *average*
> working mathematician is not yet going to find such work useful or
> rewarding for its own sake.  If you go to, say, the U.S. Joint
> Mathematics Meetings and stop a hundred mathematicians at random in
> the lobby and ask whether they have ever formalized their work in a
> proof assistant, how many do you think will say yes?

I think this is absolutely right, and an important point. We can even
go further: ask 100 mathematicians whether they have ever formalised
*anything at all* in a proof assistant, and only epsilon will say yes.
This is why I am focussing on the undergraduates. What we as a
community can offer undergraduates is a guarantee that a proof is
correct; one could regard this as "instant feedback". I think it is
currently very difficult to answer the question I've been asked by
several staff members -- "what is in it for me"? Some people might
find this a negative approach, but if computer proof systems are
introduced in undergraduate curricula, and the response to the
question "what is the point of teaching these people type theory?" can
be something like this: "what is the point of teaching them Banach
spaces? Some will use it later on, many won't. Many students graduate,
leave mathematics, and never really use these high-powered objects
again. For those people, a course on type theory will teach them just
as much as a course on Banach spaces -- it will just give them another
domain where they can reason logically, learn some easy theorems,
learn some deeper results, etc. Oh, and there's evidence that one day
type theory will change the world in a way that Banach spaces probably
will not". This is the line I am going to take in a couple of years'
time when we are discussing changes to my university's curriculum.

And then in a generation's time, one can hope that more than epsilon
will say yes. Mathematical culture sometimes changes very slowly. We
might be using different systems but I still believe that we are
looking at the future, and if the current staff can't see it then we
have to work on the future staff. The problem I find with this evil
plan for world domination is that most senior people I talk to (across
all of these systems) tend not to be employed by maths departments.
This is a different issue, which needs different ideas, but those are
really orthogonal to this conversation. The thing I know for sure is
that there are modern maths undergraduates who grew up with computer
games and who find the idea of turning their example sheet questions
into levels of a computer game quite appealing.

Kevin


>
> Perhaps I am too pessimistic.  But let me in turn offer myself as an
> example: in addition to being a homotopy type theorist, I have another
> hat as a classical category theorist and homotopy theorist.  When I
> prove things in HoTT, I often formalize them in a proof assistant.
> But when I prove things in classical mathematics, I very rarely
> consider formalizing them.  Only once have I formalized a proof in
> classical category theory; the experience was more time-consuming and
> less enjoyable than I expected, and I have no plans to do it again.
> And I expect that as classical mathematicians go, I am (even when I
> have my classical mathematician hat on) pretty far on the
> sympathetic-to-formalization side of the spectrum.
>
>
>
> On Wed, May 29, 2019 at 12:05 PM Martín Hötzel Escardó
> <escardo.martin@gmail.com> wrote:
> >
> >  Thanks for this discussion. I like it.
> >
> > Maybe I would like to argue with this point:
> >
> > On 28/05/2019 10:50, Michael Shulman wrote:
> > > I think it's fairly hopeless to convince a classical mathematician
> > > that they should put in a lot of work to convince a computer of the
> > > truth of *something they already knew*.
> >
> > I am not sure why the person who started this thread, a mathematician,
> > Kevin Buzzard, decided to put in such a lot of work, but did and he
> > has (in Lean), with his students.
> >
> > But having interacted with a lot of students (from my institution, and
> > from everywhere in the world, from maths, logic, computer science and
> > philosophy departments (and once even a high school student in the
> > UniMath School)), what I can say is that they are not trying to
> > convince the computer.
> >
> > They are trying to convince themselves, using the computer to both
> > check their understanding and record their understanding when
> > the proof is complete.
> >
> > If I am allowed to speak for myself, I created a univalent library in
> > Agda for the purpose of *doing something else*. However, it is nice to
> > stare at the library and see everything developed from first
> > principles. When presented with the mathematical literature, both as
> > students and experienced mathematicians, we are never sure how far
> > back one has to read until everything begins in a precise way. How
> > much have we created, and how do all the different fields of
> > mathematics interact with each other? When one records mathematics in
> > the computer, this begins to become clear, or at least the asnwers to such
> > questions become possible.
> >
> > We don't need to *convince* anybody. This will *happen*. And it is
> > already happening. The students like it. This is my experience.
> >
> > M.
> >
> >
> > --
> > 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/c7197bc2-7fc5-4027-bed6-24b2d350950f%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/CAOvivQxAZEXiCSS5%2BipOszo%3DJeymDXL3jyfuNFdY7AKxAZSS4g%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/CAH52Xb0SKwTaKtkBdZgav3KPkrqGs-eYae11v103ErYU%3D2dCRQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-06-02 16:30                   ` Bas Spitters
@ 2019-06-02 17:55                     ` Kevin Buzzard
  2019-06-02 20:46                       ` Nicola Gambino
  2019-06-04 20:32                       ` Michael Shulman
  0 siblings, 2 replies; 31+ messages in thread
From: Kevin Buzzard @ 2019-06-02 17:55 UTC (permalink / raw)
  To: Bas Spitters; +Cc: Noah Snyder, Homotopy Type Theory, Juan Ospina

On Sun, 2 Jun 2019 at 17:30, Bas Spitters <b.a.w.spitters@gmail.com> 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-isomorphism/
> 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-isomorphism-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 "=" 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 <kevin.m.buzzard@gmail.com> 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 <b.a.w.spitters@gmail.com> 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 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 <kevin.m.buzzard@gmail.com> 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 + impredicative 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 more 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 just a matter of writing some incantation at the top of a file and then not thinking 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, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean 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 calculations 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 possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians 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 this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists 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 would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least 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 weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic 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 have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) 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 formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will 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 bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians 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 <b.a.w.spitters@gmail.com> wrote:
>> > >>
>> > >> There has been progress in making a cleaner interface with the standard 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 future.
>> > >> 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 connection 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, there'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 currently published in the Annals.
>> > >>
>> > >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote:
>> > >>>
>> > >>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library."   “Coq with the indices-matter option plus the 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 can 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 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* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical 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 assumed 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, “Coq 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 does 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 categories 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 <kevin.m.buzzard@gmail.com> 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, "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 <nsnyder@gmail.com> wrote:
>> > >>>>>
>> > >>>>> I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s 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 "faithfully", 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 type theory this is going to involve annoying book-keeping which it seems like you’d 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 mathematician "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 using which cannot deduce this immediately. As an interesting experiment, find your 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 will be very confident that this is true, even if they do not know the definition; 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 make 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 for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points 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 semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.”  Is that step something you’d be able to deal with easily in Lean?  If not, that’s somewhere that down the line HoTT might make things more practical.
>> > >>>>
>> > >>>>
>> > >>>> This is a great example! To be honest I am slightly confused about 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 development) 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’re making a category error in your question.  HoTT is an abstract type theory, not a proof assistant.
>> > >>>>>
>> > >>>>> Best,
>> > >>>>>
>> > >>>>> Noah
>> > >>>>>
>> > >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> 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 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’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....@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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%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-hmwRsr1iwztPg%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/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3A%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/CAH52Xb0XD3F9%3DXc2eHZDAyFHQ-3e%2BHUXc7kRTp_%2BvhzBPVx-8g%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  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
  1 sibling, 1 reply; 31+ messages in thread
From: Nicola Gambino @ 2019-06-02 20:46 UTC (permalink / raw)
  To: Kevin Buzzard
  Cc: Bas Spitters, Noah Snyder, Homotopy Type Theory, Juan Ospina

Hi,

> On 2 Jun 2019, at 18:55, Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote:
> 
> 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 "=" 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.

I am under the impression that all isomorphisms that are definable within DTT/HoTT/UF are canonical isomorphisms, by which I informally mean that they are definable only by means of the universal properties characterizing the objects under consideration.

This is based on the well-known observation that type theories often describe the free category with a certain kind of structure. 

Perhaps someone for whom it is not 21:45 on a Sunday can turn this impression into a theorem or correct it. 

If the impression is correct, then HoTT/UF is the half-way house (whose structural safety is supported by various models of univalence) and the mathematicians who work informally mixing equality and canonical isomorphisms are more extreme (and potentially inconsistent).  

With best wishes,
Nicola

-- 
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/29FFF023-0DB7-4E09-8A77-B4F1C2730203%40leeds.ac.uk.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-06-02 20:46                       ` Nicola Gambino
@ 2019-06-02 20:59                         ` Valery Isaev
  0 siblings, 0 replies; 31+ messages in thread
From: Valery Isaev @ 2019-06-02 20:59 UTC (permalink / raw)
  To: Nicola Gambino; +Cc: Homotopy Type Theory

[-- Attachment #1: Type: text/plain, Size: 3100 bytes --]

This brings an old question of what is a canonical isomorphism
<https://mathoverflow.net/questions/19644/what-is-the-definition-of-canonical>.
To give a simple example in the realm of HoTT, consider isomorphisms
between S^1 and S^1. There is a "canonical" isomorphism, the identity, but
there are many others. Are they less canonical? You can transport stuff
along any of them, so they are not any less canonical from this perspective.

Regards,
Valery Isaev


вс, 2 июн. 2019 г. в 23:47, Nicola Gambino <N.Gambino@leeds.ac.uk>:

> Hi,
>
> > On 2 Jun 2019, at 18:55, Kevin Buzzard <kevin.m.buzzard@gmail.com>
> wrote:
> >
> > 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 "=" 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.
>
> I am under the impression that all isomorphisms that are definable within
> DTT/HoTT/UF are canonical isomorphisms, by which I informally mean that
> they are definable only by means of the universal properties characterizing
> the objects under consideration.
>
> This is based on the well-known observation that type theories often
> describe the free category with a certain kind of structure.
>
> Perhaps someone for whom it is not 21:45 on a Sunday can turn this
> impression into a theorem or correct it.
>
> If the impression is correct, then HoTT/UF is the half-way house (whose
> structural safety is supported by various models of univalence) and the
> mathematicians who work informally mixing equality and canonical
> isomorphisms are more extreme (and potentially inconsistent).
>
> With best wishes,
> Nicola
>
> --
> 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/29FFF023-0DB7-4E09-8A77-B4F1C2730203%40leeds.ac.uk
> .
> 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/CAA520fs2MiSPAKkdyhOnqBSdqPw%2BhYCFL-6QRNAjobP-xKTkKA%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 4504 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-06-02 17:55                     ` Kevin Buzzard
  2019-06-02 20:46                       ` Nicola Gambino
@ 2019-06-04 20:32                       ` Michael Shulman
  2019-06-04 20:58                         ` Kevin Buzzard
  2019-06-06 16:30                         ` Matt Oliveri
  1 sibling, 2 replies; 31+ messages in thread
From: Michael Shulman @ 2019-06-04 20:32 UTC (permalink / raw)
  To: Kevin Buzzard; +Cc: Homotopy Type Theory

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 <kevin.m.buzzard@gmail.com> wrote:
>
> On Sun, 2 Jun 2019 at 17:30, Bas Spitters <b.a.w.spitters@gmail.com> 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-isomorphism/
> > 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-isomorphism-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 "=" 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 <kevin.m.buzzard@gmail.com> 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 <b.a.w.spitters@gmail.com> 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 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 <kevin.m.buzzard@gmail.com> 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 + impredicative 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 more 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 just a matter of writing some incantation at the top of a file and then not thinking 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, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean 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 calculations 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 possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians 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 this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists 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 would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least 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 weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic 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 have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) 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 formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will 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 bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians 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 <b.a.w.spitters@gmail.com> wrote:
> >> > >>
> >> > >> There has been progress in making a cleaner interface with the standard 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 future.
> >> > >> 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 connection 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, there'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 currently published in the Annals.
> >> > >>
> >> > >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote:
> >> > >>>
> >> > >>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library."   “Coq with the indices-matter option plus the 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 can 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 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* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical 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 assumed 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, “Coq 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 does 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 categories 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 <kevin.m.buzzard@gmail.com> 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, "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 <nsnyder@gmail.com> wrote:
> >> > >>>>>
> >> > >>>>> I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s 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 "faithfully", 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 type theory this is going to involve annoying book-keeping which it seems like you’d 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 mathematician "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 using which cannot deduce this immediately. As an interesting experiment, find your 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 will be very confident that this is true, even if they do not know the definition; 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 make 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 for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points 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 semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.”  Is that step something you’d be able to deal with easily in Lean?  If not, that’s somewhere that down the line HoTT might make things more practical.
> >> > >>>>
> >> > >>>>
> >> > >>>> This is a great example! To be honest I am slightly confused about 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 development) 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’re making a category error in your question.  HoTT is an abstract type theory, not a proof assistant.
> >> > >>>>>
> >> > >>>>> Best,
> >> > >>>>>
> >> > >>>>> Noah
> >> > >>>>>
> >> > >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> 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 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’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....@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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%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-hmwRsr1iwztPg%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/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3A%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/CAH52Xb0XD3F9%3DXc2eHZDAyFHQ-3e%2BHUXc7kRTp_%2BvhzBPVx-8g%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/CAOvivQzFBjtA33McF1nAerfcnFRbnWLAw73-F3GPBumbVqetag%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-06-02 17:49                             ` Kevin Buzzard
@ 2019-06-04 20:50                               ` Martín Hötzel Escardó
  2019-06-05 17:11                                 ` Thorsten Altenkirch
  0 siblings, 1 reply; 31+ messages in thread
From: Martín Hötzel Escardó @ 2019-06-04 20:50 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 1025 bytes --]



On Sunday, 2 June 2019 18:49:30 UTC+1, Kevin Buzzard wrote:
>
> The thing I know for sure is 
> that there are modern maths undergraduates who grew up with computer 
> games and who find the idea of turning their example sheet questions 
> into levels of a computer game quite appealing. 
>
>
I am surprised that Thorsten Altenkirch didn't manifest himself at this 
point. He uses to say that you can't teach old dogs new tricks. 

I am not sure it is the computer games (it could be, and if not they could 
anyway help, perhaps). I think it is their open minds.

Martin

-- 
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/209e2262-cb8a-4b31-9b6b-44a5df0185a5%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 1617 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-06-04 20:32                       ` Michael Shulman
@ 2019-06-04 20:58                         ` Kevin Buzzard
  2019-06-06 16:30                         ` Matt Oliveri
  1 sibling, 0 replies; 31+ messages in thread
From: Kevin Buzzard @ 2019-06-04 20:58 UTC (permalink / raw)
  To: Michael Shulman; +Cc: Homotopy Type Theory

The Langlandsy folk (of whom I am one, I guess) sometimes use
"canonical" in a completely different way :-/ Randomly googling led me
to

https://mathoverflow.net/questions/127691/reconciling-lusztigs-results-with-the-langlands-philosophy

(and I'm sure there are other examples -- I've even used it in my own
work) where "canonical" is being used to describe a bijection between
two sets. This is the thing I've referred to as "mission creep".
Everyone thinking about functors and natural transformations etc --
all of these thoughts come to nothing when faced with the assertion
that the Langlands correspondence is "canonical". What I believe the
word means in that context is "this bijection of sets satisfies a
whole bunch of cool properties, and I reserve the right to add to this
list of cool properties in the future". This usage of the word has
bothered me for years. When Gee and I were trying to write down a
precise statement of local Langlands functoriality we ran into this;
different experts seemed to have slightly different lists. When we
were doing calculations we ran into a property which wasn't on any of
the lists we'd seen, but which we wanted to be true, and we asked
about whether this property was expected to be true in general, and/or
was proved in any of the cases where the local Langlands conjectures
were theorems. David Vogan said that indeed it should be on the list
and even sketched a proof that it was true in the case of real and
complex groups for us; other experts had not seen it before. At that
time it really did feel like "canonical" was the same as "magical";
the more questions you asked, the more beautiful it got. The notion
was completely unformalisable. One day someone might discover some
elusive Tannakian category structure on some set of automorphic
representations and all of a sudden the word might acquire some formal
meaning, but until then this usage of the word remains a complete
mystery to me -- I guess it may as well simply be replaced with the
word "mysterious" or "beautiful" or something which is clearly not
meant to be definable.

As for the other issue, it would be easier to discuss if there were
some formalisation of the proof that the structure presheaf on the
spectrum of a commutative ring was a sheaf, in one of these HoTT
systems. As far as I know this has not yet been done. Part of me wants
to encourage the HoTT community to try formalising this statement ("an
affine scheme is a scheme", if you like) in some HoTT proof
verification system. Of course I could try doing it myself in Lean
HoTT but I know I'll never get round to it. There is some subtlety
here, which I am still perhaps doing a poor job of explaining. It all
boils down to this very sneaky use of "=" in EGA.

Kevin

On Tue, 4 Jun 2019 at 21:32, Michael Shulman <shulman@sandiego.edu> wrote:
>
> 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 <kevin.m.buzzard@gmail.com> wrote:
> >
> > On Sun, 2 Jun 2019 at 17:30, Bas Spitters <b.a.w.spitters@gmail.com> 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-isomorphism/
> > > 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-isomorphism-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 "=" 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 <kevin.m.buzzard@gmail.com> 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 <b.a.w.spitters@gmail.com> 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 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 <kevin.m.buzzard@gmail.com> 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 + impredicative 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 more 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 just a matter of writing some incantation at the top of a file and then not thinking 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, but don't use these commands or these tactics"), which maybe raises the entry barrier for mathematicians a bit (and speaking from personal experience, already this entry barrier is quite high). High level tactics are absolutely crucial for mathematical Lean users. This is one of the reasons that the Lean 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 calculations 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 possible I am becoming convinced that it can really change mathematics. In my experience the biggest obstruction to it changing mathematics is simply that mathematicians 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 this stuff works. In short, I think type theory has an image problem. Sure there are category theorists who know about it, but how many category theorists 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 would love to draw the mathematics and computer science communities closer together over ideas like this, but it's hard work. I am wondering whether developing accessible databases of undergraduate level mathematics would at least 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 weekend I've learnt something about UniMath, but whilst it might do bicategories very well (which are not on our undergraduate curriculum), where is the basic 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 have schemes. I know that Gonthier and his coauthors had to make a lot of undergraduate level maths (Galois theory, algebraic number theory, group theory) 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 formalisation when you're trying to sell to "normal research mathematicians", and I don't know what is. I'm now wondering making formalised undergraduate mathematics more accessible to untrained mathematicians is a better approach, but who knows. Obviously "AI which can solve the Riemann hypothesis" will 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 bunch of extremely smart people, both mathematicians and computer scientists, have invested a lot of time in thinking about how to do mathematics with type theory. I find it very frustrating that mathematicians are not beginning to notice. Of course there are exceptions. One day though -- will there simply be a gigantic wave which crashes through mathematics and forces mathematicians 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 <b.a.w.spitters@gmail.com> wrote:
> > >> > >>
> > >> > >> There has been progress in making a cleaner interface with the standard 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 future.
> > >> > >> 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 connection 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, there'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 currently published in the Annals.
> > >> > >>
> > >> > >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder <nsnyder@gmail.com> wrote:
> > >> > >>>
> > >> > >>> UniMath vs HoTT wasn’t exactly my point, UniMath = Book-HoTT is of a category from “Coq with the indices-matter option plus the HoTT library."   “Coq with the indices-matter option plus the 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 can 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 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* tactics are available in Coq+indices-matter+HoTT, but not many of the more advanced ones, and to my knowledge, not tactics needed for complicated homotopical 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 assumed 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, “Coq 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 does 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 categories 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 <kevin.m.buzzard@gmail.com> 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, "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 <nsnyder@gmail.com> wrote:
> > >> > >>>>>
> > >> > >>>>> I’d also imagine that a “practical” implementation would likely have some kind of “two-level” type theory where you can use types that behave classically when that’s better and HoTT types when that’s 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 "faithfully", 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 type theory this is going to involve annoying book-keeping which it seems like you’d 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 mathematician "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 using which cannot deduce this immediately. As an interesting experiment, find your 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 will be very confident that this is true, even if they do not know the definition; 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 make 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 for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points 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 semisimple rings whose proof starts “wlog, by Artin-Wedderburn, we can assume both algebras are multimatrix algebras over division rings.”  Is that step something you’d be able to deal with easily in Lean?  If not, that’s somewhere that down the line HoTT might make things more practical.
> > >> > >>>>
> > >> > >>>>
> > >> > >>>> This is a great example! To be honest I am slightly confused about 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 development) 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’re making a category error in your question.  HoTT is an abstract type theory, not a proof assistant.
> > >> > >>>>>
> > >> > >>>>> Best,
> > >> > >>>>>
> > >> > >>>>> Noah
> > >> > >>>>>
> > >> > >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> 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 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’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....@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/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%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-hmwRsr1iwztPg%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/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3A%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/CAH52Xb0XD3F9%3DXc2eHZDAyFHQ-3e%2BHUXc7kRTp_%2BvhzBPVx-8g%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/CAH52Xb0v2jbutOG7bfgroYn%2B3HdD_rWtz9BC505fH1NdpnLzrQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-06-04 20:50                               ` Martín Hötzel Escardó
@ 2019-06-05 17:11                                 ` Thorsten Altenkirch
  0 siblings, 0 replies; 31+ messages in thread
From: Thorsten Altenkirch @ 2019-06-05 17:11 UTC (permalink / raw)
  To: Martín Hötzel Escardó, Homotopy Type Theory

[-- Attachment #1: Type: text/plain, Size: 2975 bytes --]

Sees my name was mentioned (says the devil).

Computer games are the perfect analogy. You are fighting a proof and once you have done it you reach the next level. But then there is still the boss lemma to be defeated.

When I started using Type Theory using Randy Pollack’s LEGO system ages ago, I was playing nethack at the same time. The similarity of the two activities was intriguing (also both were entirely ASCII based). Also you can still to formal proofs when tired and or drunk. But you can’t do paper maths.

Thorsten

From: <homotopytypetheory@googlegroups.com> on behalf of Martín Hötzel Escardó <escardo.martin@gmail.com>
Date: Tuesday, 4 June 2019 at 21:51
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] doing "all of pure mathematics" in type theory



On Sunday, 2 June 2019 18:49:30 UTC+1, Kevin Buzzard wrote:
The thing I know for sure is
that there are modern maths undergraduates who grew up with computer
games and who find the idea of turning their example sheet questions
into levels of a computer game quite appealing.

I am surprised that Thorsten Altenkirch didn't manifest himself at this point. He uses to say that you can't teach old dogs new tricks.

I am not sure it is the computer games (it could be, and if not they could anyway help, perhaps). I think it is their open minds.

Martin

--
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<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/209e2262-cb8a-4b31-9b6b-44a5df0185a5%40googlegroups.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/209e2262-cb8a-4b31-9b6b-44a5df0185a5%40googlegroups.com?utm_medium=email&utm_source=footer>.
For more options, visit https://groups.google.com/d/optout.




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-- 
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/38C01A88-302F-4DA0-91CB-8411B4F595A0%40nottingham.ac.uk.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 6738 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: [HoTT] doing "all of pure mathematics" in type theory
  2019-06-04 20:32                       ` Michael Shulman
  2019-06-04 20:58                         ` Kevin Buzzard
@ 2019-06-06 16:30                         ` Matt Oliveri
  1 sibling, 0 replies; 31+ messages in thread
From: Matt Oliveri @ 2019-06-06 16:30 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 1812 bytes --]

I don't think implicit coercions fully handle the problem Kevin's talking 
about with the way "canonical isomorphisms" are used. It sounds like 
canonical isomorphisms are supposed to have a ton of coherences which are 
"obvious", so you can treat canonically isomorphic structures as if they 
are strictly equal. With implicit coercions, (in e.g. Coq) the transport 
isn't written, but it can still mess things up if you don't have the 
coherences you expected. And even if you do have the coherences you need, 
implicit coercions does not arrange to apply them automatically.

I'm reminded of Guillaume's thought from his HoTTEST talk, to have some 
kind of proof automation that makes it look as if a path is a judgmental 
equality, by automatically using the necessary coherences.

On Tuesday, June 4, 2019 at 4:32:31 PM UTC-4, Michael Shulman wrote:
>
> 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. 
>
>

-- 
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/1b8a8efe-ac71-44e1-9131-96dc2c445768%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 2389 bytes --]

^ permalink raw reply	[flat|nested] 31+ messages in thread

end of thread, other threads:[~2019-06-06 16:30 UTC | newest]

Thread overview: 31+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-05-25 10:12 [HoTT] doing "all of pure mathematics" in type theory Kevin Buzzard
2019-05-25 10:22 ` Steve Awodey
2019-05-25 12:23   ` Kevin Buzzard
     [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

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).