# Is there a formal difference between $f:X \to X$ and $f\in X \to X$?

We can denote by $X\to X$ the set of all functions from $X$ to $X$. Therefore, we can use the following statement to say that $f$ is a function from $X$ to $X$: $$f\in X\to X$$

$$f:X \to X$$

In fact, we could say that $X\to X$ is defined as $\{f| f:X\to X\}$. If I'm not mistaken, $:$ is a notation that belongs to type theory, rather than set theory as $\in$ does.

So is there a fundamental difference between these two notations? Does it make sense to say that one of the two is more "fundamental" than the other?

• I've never seen $X \rightarrow Y$ used to indicate the set of all functions from $X$ to $Y$. The usual notation is $Y^X$, and in a categorial setting you would write something like $\mathbf{Set}(X, Y)$. – quicksort Apr 29 '18 at 12:21
• @quicksort, wikipedia says "In set theory, the set of functions from $X$ to $Y$ may be denoted $X → Y$ or $Y^X$", but if you disagree, please read $X^X$ instead. – user56834 Apr 29 '18 at 12:46

Any use of $\in$ usually strongly suggests a set-theoretic context (though you occasionally see it in a type-theoretic context). The $f:X\to Y$ notation was, I believe, popularized in mathematics by category theory. In this case, it means $f\in\mathsf{Hom}(X,Y)$. This is compatible with $f\in Y^X$ in the case that the category is the category of sets and functions. In a general categorical context, $Y^X$ is usually reserved for exponential objects for which it makes no sense to ask if $f\in Y^X$, though you (usually) can ask if there is an arrow $1 \to Y^X$.
In logic, when $X$ and $Y$ are sorts, usually $f:X\to Y$ means that $f$ is a function symbol. In this case, $X$ and $Y$ aren't sets and neither is $X \to Y$. It makes no sense to say $f\in X\to Y$ unless $\in$ isn't being thought of as set membership or we want to say $X\to Y$ means the set of function symbols from $X$ to $Y$. This latter view starts to get rather similar to the categorical view.
In type theory, usually $f:X\to Y$ means something like $f$ has type $X\to Y$ and $X\to Y$ is the type of functions from $X$ to $Y$. Types are not sets and part of the purpose of this notation is to remind one of that fact. Indeed, types are more like sorts and this notation is similar to how it is used in logic. Sometimes $Y^X$ is also used where $Y^X$ is used in a more first-class sense in a way that is compatible with the similar distinction I mentioned for category theory, so we might write $X\to Z^Y$ rather than $X\to(Y\to Z)$. Sometimes no distinction is being made and the notation is completely synonymous and the choice is made purely for typographical reasons. For computer programming, the choice is mostly typographical, f : X -> Y is easier to write and easier to read, though programming languages are also closely related to type theories.
It doesn't really make sense to talk about which of these notations is "more fundamental" than the others in general. That said, the $f:X\to Y$ notation is usually making the least commitments if multiple notations are in use. Often $f:X\to Y$ isn't a proposition with a truth value, so it wouldn't make much sense to write $\{f\mid f:X\to Y\}$. Admittedly, in the context where it isn't a proposition, you usually aren't using set theory. If you really wanted to, you could meta-theoretically write $\{t\mid \cdot\vdash t:X\to Y\}$ to mean the set of closed terms of type $X\to Y$, say. This would have nothing to do with a set of functions though.