## Cardinal arithmetic with types

### Theorem

##### Sum, product and function type

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$

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$

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$

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

$\left|X+Y\right|=\left|X\right|+\left|Y\right|$
$\left|X\times Y\right|=\left|X\right|\times \left|Y\right|$
$\left|X\to Y\right|=\left|Y\right|^{\left|X\right|}$

where $+,\times, \to$ on the left hand side are type constructors and the ones on the left hand side are the basic arithmetic operations.

##### Depended types

We haven't defined the constructor rules for depended sum and product, $\sum$ and $\prod$, but let's just remark that the above can be viewed as special cases for depended types:

If $x:A$ and $B(x)$ is a family of types varying over $A$ (the $B$'s are fibers over $A$), then the sum type $\sum(x:A).\,B(x)$ (disjoint union of fibers) and the product type $\prod(x:A).\,B(x)$ (space of sections) fulfill

$\left|\sum(x:A).\,B(x)\right|=\sum_{x:A}\left|B(x)\right|$
$\left|\prod(x:A).\,B(x)\right|=\prod_{x:A}\left|B(x)\right|$

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{r}):=Y$, we get

• $\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

• $\sum(x:A).\,B(x)=\sum(x:A).\,B=A\times B$
• $\prod(x:A).\,B(x)=\prod(x:A).\,B=A\to B$