Huh. Thinking about this example I'm confused, because the power series for exp(x) looks like the type for unordered lists of x: e.g. the term for lists of leng

Huh. Thinking about this example I'm confused, because the power series for exp(x) looks like the type for unordered lists of x: e.g. the term for lists of length three is x^3, and if you ignore order you get x^3/3!. The cosine is almost the same as the even terms of this series, but with a minus sign on every other term. What confuses me (besides what to make of the minus sign) is that the type of sets of x ought to be 2^x -- that is, x -> Bool -- because it's isomorphic to the characteristic function of a set, and a function type is an exponential (https://bartoszmilewski.com/2015/03/13/function-types/ https://bartoszmilewski.com/2015/03/13/function-types/). But 2^x differs from exp(x) by a constant factor. So I seem to be messing with surface-level analogies without real understanding.