===== 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$

==== Parents ====
=== Requirements ===
[[Product type]], [[Sum type]]