Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
cardinal_arithmetic_with_types [2014/03/30 20:19] nikolaj |
cardinal_arithmetic_with_types [2014/03/30 20:19] nikolaj |
||
|---|---|---|---|
| Line 33: | Line 33: | ||
| 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 | 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$ | ||
