Origins of the numerical notation for types in type theory
This almost certainly derives from (finite) set theory. The cardinality of a finite set $S$, written $|S|$, is the number of distinct elements it has. For finite sets, we have the following relations: $$\begin{align}
|\emptyset| &amp; = 0 \\
|1| &amp; = 1 \\
|A\times B| &amp; = |A||B| \\
|A\uplus B| &amp; = |A|+|B| \\
|B^A| &amp; = |B|^{|A|}
\end{align}$$
where $A\times B$ is the Cartesian product of $A$ and $B$, $A\uplus B$ is the disjoint union of $A$ and $B$, and $B^A$ is the set of functions from $A$ to $B$. The type theoretic constructions $A\times B$ (product types), $A+B$ (sum types), and $A\to B$ (function types) correspond to these set theoretic constructs. For example, finite sets form a model of the simply typed lambda calculus with products and sums where product, sum, and function types are interpreted as exactly the constructs on finite sets above. This correspondence is not general. There are many other models of the simply typed lambda calculus that will interpret these type constructions differently. Nevertheless, this is the archetypal example.

Category theorists often use similar notation but it is motivated the same way.

Another take on this is that these type operations (ignoring function types though their existence implies distributivity) make types into a commutative semiring up to isomorphism. Equations that you can prove in the theory of commutative semirings give rise to type isomorphisms.