In mathematics, a setoid (X, ~) is a set (or type) X equipped with an equivalence relation ~.
[1] Setoids are studied especially in proof theory and in type-theoretic foundations of mathematics.
In type-theoretic foundations of mathematics, setoids may be used in a type theory that lacks quotient types to model general mathematical sets.
To do real analysis in Martin-Löf's framework, therefore, one must work with a setoid of real numbers, the type of regular Cauchy sequences equipped with the usual notion of equivalence.
Predicates and functions of real numbers need to be defined for regular Cauchy sequences and proven to be compatible with the equivalence relation.