# Does defining a type of mathematical object require defining a binary relation of “equality”?

I'm trying to determine whether defining a type of mathematical object requires us to know what we mean by another object being "equal" to it. For example, when we define a type of object like set, function, category, or class, is it also necessary to include within our definition what is meant by, for instance, two sets, functions, categories, or classes being "equal"? I would appreciate any commentary.

For some background:

I came upon this question when I was thinking about vector spaces. For example, if we want to study the real vector space of functions from $\mathbb R$ to $\mathbb R$, not only do we need to define the operations of addition and scalar multiplication, but I think we also need to define the binary relation of equality in order to check that the vector space axioms hold. For example, to check whether or not for all functions $f,g$ from $\mathbb R$ to $\mathbb R$ and for every real number $\lambda$, that $$\lambda(f + g) = \lambda f + \lambda g,$$ I think it is necessary to also define what we mean by '$=$' in the above equation, i.e., that $$f = g" \text{ if and only if } f(x) = g(x) \text{ for all } x\in \mathbb R.$$ At what point do we define what is meant by equality of functions? Is it something that is necessary to do as soon as we define what a "function" is?

• You certainly need to know what it means for two functions to be equal. We often don't define it, because the definition is inherited from the set theory definition. Your example is such a case - a function $\mathbb R\to\mathbb R$ is a subset of $\mathbb R\times\mathbb R$ with certain properties, and two functions are considered equal if they are equal as sets. – Thomas Andrews Mar 28 '16 at 20:54
• As others have said, set theory gives you a global equality "for free", but I think it is a very good exercise to explicitly define equality on types that you introduce, ideally as constructively as possible. (In Computational Type Theory, a type literally is a partial equivalence relation on preexisting terms.) This will reveal a lot of hidden complexity, but it will also make you appreciate the fact that checking the equality of linear functions between finite-dimensional vector spaces only involves checking a finite number of inputs. Similarly for polynomials. – Derek Elkins Mar 29 '16 at 5:26

In the set theory paradigm, which is the general workframe of today mathematics, everything is supposed to be a set, so equality has a very clear meaning, given by the extensionality axiom : $x=y$ iff they have the same elements.
For instance a function is a set of the form $(A,B,\Gamma)$ where $\Gamma\subset A\times B$ satisfies some axioms. Then equality of functions is just the equality of the corresponding sets.