How to define real number in agda?

Question

I want to implement Dedekind's cut in Agda. I tried to represent real number first. But I am not able to define it in Agda. How to define it??

Answer 1

Real numbers can be constructed in a few different ways:

Following Erret Bishop's construction of real numbers in Constructive Analysis, real numbers can be formalized in Agda as a sequence of rational numbers along 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 : {n m : ℕ} -> ∣ f n - f m ∣ ≤ (suc n)⁻¹ + (suc m)⁻¹

Checkout this repository for the formalized construction of an equivalence relation using this definition.

Another way to define real numbers is with Dedekind cuts, which as @vitrus mentioned, is discussed in chapter 11 in the Homotopy Type Theory book