Comment by westurner

9 months ago

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 > "Should Type Theory Replace Set Theory as the Foundation of Mathematics?" (2023)

0 comments

westurner

Reply