I’m reading chapter 3, entitled “Set Theory” of *Constructive Analysis* by Errett Bishop and Douglas Bridges. It’s pretty hard to figure out what the author means. For instance:

… a

setis defined by describing what must be done to construct anelementof the set, and what must be done to show that two elements of the set areequal.

The author defines a subset `A` of a set `B` to be a set `A` along with a suitable inclusion map `i`:`A` ⇒ `B`. Anyhow, to give an idea how vague his definition of a set is, consider the following definition of the void subset (`∅`) of any set `S`.

The

void subset∅of a setSis defined as follows. To construct an elementxof∅, construct an elementsofSand prove that 0=1; the inclusion map is defined byi(x)≡s. The definition of∅is negativistic, and we prefer to mention the void set as seldom as possible.

Firstly, there might not be a way of constructing an element `s` of `S`. Secondly, how is one supposed to prove that 0=1?

Fortunately I know type theory, and know what he is trying to say. His definition of a set is what is ‘commonly’ known as a setoid. A setoid is a type, and an equivalence relation. More accurately it is a triple <`S`, ≈_{S}, `p`_{S, ≈S}>.
where:

`S`is a type.- ≈
_{S}is a function from`S`×`S`producing a type. `p`_{S, ≈S}is a proof that ≈_{S}is an equivalence relation.

Really `p` is also a triple of three proofs. One proving reflexivity, one proving symmetry, and one proving transitivity. You can divide the structures up however you want.

Anyhow a subset of a set <`S`, ≈_{S}, `p`>
would be a set <`A`, ≈_{A}, `q`> and an inclusion map `i`:`A` ⇒ `S`, and a proof `r` that whenever `a`≈_{A}`a`′ then `i`(`a`)≈_{S}`i`(`a`′).

Finally we can defined the void subset of a set <`S`, ≈_{S}, `p`> as having the type ⊥ (bottom), with = (Leibniz’s equality, but really any function will do). The inclusion map will be abort_{S}:⊥ ⇒ `S`. Finally, to prove the inclusion map is sound:

- We are given
`a`:⊥ and`a`′:⊥ and that`a`=`a`′. `a`:⊥ is impossible, so by contradiction we are done (in otherwords return abort_{abortS(a)≈SabortS(a′)}(`a`)).

(If you want, you can take ⊥≡(0=1), as there is a canonical bijection between the two types.)

See, wasn’t that more clear? I’m not really sure that the definition is negativistic

. Negativistic things are of the form `foo` ⇒ ⊥, but our inclusion map is the other way: ⊥ ⇒ `foo`. I think the author may be in error on this point.