I have some uncertainty about setoids and their purpose.

I will ask some overlapping questions.

Why do we need setoids?

Why can't we just work with quotient types?

Why does constructive math like setoids?

Why are setoids considered the natural translation of classical (extensional) sets into type theory?

Patrick Nicodemus said:

Why do we need setoids?

Why can't we just work with quotient types?

The usual motivation is that we're working in a theory without quotient types, like CIC or MLTT. In a theory with quotienting, setoids play a much smaller role (but typically still some; you're always going to have some equivalence relations you haven't yet quotiented by, at least).

Patrick Nicodemus said:

Why does constructive math like setoids?

I can't remember exactly where it comes in, but I believe the principle of choice is essential to the construction of quotients in ZFC (something something canonical elements of equivalence classes...). Hopefully someone can clarify this. When we don't have choice, we have to do something explicit in the foundations to allow them to exist. Furthermore, Martin-Löf's formulation of the identity type is quite allergic to proofs of equality between syntactically distinct terms, so well behaved type theories with quotients have typically had to replace it (e.g in cubical type theory).

Patrick Nicodemus said:

Why are setoids considered the natural translation of classical (extensional) sets into type theory?

When we don't have things like quotienting and function extensionality, then `Set`

just isn't good enough for any non-trivial algebra and category theory. For example, without function extensionality, the category of sets doesn't have general coproducts, because the equations we need to prove are between functions, and they don't happen to hold by judgemental equality. Without quotients, you don't get things like real numbers or tensor products. Instead, we take the category of setoids, where there are function setoids satisfying function extensionality and we can take whatever quotients we want.

For finitary algebraic structures, you don't need choice to construct quotients. For infinitary ones, you will need some form of choice. Typical examples include compelete lattices.

In general, you cannot make all quotient equalities into judgemental ones since this will break decidability of typechecking.

However you can get pretty far with decidable quotients.

I've been reading up on this the past couple days and I found a fairly concrete example in Troelstra's book on constructivism and mathematics that helps to illustrate the value of setoids.

Question: Constructively, is it true that $\forall x\in \mathbb{R}, \exists n\in \mathbb{N}, x < n$?

Working with strict equality, we almost certainly cannot prove this theorem constructively, as all functions on $\mathbb{R}$ that we know how to define constructively are continuous, and the only continuous functions $\mathbb{R}\to \mathbb{N}$ are the constant functions.

However if one allows for operations $\mathbb{R}\to \mathbb{N}$ that do not respect equality, and so perhaps send distinct Cauchy sequences to distinct natural numbers even when these distinct Cauchy sequences are equal as real numbers, then the problem can be solved easily: fix any rational $\epsilon$ and for any Cauchy sequence $\{x_n\}$, compute this sequence out to $x_N$ where the precision of the sequence past $N$ is better than $\epsilon$, and return the least natural number greater than $x_n+\epsilon$. This in itself is pretty good justification for setoids in my book - surely I think most mathematicians would be badly turned off from constructive mathematics if you told them it could not be proved that every real was bounded above by a natural number!

Troelstra also points out that the set/setoid distinction and the extensional/intensional distinction is closely related to the constructivity or nonconstructivity of the axiom of choice, which is something that Martin-Lof addresses at length in his paper "100 years of the axiom of choice". For types $A, B$, and $f : A\to B$, if $f$ is surjective then it has a section; this is a theorem of MLTT. So in this sense the axiom of choice is a theorem. However if $A, B$ are setoids and $f$ is a function properly speaking, then surjectivity only suggests that there is an 'operation' $g: B\to A$ which splits $f$, not necessarily respecting the equality. The existence of a proper function $s : B\to A$ with $sf = \operatorname{id}_B$ is much less trivial, matching the conventional wisdom that the Axiom of Choice is a badly nonconstructive axiom (conventional wisdom which is backed up by the theorems of Diaconescu and Goodman-Myhill that the axiom of choice implies LEM).

(deleted)

Working with strict equality, we almost certainly cannot prove this theorem constructively, as all functions on $\mathbb{R}$ that we know how to define constructively are continuous, and the only continuous functions $\mathbb{R}\to \mathbb{N}$ are the constant functions.

`∀x∈R,∃n∈N,x<n`

is not a function to nat (because of exists which squashes)

indeed you need axiom of choice to turn such a thing into `exists f : real -> nat, forall x, x < f x`

It's a general principle of any "reasonable" foundation that (proposition-valued) predicates can ignore quotienting of their arguments. With HoTT-style h-propositions, it's clear how to get this to work: The eliminator for quotients says that you get an element of the unquotiented set, but you have to show that the term you produce respects the equivalence relation the set was quotiented by. It's easy to prove that the equivalence relation is respected when all the terms you could possibly produce are equal (because they're h-props). We can reproduce this style of reasoning in setoids by interpreting $\forall$ as the $\Pi$-setoid and $\exists$ as a $\Sigma$-type together with the equivalence relation which equates everything.

Michael Soegtrop said:

One can compute constructively any real number to arbitrary precision.

The difficulty is that this operation doesn't respect equality on real numbers (the same real number, represented by different Cauchy sequences, could produce different approximations). So you don't get an equivalence-preserving function from the setoid $\mathbb R$ to $\mathbb N$ without squashing the $\mathbb N$ (or dropping the equivalence-preserving requirement).

