35 views

Skip to first unread message

May 25, 2019, 6:12:04 AM5/25/19

to Homotopy Type Theory

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

May 25, 2019, 6:22:41 AM5/25/19

to Kevin Buzzard, 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

> --

> 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 HomotopyTypeThe...@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.

the Atiyah-Hirzebruch and Serre spectral sequences for cohomology

in HoTT using Lean:

https://arxiv.org/abs/1808.10690

Regards,

Steve

> 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 HomotopyTypeThe...@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.

May 25, 2019, 8:23:19 AM5/25/19

to Steve Awodey, 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.

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.

May 25, 2019, 9:13:30 AM5/25/19

to Homotopy Type Theory

On Sat, 25 May 2019 at 12:26, Thierry Coquand <Thierry...@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

> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/BFBE1A09-A246-4DAD-8AD2-25C3C517A7FE%40cmu.edu.

>

>

> 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

May 25, 2019, 9:34:55 AM5/25/19

to Homotopy Type Theory

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:

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+unsub...@googlegroups.com.

May 25, 2019, 10:50:27 AM5/25/19

to Juan Ospina, Homotopy Type Theory

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

> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegroups.com.

May 25, 2019, 11:36:45 AM5/25/19

to Noah Snyder, Juan Ospina, Homotopy Type Theory

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 <nsn...@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

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.com.

May 25, 2019, 12:42:02 PM5/25/19

to Kevin Buzzard, Homotopy Type Theory, Juan Ospina

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.

May 26, 2019, 1:50:35 AM5/26/19

to Noah Snyder, Kevin Buzzard, Homotopy Type Theory, Juan Ospina

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:

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwztPg%40mail.gmail.com.

May 26, 2019, 7:41:36 AM5/26/19

to Bas Spitters, Noah Snyder, Homotopy Type Theory, Juan Ospina

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

May 26, 2019, 8:09:58 AM5/26/19

to Kevin Buzzard, 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

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

May 26, 2019, 1:00:21 PM5/26/19

to Bas Spitters, 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.s...@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

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.s...@gmail.com> wrote:

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

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.

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

May 26, 2019, 10:33:45 PM5/26/19

to Homotopy Type Theory

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

) 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

, 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

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

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

May 27, 2019, 4:41:31 AM5/27/19

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

better story for --without-K, and Anders Mörtberg, Andrea Vezzosi and

others have implemented --cubical, with direct support for HITs.

--

/NAD

May 27, 2019, 9:09:16 AM5/27/19

to Bas Spitters, Kevin Buzzard, 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

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/

and is formalized in CIC (Gallina) without axiom ...

> and the analysis library that is currently under development.

> https://github.com/math-comp/analysis

Best wishes,

assia

May 28, 2019, 5:51:05 AM5/28/19

to Kevin Buzzard, 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.

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.

May 28, 2019, 6:13:18 AM5/28/19

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

both univalence and higher inductive types. (As well as things like

higher inductive-coinductive-recursive types that may not have a proper

explanation.)

--

/NAD

May 28, 2019, 6:23:04 AM5/28/19

to Nils Anders Danielsson, 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!

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!

> --

> 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 HomotopyTypeThe...@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.
> 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 HomotopyTypeThe...@googlegroups.com.

May 28, 2019, 11:20:04 AM5/28/19

to Michael Shulman, Kevin Buzzard, 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: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Michael Shulman [shu...@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

--

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 HomotopyTypeThe...@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.

May 29, 2019, 3:04:38 PM5/29/19

to Homotopy Type Theory

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.

May 30, 2019, 1:14:46 PM5/30/19

to Martín Hötzel Escardó, 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.

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.

> --

> 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 HomotopyTypeThe...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/c7197bc2-7fc5-4027-bed6-24b2d350950f%40googlegroups.com.
> 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 HomotopyTypeThe...@googlegroups.com.

Jun 2, 2019, 12:30:15 PM6/2/19

to Kevin Buzzard, Noah Snyder, Homotopy Type Theory, Juan Ospina

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.

This is explained in many places (e.g. the book). Here's an early article explaining it for algebraic structures:

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

Best,

Bas

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb1uvc%3DAA6Pe%3DZ98K-rJ%2BQ1xzLf4LDAwWQhJWW62bO5L3A%40mail.gmail.com.

Jun 2, 2019, 1:49:30 PM6/2/19

to Michael Shulman, Martín Hötzel Escardó, Homotopy Type Theory

On Thu, 30 May 2019 at 18:14, Michael Shulman <shu...@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
>

> 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?

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

Jun 2, 2019, 1:56:04 PM6/2/19

to Bas Spitters, Noah Snyder, Homotopy Type Theory, Juan Ospina

On Sun, 2 Jun 2019 at 17:30, Bas Spitters <b.a.w.s...@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
>

> 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?

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

Jun 2, 2019, 4:47:14 PM6/2/19

to Kevin Buzzard, Bas Spitters, Noah Snyder, Homotopy Type Theory, Juan Ospina

Hi,

> On 2 Jun 2019, at 18:55, Kevin Buzzard <kevin.m...@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

> On 2 Jun 2019, at 18:55, Kevin Buzzard <kevin.m...@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.

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

Jun 2, 2019, 5:00:20 PM6/2/19

to Nicola Gambino, Homotopy Type Theory

This brings an old question of what is a canonical isomorphism. 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.Ga...@leeds.ac.uk>:

--

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 HomotopyTypeThe...@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.

Jun 4, 2019, 4:32:31 PM6/4/19

to Kevin Buzzard, 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.

> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb0XD3F9%3DXc2eHZDAyFHQ-3e%2BHUXc7kRTp_%2BvhzBPVx-8g%40mail.gmail.com.

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

Jun 4, 2019, 4:50:47 PM6/4/19

to Homotopy 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