Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
functions [2015/12/14 10:34] nikolaj |
functions [2015/12/14 10:35] nikolaj |
||
|---|---|---|---|
| Line 11: | Line 11: | ||
| == todo == | == todo == | ||
| - | Is there any reason to generalize $\to$ (as in $A\to{B}$, fucntion type) to $\prod$ (as in $\prod_{a:A}B(a)$, i.e. dependent product type) here? | + | 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 === | === Related === | ||
| [[Domain of discourse]] | [[Domain of discourse]] | ||
