Thank you for your answer! Unfortunately the book also uses the Eberlein–Smulian Theorem to prove that equivalence!

With the theory presented in the HoTT book, will I be able to formalize, for example, what are in the books "Classical Set Theory" (by Taras Banakh) and "The Structure of the Real Line" (by Lev Bukovský)? Now I want to learn a Dependent Type Theory similar to those behind theorem prover like Lean and Coq because later I want to rewrite everything using a specific theorem prover (now I just want to prove everything without using any proof assistant).

@PaceNielsen could you indicate me a good, succinct PDF on well order and transfinite induction and recursion?