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

[2] https://www.cambridge.org/core/books/introduction-to-homotop...

[3] https://github.com/HoTT-Intro/Agda

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.

> 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

* Is HoTT the way to do mathematics? (2020) 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 - Discussed here https://news.ycombinator.com/item?id=40414404

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.

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

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.

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.

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

   Are there types presented therein?

No. Analysis typically is presented using naive set theory to build the natural numbers, integers, rationals and (via Dedekind cuts) real numbers. For avoidance of doubt in the standard construction of maths these are sets, not types. Then from there a standard first course in analysis deals with the topology of the reals, sequences and series, limits and continuity of real functions, derivatives and the integral. Then if people study analysis further it would typically involve complex numbers and functions, how you do calculus with them, Fourier analysis etc, but types and type theory wouldn’t form part of any standard treatment of analysis that I’m aware of.

Types are not a mainstream topic in pure maths. Type theory was part of Bertrand Russell’s attempt to solve the problems of set theory, which ended up as a bit of a sideshow because ZF/ZFC and naive set theory turned out to require far less of a rewrite of all the rest of maths and so became the standard approach. Types come up I think if people go deeply into formal logic or category theory (neither of which is a type of analysis), but category theory is touched on in abstract algebra after dealing with the more conventional topics (Groups, rings, fields, modules) sometimes. Most people I know who know about type theory came at it from a computer science angle rather than pure maths. You might learn some type theory if you do the type of computer science course where you learn lambda calculus.

   why present in Lean, if the precedent formalisms are irrelevant?

If someone gave a powerpoint presentation, do they have to use the presentation to talk about how powerpoint is made? If someone writes a paper in latex, does the paper have to be about latex and mathematical typesetting? Or are those tools that you’re allowed to use to accomplish some goal?

He’s presenting in Lean because that’s the proof assistant that he actually uses and he’s interested in proof assistants and other tools and how they help mathematicians. He’s not presenting about lean and how it’s made. He’s showing how you can use it to do proofs in analysis.

Well, FWIU, what you refer to as "topology" is founded in HoTT "type theory".

> for avoidance of doubt in the standard construction of maths these are sets, not types. Then from there a standard first course in analysis deals with the topology of the reals, sequences and series, limits and continuity of real functions, derivatives and the integral.

HoTT is precedent to these as well.

So, Lean isn't proven with HoTT either.

Is type theory useful in describing a Hilbert hotel infinite continuum of Reals or for describing quantum values like qubits and qudits?

I don't think I'm overselling HoTT as a useful axiomatic basis for things proven in absence of type and information-theoretic foundations.

From https://news.ycombinator.com/item?id=43191103#43201742 , which I may have already linked to in this thread :

> "Should Type Theory Replace Set Theory as the Foundation of Mathematics?" (2023) https://link.springer.com/article/10.1007/s10516-023-09676-0

That would include Real Analysis (which indeed one isn't at all obligated to prove with a prover and a language for proofs down to {Null, 0, 1} and <0.5|-0.8>).

Are types checked at runtime, with other Hoare logic preconditions and postconditions?

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