But is this the question here? The question is if for any concrete constructive real x there constructively exists an n such that x<n. What does this have to do with equality on reals?

how do you define constructive real?

Well as defined in the Coq standard library (https://github.com/coq/coq/blob/3ed332aeac665d034b5f9045ccffcd83ea03d962/theories/Reals/Cauchy/ConstructiveCauchyReals.v#L66)

I guess I should just go and try prove it in Coq - the easiest way to understand it.

those are cauchy sequences not reals

Sorry, I got the wrong line, I updated the link.

what I said was actually meant for the new link so my point stands

Not sure what exactly you mean. As I said I will just try and prove ∀x∈R,∃n∈N,x<n - then I will see.

(with CReal from above as real).

I mean you can prove `exists x y : R, x <= y <= x /\ x <> y`

where `<=`

is CRealLe and `<>`

is the negation of `Coq.Init.Logic.eq`

(deleted)

Patrick Nicodemus said:

Working with strict equality, we almost certainly cannot prove this theorem constructively, as all functions on $\mathbb{R}$ that we know how to define constructively are continuous, and the only continuous functions $\mathbb{R}\to \mathbb{N}$ are the constant functions.

This reasoning is a bit flawed. As mentioned by Michael, it is easy to constructively build a function `f: R -> N`

such that `forall x, x < f x`

. And this function is indeed continuous. But you should keep in mind what continuous actually means here. As James mentioned, either `f`

is not setoid-preserving or `N`

is squashed. In the former case, the input topology is not Hausdorff's, while in the latter case, the output topology is trivial. Thus, in both cases, the notion of continuity is utterly pointless, and does not say much about the constantness of function `f`

.

@Gaëtan Gilbert : sorry, I still can't follow you. Are you saying more or less "yes, with CReal for R you can prove `∀x∈R,∃n∈N,x<n `

, but CReals are no real numbers, because you could prove things which should be contradicting like `exists x y : R, x <= y <= x /\ x <> y`

"?

Can you share you intuition how one would prove that? I don't see that and would even think that I can prove False assuming that.

CReals are no real numbers

yes

they are unquotiented cauchy sequences

Well but isn't this what one usually means by "constructive real"?

Are you sure you can prove `exists x y : R, x <= y <= x /\ x <> y`

? How?

Maybe I got the initial statement of @Patrick Nicodemus wrong. I assumed that "Constructively, is it true" implies that we are talking about constructive reals.

Michael Soegtrop said:

Well but isn't this what one usually means by "constructive real"?

Are you sure you can prove`exists x y : R, x <= y <= x /\ x <> y`

? How?

Sure. Take two equivalent but not equal Cauchy sequences (e.g., the constant sequence zero and any non-constant sequence converging to zero).

@Guillaume Melquiond : ah yes, silly me - interesting. I need to ponder over what this implies for a while.

But this is true for the Coq rationals as well. So stating on that basis that constructive reals are not reals is not quite valid, since one can state on the same basis that Coq rationals are not rationals.

Not quite. If you take Coq's `Qc`

set, you can prove that `x <= y <= x -> x = y`

. That is because the canonicity of a representant in the quotient set is now decidable (while this is not true for Cauchy sequences).

I am talking about the standard library Q: `Record Q : Set := Qmake { Qnum : Z; Qden : positive }.`

.

But `Qc`

is also a standard library.

Ah OK - I thought it was mathcomp.

Anyway I think we can conclude that there exists a definition of rationals in the Coq standard library which defines something which are not rationals if one applies @Gaëtan Gilbert's argument.

Yes. `Q`

should never have been defined as a synonymous for `Z * positive`

. Those are not rational numbers, whichever way you look at them.

I see what you mean and for Q I follow your argument, although I can't say I ever had any issues with QArith Q.

For reals I am not sure if constructive reals in the sense of "unquotiented Cauchy sequences" are not the better model for real numbers. Maybe that has to do with the fact that I am physicist and have a bit more mechanical and less abstract view of the world.

On your last point, would the right solution be to use the *setoid* over unquotiented Cauchy sequences?

Guillaume Melquiond said:

Yes.

`Q`

should never have been defined as a synonymous for`Z * positive`

. Those are not rational numbers, whichever way you look at them.

I guess, to clarify, the point here is that the *set* `Z * positive`

has no more to do with ℚ than the set `nat * nat`

has to do with ℤ. Only the *setoid* deserves to be called `Q`

. That said, the setoid of rational numbers is probably the only codified use of the set `Z * positive`

, so the naming is harmless in practice.

My point is that Coq's `Q`

is not the setoid. The actual setoid is named `Qc`

in the standard library. `Q`

is really just the cartesian product.

Isn't Qc the actual quotient? If a setoid is a pair of a set and an equivalence, calling `Q`

a setoid is as improper as calling the set `Z`

a ring — it’s an abuse of notation that calls for canonical structures (even if Coq does not let you write `Z : ring`

directly, IIUC).

Paolo Giarrusso said:

Isn't Qc the actual quotient?

Right, my mistake. And since `Qeq`

is declared as a global instance, `Q`

can indeed be considered a setoid.

Last updated: Feb 01 2023 at 11:04 UTC