可算選択公理を仮定しない構成的数学では、Cauchy列に基づいた実数の構成をやるときに完備性が示せなくなる（らしい）。この弱点は、実数の構成に使うCauchy列を有理数の点列ではなく、有理数の集合の列とすれば克服できる。
このことは「Handbook of Constructive Mathematics」のFred Richmanの記事で示唆されているが、あまり詳しい取扱いはなかったので自分でやってみた。と言っても、地味な命題の証明は省略しているが……。
https://miz-ar.info/math/real-construction-without-choice-20250816.pdf
Mathlogにも書いてみた。