4 ms·

A Lean textbook! Why no HoTT, though? "Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?" https://news.ycombinator.com/item?id=431

A Lean textbook! Why no HoTT, though? "Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?" https://news.ycombinator.com/item?id=43196452 https://news.ycombinator.com/item?id=43196452 Additional Lean resources from HN this week: "100 theorems in Lean" https://news.ycombinator.com/item?id=44075061 https://news.ycombinator.com/item?id=44075061 "Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean" https://news.ycombinator.com/item?id=44119725 https://news.ycombinator.com/item?id=44119725

krapht 1y ago
Why should there be HoTT, though? A lot less work has gone into making HoTT theorem provers ergonomic to use. Also, the documentation is a lot more sparse. The benefits of HoTT are also unclear - it seems to only save work when dealing with very esoteric constructs in category theory.
moomin 1y ago
It’s an existing textbook, which answers the “Why not HoTT?” question. Although another might be that people doubt its pedagogical value.
Mond_ 1y ago
HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this. HoTT isn't even remotely close to being accepted as a reasonable standard, and it's kind of a non-starter for most people. This is a bit like asking the developers of a Javascript framework why they they didn't write a framework for Elm or Haskell.
- zozbot234 1y ago
  > HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this. It's also a bit of a controversial topic in formalized mathematics. See the following relevant comments by Kevin Buzzard (an expert in Lean and also in the sort of abstract nonsense that might arguably benefit directly from HoTT) - Links courtesy of https://ncatlab.org/nlab/show/Kevin+Buzzard https://ncatlab.org/nlab/show/Kevin+Buzzard * Is HoTT the way to do mathematics? (2020) https://www.cl.cam.ac.uk/events/owls/slides/buzzard.pdf https://www.cl.cam.ac.uk/events/owls/slides/buzzard.pdf ("Nobody knows because nobody tried") * Grothendieck's use of equality (2024) https://arxiv.org/abs/2405.10387 https://arxiv.org/abs/2405.10387 - Discussed here https://news.ycombinator.com/item?id=40414404 https://news.ycombinator.com/item?id=40414404
seanhunter 1y ago
> Why no HoTT, though? Sort of a weird question to ask imo. Terrence Tao has a couple of analysis textbooks and this is his companion to the first of those books in Lean. He doesn’t have a type theory textbook, so that’s why no higher-order type theory - it’s not what he’s trying to do at all.
- westurner 1y ago
  If HoTT is already proved and sets, categories, and types are already proven; I agree that it's not necessary to prove same in an applied analysis book; though it is another opportunity to verify HoTT in actual application domains. "Is this consistent with HoTT?" a tool could ask.
  - seanhunter 1y ago
    But none of this is what he’s trying to do. He wrote a book to go with his course in undergraduate real analysis. <= this does not contain HoTT because HoTT is not part of undergraduate real analysis He’s making a companion to that book for lean <= so this also doesn’t contain HoTT. Just like it doesn’t contain anything about raising partridges or doing skydiving, it doesn’t have anything about HoTT because that’s not what he’s trying to write a book about. He’s writing a lean companion to his analysis textbook. I get that you are interested in HoTT. If so you should probably get a book on it. This isn’t that book. He is a working mathematician showing how a proof assistant can be used as part of accomplishing a very specific mainstream mathematical task (ie proving the foundational theorems of analysis). He's not trying to write something about the theoretical basis for proof assistants.
    - westurner 1y ago
      Are there types presented therein? Presumably, left-to-right MRO solves for diamond-inheritance because of a type theory. I suppose it doesn't matter if HoTT is the most sufficient type / category / information-theoretic set theory for inductively-presented real analysis in classical spaces at all. But then why present in Lean, if the precedent formalisms are irrelevant? (Fairly also, is HoTT proven as a basis for Lean itself, though?)
