It does say something important about differentiation, which shows up very clearly and explicitly in the theory of generating functions and combinatorial specie

It does say something important about differentiation, which shows up very clearly and explicitly in the theory of generating functions and combinatorial species, and relates to my second proof. When you differentiate a type, you get the type of its splittings or what Conor McBride calls its one-hole contexts. > >1 + r + r^2 + ... = 1/(1-r) is the type of tuples with entries in r ? r^n is the type of n-tuples with entries in r. When you sum over all n, you get the type of tuples of any length with entries in r. One thing that might be confusing you is that I'm thinking of r itself as a type, not as a number. You get a number from a type by counting its elements, but a type has much more structure than just its size.