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