Comment by bumbledraven

For reference, the paper mentions the term "homotopy" exactly once, in this sentence:

> The set-theoretic definition is too strong (Cauchy reals and Dedekind reals are certainly not equal as sets) and the homotopy type theoretic definition is too weak (things can be equal in more than one way, in contrast to Grothendieck’s usage of the term).