## Function

### Set

 context $X,Y$ definiendum $f\in Y^X$ inclusion $f\in$ partial function$(X,Y)$ postulate $\bigcup\pi_1(f)=X$

### Discussion

One defines $\mathrm{dom}(f):=\bigcup\pi_1(f)$. The requirement $\mathrm{dom}(f)=X$ just says that the function must make sense for all inputs.

#### Predicates

Notice that for $f\in Y^X$ and $Y\subset Z$ we also have $f\subset Z^X$. In any situation in which a target set is of relevance, when a function gets introduced one must include a codomain declaration by writing

$f\in Y^X \land \mathrm{codom}(f)=Y$

where $\mathrm{codom}$ is a new logical operator. We write the above as

$f:X\to Y$

We define following two properties

 predicate $f\dots \text{functional} \equiv \exists X,Y.\ f\in Y^X$ predicate $f\dots \text{function} \equiv \exists X,Y.\ f: X\to Y$

One must stress that declaring $\text{codom}(f)=Y$ created a context and it does not follow from $f\in Y^X$ itself. The set $\mathrm{im}(f)$ is clearly the smallest codomain, but any set containing $\mathrm{im}(f)$ might be a candidate. Notice for example that the notion of surjectivity of a function totally depends on this so called type declaration. Functions with different codomains still have the same extensional input-output properties, although, formally, one should differentiate between them. E.g. with different function symbols etc. According to the function property, we want to use the term “function” for a set for which we have declared the codomain.

(Alternatively to the above definitions, one could, in the Bourbakian tradition, also define functions to be a triple $\langle X,Y,f\rangle$, which contains not only the graph but also explicitly names a codomain. In this case, the difference of two functions which different codomains can not be overlooked.)

##### Depended functions within set theory

We will introduce concise notation mirroring the concepts of depended types in type theory.

Consider a function $F$ with domain $A$. We write

 predicate $f:{\large\prod}_{x\in A}F(x)\equiv \left(f:A\to\bigcup_{x\in A} F(x)\right) \land \left(\forall x.\,f(x)\in F(x)\right)$

If you think of $F(x)$ as fibers over a point $x\in A$, then $f$ is a section.

#### Notation

If $\{\langle x,y\rangle\}\in f$, we write $y$ as $f(x)$. The set of all pairs $\{\langle x,f(x)\rangle\}$ is also called the graph of the function and here it's formally the same as $f$. The left and right hand side are denoted argument and value. If $a\in A, b\in B$ and $\mathrm{dom}(f)=A\times B$, then $\langle \langle a,b\rangle,f(\langle a,b\rangle)\rangle \in f$ and we usually write $f(a,b)\equiv f(\langle a,b\rangle)$.

Moreover, one often speaks of a family of indexed objects, which is just an index to image prescription, i.e. it's really just a function. This is e.g. written $f=(f_x)_{x\in X}$ while depending on the context different use of symbols are common. E.g. $(X_i)_{i\in I}$, or what is also common is $(a_n)_{n\in \mathbb N}$. The latter is btw. bijective to an infinite sequence.