===== Functions =====
==== Meta ====
${\mathfrak D}_\mathbb{\to}$

-----
=== Discussion ===
== Many definitions are implcit ==
Caution: 
Many function definitions are implicit, sometimes secretly so. E.g. defining 

$f(x):=\sum_{n=0}^\infty\frac{(-1)^{3n}}{n!}z^n$ 

is defining 

$f(x):=\lim_{m\to\infty}\sum_{n=0}^m\frac{(-1)^{3n}}{n!}z^n$ 

and a Limit definition is always a Task to find said limit.

== Practically speaking, uor functions are partitially defined ==
Caution: In the function definition, the domain of the function, as well as variables in context, are stated quite broadly - it must be checked if the to-be-function would return a value for any given input. 

In that sense, "Functions" really is "Partial functions", a priori, although I try to state good valid domains on AoC.

== todo ==
Is there any reason to generalize $\to$ to $\prod$ here? I.e. going from $A\to{B}$ (function type) to $\prod_{a:A}B(a)$ (dependent product type).

-----
=== Related ===
[[Domain of discourse]]