 When actually doing constructive mathematics in type theory, one often needs to equip completely presented sets (types) with an equivalence relation, the combination being known as a setoid. Mappings are then functions that respect those equivalence relations. This is in close agreement with the way Bishop presented his informal theory of sets. The dependent types of Martin-Löf are useful for constructing subsets. For instance, the real numbers can be constructed using the \(\Sigma\)-type (see Martin-Löf [1984]):