Is there any correspondence between SUM type in type theory and arithmetical summation?

Question

Is there any correspondence between the coproduct(sum) type in type theory and arithmetical summation?

For example what does 3+4 or x+6 mean in type theory?

Answer 1

The arithmetic notation in type theory is motivated by the behaviour on sets, where the disjoint union $A + B$ has $|A| + |B|$ elements; the cartesian product has $|A| \times |B|$ elements; and the set of functions $B^A$ has $|B|^{|A|}$ elements. Sum, product and function types satisfy many of the usual identities you expect of arithmetic (although typically up to isomorphism, rather than equality).

The paper Objects of Categories as Complex Numbers by Marcelo Fiore and Tom Leinster explores this in some detail, though it helps to have a little experience with algebra or category theory.

Sometimes a natural number $n$ will denote a type with exactly $n$ terms in any context (analogous to a set with $n$ elements). In this setting, $3 + 4 \cong 7$ as types. $x + 6$ isn't well-formed without placing $x$ in some context.