I.D84 — Constructive Reals

TauReal: constructive reals via Cauchy completion of TauRat. Represented as sequences of TauRat approximations with pointwise equivalence. Every TauReal is explicitly specified by a constructive sequence.