v64 1y ago
Formalization of many of the ideas from HoTT are currently happening in the Agda community. [1] It's out of my wheelhouse, so I don't know the exact motivations, but Agda is apparently a better way to formalize those ideas than in Lean. Also, there's a new textbook coming out later this year that's a more modern update to the original HoTT book [2] which also has an Agda formalization. [3] [1] https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/ https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Note... [2] https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6 https://www.cambridge.org/core/books/introduction-to-homotop... [3] https://github.com/HoTT-Intro/Agda https://github.com/HoTT-Intro/Agda

krapht 1y ago

Why should there be HoTT, though? A lot less work has gone into making HoTT theorem provers ergonomic to use. Also, the documentation is a lot more sparse. The benefits of HoTT are also unclear - it seems to only save work when dealing with very esoteric constructs in category theory.

moomin 1y ago

It’s an existing textbook, which answers the “Why not HoTT?” question. Although another might be that people doubt its pedagogical value.

Mond_ 1y ago

HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this. HoTT isn't even remotely close to being accepted as a reasonable standard, and it's kind of a non-starter for most people. This is a bit like asking the developers of a Javascript framework why they they didn't write a framework for Elm or Haskell.

zozbot234 1y ago
> HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this. It's also a bit of a controversial topic in formalized mathematics. See the following relevant comments by Kevin Buzzard (an expert in Lean and also in the sort of abstract nonsense that might arguably benefit directly from HoTT) - Links courtesy of https://ncatlab.org/nlab/show/Kevin+Buzzard https://ncatlab.org/nlab/show/Kevin+Buzzard * Is HoTT the way to do mathematics? (2020) https://www.cl.cam.ac.uk/events/owls/slides/buzzard.pdf https://www.cl.cam.ac.uk/events/owls/slides/buzzard.pdf ("Nobody knows because nobody tried") * Grothendieck's use of equality (2024) https://arxiv.org/abs/2405.10387 https://arxiv.org/abs/2405.10387 - Discussed here https://news.ycombinator.com/item?id=40414404 https://news.ycombinator.com/item?id=40414404

seanhunter 1y ago

> Why no HoTT, though? Sort of a weird question to ask imo. Terrence Tao has a couple of analysis textbooks and this is his companion to the first of those books in Lean. He doesn’t have a type theory textbook, so that’s why no higher-order type theory - it’s not what he’s trying to do at all.

westurner 1y ago
If HoTT is already proved and sets, categories, and types are already proven; I agree that it's not necessary to prove same in an applied analysis book; though it is another opportunity to verify HoTT in actual application domains. "Is this consistent with HoTT?" a tool could ask.
- seanhunter 1y ago
  But none of this is what he’s trying to do. He wrote a book to go with his course in undergraduate real analysis. <= this does not contain HoTT because HoTT is not part of undergraduate real analysis He’s making a companion to that book for lean <= so this also doesn’t contain HoTT. Just like it doesn’t contain anything about raising partridges or doing skydiving, it doesn’t have anything about HoTT because that’s not what he’s trying to write a book about. He’s writing a lean companion to his analysis textbook. I get that you are interested in HoTT. If so you should probably get a book on it. This isn’t that book. He is a working mathematician showing how a proof assistant can be used as part of accomplishing a very specific mainstream mathematical task (ie proving the foundational theorems of analysis). He's not trying to write something about the theoretical basis for proof assistants.
  - westurner 1y ago
    Are there types presented therein? Presumably, left-to-right MRO solves for diamond-inheritance because of a type theory. I suppose it doesn't matter if HoTT is the most sufficient type / category / information-theoretic set theory for inductively-presented real analysis in classical spaces at all. But then why present in Lean, if the precedent formalisms are irrelevant? (Fairly also, is HoTT proven as a basis for Lean itself, though?)

v64 1y ago

Formalization of many of the ideas from HoTT are currently happening in the Agda community. [1] It's out of my wheelhouse, so I don't know the exact motivations, but Agda is apparently a better way to formalize those ideas than in Lean. Also, there's a new textbook coming out later this year that's a more modern update to the original HoTT book [2] which also has an Agda formalization. [3] [1] https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/ https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Note... [2] https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6 https://www.cambridge.org/core/books/introduction-to-homotop... [3] https://github.com/HoTT-Intro/Agda https://github.com/HoTT-Intro/Agda