Sums and products are also operations in non-muggle math, e.g. for vector spaces if you take a proper linear algebra course. The meaning in type theory is consi

Sums and products are also operations in non-muggle math, e.g. for vector spaces if you take a proper linear algebra course. The meaning in type theory is consistent with that usage. Even in muggle math, e.g. matrix operations are an overloading. In fact overloading is extremely common and generally good practice (when there's an analogy to be had) in math. There are also connections to muggle math/arithmetic. e.g. for types as for numbers, A^(X+Y)=A^X*A^Y. For types, this says a function that takes a sum works by doing case analysis. You can also "forget" things are types and pretend A, X, Y are the number of possible values the types can have, and your equations about types become true statements about numbers.