Real numbers can be built in several different ways :
Following the construction of Erett Bishop's real numbers in constructive analysis, real numbers can be formalized in Agda as a sequence of rational numbers together with a proof of convergence of this sequence:
-- Constructible Real numbers as described by Bishop -- A real number is defined to be a sequence along -- with a proof that the sequence is regular record ℝ : Set where constructor Real field f : ℕ -> ℚ reg : {nm : ℕ} -> ∣ fn - fm ∣ ≤ (suc n)⁻¹ + (suc m)⁻¹
Checkout this repository to formally build an equivalence relation using this definition.
Another way to determine real numbers is through Dedekind abbreviations, which, as mentioned by @vitrus, are discussed in chapter 11 of the Homotopy Type Theory book.