Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
dependent_type_theory [2014/11/18 22:00] nikolaj |
dependent_type_theory [2014/11/18 22:01] nikolaj |
||
|---|---|---|---|
| Line 30: | Line 30: | ||
| * $\to$ can be taken as $\Pi$ when the quantified expression is constant, $A\to B:=\Pi_{x:A}B$ | * $\to$ can be taken as $\Pi$ when the quantified expression is constant, $A\to B:=\Pi_{x:A}B$ | ||
| - | * $\times$ can be taken as $\Sigma$ when the quantified expression is constant $A\to B:=\Sigma_{x:A}B$ | + | * $\times$ can be taken as $\Sigma$ when the quantified expression is constant $A\times B:=\Sigma_{x:A}B$ |
| * $+$ can be taken as $\Sigma$ over ${\bf 2}$, here we need an if-construction | * $+$ can be taken as $\Sigma$ over ${\bf 2}$, here we need an if-construction | ||
