Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
dependent_type_theory [2014/11/16 16:15] nikolaj |
dependent_type_theory [2015/01/08 01:14] ben don't insult the parser |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ===== Dependent type theory ===== | + | ===== Dependent type theory ===== |
| ==== Framework ==== | ==== Framework ==== | ||
| We want dependent types together with type constructors | We want dependent types together with type constructors | ||
| Line 28: | Line 28: | ||
| Then | Then | ||
| - | * $\to$ can be taken as $\Pi$ when the quantified expression is constant | + | * $\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 | + | * $\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}$ | + | * $+$ can be taken as $\Sigma$ over ${\bf 2}$, here we need an if-construction |
| * ${\bf 1}$ can be taken as ${\bf 0}\to{\bf 0}$, since $\lambda x.x$ is a term of this type | * ${\bf 1}$ can be taken as ${\bf 0}\to{\bf 0}$, since $\lambda x.x$ is a term of this type | ||
