In material set theory, the axiom of extensionality defines equality between sets: two sets are equal iff they have the same elements. In structural set theory, one cannot formulate this.

But however, if $A, B$ are two sets in structural set theory, can we ask the question whether $A = B$?

A famous structural set theory is ETCS by Lawvere. In his book with Rosebrugh, he writes:

A category $\mathcal C$ has the following data: Objects: denoted $A, B,C,\dots$

Arrows: denoted $f, g, h,\dots$ (arrows are also often called morphisms or maps)

To each arrow $f$ is assigned an object called its domain and an object called its codomain (if $f$ has domain $A$ and codomain $B$, this is denoted $f : A \to B$)

Composition: To each $f : A \to B$ and $g : B \to C$ there is assigned an arrow $g \circ f : A \to C$ called “the composite of $f$ and $g$” (or “$g$ following $f$ ”) Identities: To each object $A$ is assigned an arrow $1_A : A \to A$ called “the identity on $A$”.

So if he throws all arrows (functions) in one big bag, and has a function that assigns to each arrow a domain and a codomain, it seems to me that one must be able to discuss (equality between objects (sets) and thus also) equality of arrows even if they are not of the same type, i. e., have different domain/codomain.

Also, at one point, the test for equality between two maps $f, g: A \to B$ is formulated as follows:

$(∀x[x: 1 \to A ⇒ f_1x = f_2x]) ⇒ f_1 = f_2$

So it seems to me that $f : A \to B$ is really treated as a statement that is either true or false rather than a typing judgement, which I would have guessed it is when one would leave the question of equality between sets undefined.

  • $\begingroup$ I hope that Andrej Bauer or Mike Shulman will see this.... I read some posts of these two guys here and I think they know quite a lot about this foundational stuff. $\endgroup$ – user105099 Feb 19 '17 at 22:35
  • 1
    $\begingroup$ You might want to take a look at the ncatlab entry, "principle of equivalence", Section 3 ("Motivations") under the subsection, "From foundations and logic". An answer to your question might be contained therein. $\endgroup$ – Thomas Benjamin Feb 20 '17 at 1:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.