===== Function =====
==== Set ====
| @#55CCEE: context     | @#55CCEE: $X,Y$ |
| @#FFBB00: definiendum | @#FFBB00: $f\in Y^X $ |
| @#AAFFAA: inclusion   | @#AAFFAA: $f\in$ partial function$(X,Y)$ |
| @#55EE55: postulate   | @#55EE55: $\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

| @#EEEE55: predicate   | @#EEEE55: $f\dots \text{functional} \equiv \exists X,Y.\ f\in Y^X$ |
| @#EEEE55: predicate   | @#EEEE55: $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

| @#EEEE55: predicate   | @#EEEE55: $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]]. 
==== Parents ====
=== Subset of ===
[[Partial function]]
=== Element of ===
[[Set]]
=== Context ===
[[Relation domain]]
=== Related ===
[[Functions]]