Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
cardinal_arithmetic_with_types [2014/03/30 20:18] nikolaj |
cardinal_arithmetic_with_types [2014/03/30 20:19] nikolaj |
||
|---|---|---|---|
| Line 32: | Line 32: | ||
| This doesn't just hold for the arithmetic side, but we can also define the type constructors in terms of $\sum$ and $\prod$: | This doesn't just hold for the arithmetic side, but we can also define the type constructors in terms of $\sum$ and $\prod$: | ||
| - | For $A$ is a type of only two terms $\mathcal{l},\mathcal{r}:A$ and $B(\mathcal{l}):=X, B(\mathcal{l}):=Y$, we get | + | For $A$ is a type of only two terms $\mathcal{l},\mathcal{r}:A$ and $B(\mathcal{l}):=X, B(\mathcal{r}):=Y$, we get |
| - | * $\sum(x:A).\,B(x)=X+Y$ | + | * $\sum(x:A).\,B(x)=B(\mathcal{l})+B(\mathcal{r})=X+Y$ |
| For $B$ being constant (think of how the fibration looks like), we get | For $B$ being constant (think of how the fibration looks like), we get | ||
| * $\sum(x:A).\,B(x)=\sum(x:A).\,B=A\times B$ | * $\sum(x:A).\,B(x)=\sum(x:A).\,B=A\times B$ | ||
