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.