doing "all of pure mathematics" in type theory

35 views
Skip to first unread message

Kevin Buzzard

unread,
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

Steve Awodey

unread,
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.

Kevin Buzzard

unread,
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.

Kevin Buzzard

unread,
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.

Juan Ospina

unread,
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:

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

Noah Snyder

unread,
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.

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

Kevin Buzzard

unread,
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


Noah Snyder

unread,
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.

Bas Spitters

unread,
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.

Kevin Buzzard

unread,
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

Bas Spitters

unread,
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

Kevin Buzzard

unread,
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

Daniel R. Grayson

unread,
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


Nils Anders Danielsson

unread,
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
better story for --without-K, and Anders Mörtberg, Andrea Vezzosi and
others have implemented --cubical, with direct support for HITs.

--
/NAD

Assia Mahboubi

unread,
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

Michael Shulman

unread,
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.

Nils Anders Danielsson

unread,
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
both univalence and higher inductive types. (As well as things like
higher inductive-coinductive-recursive types that may not have a proper
explanation.)

--
/NAD

Michael Shulman

unread,
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!
> --
> 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.

Joyal, André

unread,
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.

Martín Hötzel Escardó

unread,
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.


Michael Shulman

unread,
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.
> --
> 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.

Bas Spitters

unread,
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

Kevin Buzzard

unread,
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
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
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQxAZEXiCSS5%2BipOszo%3DJeymDXL3jyfuNFdY7AKxAZSS4g%40mail.gmail.com.

Kevin Buzzard

unread,
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
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

Nicola Gambino

unread,
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

Valery Isaev

unread,
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.

Michael Shulman

unread,
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.

Martín Hötzel Escardó

unread,
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

Kevin Buzzard

unread,