4 ms·

Thanks ...the differential proof is very insightful and perhaps says something about differentiation itself. EDIT 1: Forgive my ignorance but can you please el

Thanks ...the differential proof is very insightful and perhaps says something about differentiation itself. EDIT 1: Forgive my ignorance but can you please elaborate on 1 + r + r^2 + ... = 1/(1-r) is the type of tuples with entries in r ? EDIT 2: Okay I think I get it. 1 + r + r2 are the terms in the expansion of (1+r)n

psykotic 15y ago
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.
deleted 15y ago
[deleted]