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

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?

• You have cardinal(A+B)=cardinal(A)+cardinal(B), and you can check that cardinal is in fact a monoid morphism. Commented Apr 3, 2020 at 11:11

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).
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.
• @al-pal: I don't quite understand your question. You could define type TWO = A + B and type THREE = C + D + E and then the sum type TWO + THREE would have five possible type constructors, corresponding to A, B, C, D or E, which you could case split on. Does this help? Commented Apr 4, 2020 at 20:47
• If X is a specific type, then a polynomial X * X + X + 1 corresponds to a type (either a pair of Xs, a single X or nothing). Here + represents "or", which can be considered the disjoint union of sets. Adding and multiplying polynomials of types acts in the same way you would add and multiply polynomials of integers. Case-splitting corresponds to case, match or switch in the type theory; and the piecewise notation in typical mathematics. Commented Apr 4, 2020 at 22:54