[fmap]

For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place.

The only problem is that the author is working in Lean and apparently* dismissive of non-classical type theory. So now we're back to lamenting that equality in type theory is broken...

*) I'm going by second hand accounts here, please correct me if you think this statement is too strong.

[cwzwarich]

> For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place.

Arguably, Homotopy type theory still doesn't solve the problem, because while it strengthens the consequences of isomorphism it doesn't distinguish between "isomorphism" and "canonical isomorphism", whereas (some?) mathematicians informally seem to think that there's a meaningful difference.

> The only problem is that the author is working in Lean and apparently* dismissive of non-classical type theory. So now we're back to lamenting that equality in type theory is broken...

In my opinion, Lean made a number pragmatic choices (impredicative Prop, non-classical logic including the axiom of global choice, uniqueness of identity proofs, etc.) that enable the practical formalization of mathematics as actually done by the vast majority of mathematicians who don't research logic, type theory, or category theory.

It's far from established that this is possible at all with homotopy type theory, yet alone whether it would actually be easier or more economical to do so. And even if this state of affairs is permanent, homotopy type theory itself would still be an interesting topic of study like any other field of mathematics.

[lupire]

"Canonical" refers largely to the names we give to things, so that we maximize the extent to which an isomorphism maps the object named A in X to the object named A in Y. And also to choosing an isomorphism that embeds in a different isomorphism (of superstructures) that isn't strictly the topic of the current question.

I don't think anyone thinks canonical isomorphisms are mathematically controversial (except some people having fun with studying scenarios where more than one isomorphism is equally canonical, and other meta studies), they are a convenient communication shorthand for avoiding boring details.

https://en.m.wikipedia.org/wiki/Isomorphism_theorems

[moomin]

I think the original author makes a good case that a) the shorthand approach isn’t going to fly as we formalise b) different mathematicians mean different things by canonical and these details matter when trying to combining results and that therefore 3) it would be better to provide a proper definition of what you’re talking about and give it an unambiguous name.

[euiq]

let me guess: you haven't read the article, have you?

[xigoi]

> Please don't comment on whether someone read an article. "Did you even read the article? It mentions that" can be shortened to "The article mentions that".

https://news.ycombinator.com/newsguidelines.html

[fmap]

> it doesn't distinguish between "isomorphism" and "canonical isomorphism"

You can distinguish these concepts in (higher )category theory, where isomorphisms are morphisms in groupoids and canonical isomorphisms are contractible spaces of morphisms. These sound like complicated concepts, but in HoTT you can discover the same phenomena as paths in types (i.e., equality) and a simple definition of contractibility which looks and works almost exactly like unique existence.

> In my opinion, Lean made a number pragmatic choices (impredicative Prop, non-classical logic including the axiom of global choice, uniqueness of identity proofs, etc.) that enable the practical formalization of mathematics as actually done by the vast majority of mathematicians who don't research logic, type theory, or category theory.

The authors of Lean are brilliant and I'm extremely happy that more mathematicians are looking into formalisations and recognizing the additional challenges that this brings. At the same time, it's a little bit depressing that we had finally gotten a good answer to many (not all!) of these additional challenges only to then retreat back to familiar ground.

Anyway, there were several responses to my original comment and instead of answering each individually, I'm just going to point to the article itself. The big example from section 5 is that of localisations of R-algebras. Here is how this whole discussion changes in HoTT:

1) We have a path R[1/f][1/g] = R[1/fg], therefore the original theorem is applicable in the case that the paper mentions.

2) The statements in terms of "an arbitrary localisation" and "for all particular localisations" are equivalent.

3) ...and this is essentially because in HoTT there is a way to define the localisation of an R-algebra at a multiplicative subset. This is a higher-inductive type and the problematic aspects of the definition in classical mathematics stem from the fact that this is not (automatically) a Set. A higher-inductive definition is a definition by a universal property, yet you can work with this in the same way as you would with a concrete construction and the theorems that the article mentions are provable.

---

There is much more that can be said here and it's not all positive. The only point I want to make is that everybody who ever formalised anything substantial is well aware of the problem the article talks about: you need to pick the correct definitions to formalise, you can't just translate a random math textbook and expect it to work. Usually, you need to pick the correct generalisation of a statement which actually applies in all the cases where you need to use it.

Type theory is actually especially difficult here, because equality in type theory lacks many of the nice properties that you would expect it to have, on top of issues around isomorphisms and equality that are left vague in many textbooks/papers/etc. HoTT really does solve this issue. It presents a host of new questions and it's almost certain that we haven't found the best presentation of these ideas yet, but even the presentation we have solves the problems that the author talks about in this article.

[analytiqhub]

Homotopy type theory is definitely the way to go. This 2016 talk from Vladimir Voevodsky is a good entrypoint for the general audience:

https://www.youtube.com/watch?v=gOBqROtRoPA

[aureianimus]

I'd love to hear a little bit more on what you think the downsides are? (Or a recommendation for a resource to read up on this?)

[zozbot234]

I'd also like to know more about that. My comment points out some things about HoTT that might be described as "downsides" by some but are more like things that people might expect from HoTT given that it 'handles' type equality in a rigorous yet flexible way, but aren't actually feasible in a rigorous treatment, i.e. the system is not going to pick up all the issues that are "brushed aside" in an informal treatment and resolve them on its own. Its behavior will point out to you that these issues exist, but you'll still have to do a lot of work dotting the i's and crossing the t's, as with any formalization.

