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

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

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

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$

Product type, Sum type