Cardinal arithmetic with types


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


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$



Link to graph
Log In
Improvements of the human condition