[zozbot234]

> It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place.

It's not that simple, Buzzard actually seems to be quite familiar with HoTT. The HoTT schtick of defining equality between types as isomorphism does 'handle' these issues for you in the sense that they are treated rigorously, but there's no free lunch in that. You still need to do all the usual work establishing compatibility of values, functions etc. with the relevant isomorphisms, so other than the presentation being somewhat more straightforward there is not much of a gain in usability.

[zozbot234]

Sorry about not providing a reference re: Kevin Buzzard's previously-stated thoughts on HoTT, but see https://ncatlab.org/nlab/show/Kevin+Buzzard

[jhanschoo]

Can you elaborate more on how you think HoTT can solve the issue Buzzard mentions that when formalizing informal mathematics, the author frequently has a model (or, a particular construction) in mind and requires properties present in the model, and then claims that this is true for all "canonically equivalent" objects without actually spending time explicating the abstract nonsense required to properly specify the properties that canonically equivalent objects preserve, for their developement? (see: a product vs. the product)

Edit: and furthermore, the situation where the obvious choice of universal property (read: level of isomorphism) was a poor one, in their attempt to formalize localizations.

[YetAnotherNick]

I think 99.9% of the people talking about HoTT haven't used HoTT in practice. They just see isomorphism is equivalent to equivalence(or something similar), comes up with a mental model and think this is the main contribution of HoTT, whereas isomorphism is a well studied thing even before formal set theory was a thing. HoTT gets weird and anyone who has tried any tool to prove anything in HoTT knows this, and this is the reason why it didn't got adopted even though many leading tools like lean worked hard to implement it.

[staunton]

Have you used it? If yes, could you elaborate? Or if you haven't, can you point to any recent source on what it's like to be using HoTT in 2024?

[YetAnotherNick]

[1] is the only video which I would say I found any bit accessible. But to be honest even after spending days, I couldn't grok it. And in my observation, different implementations of HoTT are quite different from each other.

[1]: https://www.youtube.com/watch?v=x4cz1OgpU3M

[bumbledraven]

For reference, the paper mentions the term "homotopy" exactly once, in this sentence:

> The set-theoretic definition is too strong (Cauchy reals and Dedekind reals are certainly not equal as sets) and the homotopy type theoretic definition is too weak (things can be equal in more than one way, in contrast to Grothendieck’s usage of the term).

[voxl]

Classical versus non-classical has nothing to do with it. HoTT does not work to capture what a mathematician means by "unique isomorphism" because witnesses of equality in HoTT are very much not unique.

[nicklecompte]

I think HOTT helps remove a lot of the footguns and computational hairiness around using type-theoretic mathematics. But the issues Buzzard is talking about are really more profound than that. This relates to a much deeper (but familiar and nontechnical) philosophical problem: you assign a symbol to a thing, and read two sentences that refer to the same symbol ("up to isomorphism"), but not necessarily the same thing. If the sentences contradict each other, is it because they disagree on the meaning of the symbol, or do they disagree on the essence of the thing? There is a strong argument that most debates about free will and consciousness are really about what poorly-understood thing(s) we are assigning to the symbol. Worse, this makes such debates ripe for bad faith, where flaws in an argument are defended by implicitly changing the meaning of the symbol.

In the context of """simple""" mathematics, preverbal toddlers and chimpanzees clearly have an innate understanding of quantity and order. It's only after children fully develop this innate understanding that there's any point in teaching them "one," "two," "three," and thereby giving them the tools for handling larger numbers. I don't think it makes sense to say that toddlers understand the Peano axioms. Rather, Peano formulated the axioms based on his own (highly sophisticated) innate understanding of number. But given he spent decades of pondering the topic, it seems like Peano's abstract conception of "number" became different from (say) Kronecker's, or other constructivists/etc. Simply slapping the word "integer" on two different concepts and pointing out that they coincide for quantities we can comprehend doesn't actually do anything by itself to address the discrepancy in concept revealed by Peano allowing unbounded integers and Kronecker's skepticism. (The best argument against constructivism is essentially sociological and pragmatic, not "mathematically rational.")

Zooming out a bit, I suspect we (scientifically-informed laypeople + many scientists) badly misunderstand the link between language and human cognition. It seems more likely to me that we have extremely advanced chimpanzee brains that make all sorts of sophisticated chimpanzee deductions, including the extremely difficult question of "what is a number?", but to be shared (and critically investigated) these deductions have to be squished into language, as a woefully insufficient compromise. And I think a lot of philosophical - and metamathematical - confusion can be understood as a discrepancy between our chimpanzee brains having a largely rigorous understanding of something, but running into limits with our Broca's and Wernicke's areas, limits which may or may not be fixed by "technological development" in human language. (Don't even get me started on GPT...)

[psychoslave]

The level of insights and clearness in your message, and most comments in this thread actually, is surprising great compared to what I often read on HN.

Thank you very much for this

[Ericson2314]

The fact that Buzzard is writing this paper at all to me shows a much higher degree of respect than before --- see how humble the overview is. I think this is great progress!