We will even be a bit bolder and define a "finitely supported function", constructively, as a function which has a finite subset of the domain such that all values outside that subset map to zero. Given decidable equality on both domain and codomain, this is equivalent to the definition of a finitely supported function as a function whose support is finite. 8/10
Perhaps this way of treating finitely supported functions constructively is in the literature (or perhaps it is the kind of technical detail which no one thinks to publish), I'm not too sure. But I hope it was interesting for you to read about my work on polynomials and finite support. 9/10
References:
* https://ncatlab.org/nlab/show/support+of+a+function
* https://us.metamath.org/ileuni/df-fsuppfi.html
* https://github.com/metamath/set.mm/issues/5539 including the comments and linked pull requests
10/10
Oct 27, 2026, 4:14 PM@soaproot I believe your definition of finitely supported function is correct when the domain is a discrete set. When I is not necessarily discrete and A is a pointed set (a set with a zero element), I would propose to define a finitely supported function from I to A to be an element of the colimit of all sets Map(J, A), taken over all maps J -> I where J is a finite set.
When I is discrete, one can restrict to subsets J of I and one recovers your description. Note that if I is not discrete, there is no natural map from my proposed colimit to the set Map(I, A), so "finitely supported function" is no longer a special case of "function", but something different.
This thread is related:
https://mathoverflow.net/questions/302516/constructively-is-the-unit-of-the-free-abelian-group-monad-on-sets-injective
@jdw Good point, I have some text saying I've only really been thinking of the case where the domain of the function has decidable equality, but that is worth emphasizing. The tuples of exponents in my thread have decidable equality, in particular. But thanks for the thoughts of what would happen without that condition.