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