Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
cardinal_arithmetic_with_types [2014/03/30 20:18] nikolaj |
cardinal_arithmetic_with_types [2014/03/30 20:18] nikolaj |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| If $X$ has two terms $a,b:X$ and $Y$ has three terms $u,v,w:Y$, then $X+Y$ has five terms | If $X$ has two terms $a,b:X$ and $Y$ has three terms $u,v,w:Y$, then $X+Y$ has five terms | ||
| - | $\nu_{\mathcal l}(a),\ \nu_{\mathcal l}(b),\ \nu_{\mathcal r}(u),\ \nu_{\mathcal r}(v),\ \nu_{\mathcal r}(w):X+Y$ | + | * $\nu_{\mathcal l}(a),\ \nu_{\mathcal l}(b),\ \nu_{\mathcal r}(u),\ \nu_{\mathcal r}(v),\ \nu_{\mathcal r}(w):X+Y$ |
| Similarly, $X\times Y$ has six terms | Similarly, $X\times Y$ has six terms | ||
| - | $\langle a,u\rangle,\ \langle a,v\rangle,\ \langle a,w\rangle,\ \langle b,u\rangle,\ \langle b,v\rangle,\ \langle b,w\rangle:X\times Y$ | + | * $\langle a,u\rangle,\ \langle a,v\rangle,\ \langle a,w\rangle,\ \langle b,u\rangle,\ \langle b,v\rangle,\ \langle b,w\rangle:X\times Y$ |
| and $X\to Y$ has eight terms | and $X\to Y$ has eight terms | ||
| - | $a\mapsto u\text{ and }b\mapsto u,\ a\mapsto u\text{ and }b\mapsto v,\dots :X\to Y$ | + | * $a\mapsto u\text{ and }b\mapsto u,\ a\mapsto u\text{ and }b\mapsto v,\dots :X\to Y$ |
| and these have no terms else. So clearly, at least for types where a cardinal assignment $|\cdot|$ into the natural numbers makes sense, we have | and these have no terms else. So clearly, at least for types where a cardinal assignment $|\cdot|$ into the natural numbers makes sense, we have | ||
| 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 $\sum(x:A).\,B(x)=X+Y$ | + | 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 |
| + | * $\sum(x:A).\,B(x)=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$ | ||
